Anonymous | Login | Signup for a new account 2016-10-01 22:39 CEST
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005688OCamlOCaml typingpublic2012-07-16 14:382012-07-16 17:31
Reporterlpw25
Assigned Togasche
PrioritynormalSeverityfeatureReproducibilityN/A
StatusresolvedResolutionsuspended
PlatformOSOS Version
Product Version
Target VersionFixed in Version
DescriptionI have read the discussion of adding variance annotations to GADTs on caml-list, and thought that a feature request would be a sensible place to discuss a partial solution.

I have not constructed a proof of soundness, but every example of how variance annotations can be unsound is caused by the same general problem: while local constraints from a generalised constructor are in place, two types within the type of that constructor are unified, however one of these types is not invariant so the unification is not always valid.

For example:

type (_, +_) eq = Refl : ('a, 'a) eq

let bad_proof (type t) = (Refl : (<m:t>, <m:t>) eq :> (<m:t>, < >) eq)

let downcast_1 : type a. (a, < >) eq -> < > -> a =
fun (type a) (Refl : (a, < >) eq) (s : < >) -> (s :> a)

let downcast_2 : < > -> <m:o> = downcast_1 bad_proof

The problem here is caused by the fact that the second parameter of eq can be unified with the first parameter under the local constraints of Refl, so it is not safe to change the second parameter to a supertype without also changing the first.

Similarly:

type -'a t = C : < m : int > -> < m : int > t

let eval : type a . a t -> a = fun (C x) -> x

let a = C (object method m = 5 end)

let b = (a :> < m : int ; n : bool > t)

let c = eval b

The problem here is that the type parameter of t can be unified with < m: int > under the local constraints of C, so it is not safe to change it to a subtype.

This suggests a simple safety condition that would allow many of the simple uses of GADTs would be to allow a type parameter with a variance annotation to be instantiated in a GADT constructor provided that none of the other types within the constructor's type can be unified with the instantiated type parameter.

For instance

type +_ foo = Foo : <m: int> foo

would be allowed because <m: int> foo could never be unified with int or <m: int>.

Similarly

type +_ foo = Foo : bool -> <m:int> foo

would be allowed because bool could never be unified with int or <m:int> and <m:int> foo could never be unified with int or <m:int>.

On the other hand

type (_, +_) eq = Refl : ('a, 'a) eq

would not be allowed because the first 'a could be unified with the second 'a, and

type -'a t = C : < m : int > -> < m : int > t

would not be allowed because the first < m: int > could be unified with the second <m : int>.

I think that this scheme is safe and allows many basic patterns to be given a variance. There are probably more accurate restrictions than this, but it seems like a sensible starting point. The implementation could use CType.mcomp to check whether two types could ever be unified. Since it depends on showing that two types could never be unified, it would be a bit fragile and require precise error messages in order to be usable.

If it is felt that this scheme is too heavyweight or too fragile, it would at least be useful to allow variance annotations for special cases that are obviously safe e.g. types with a single type parameter that only appears in constant constructors.
TagsNo tags attached.
Attached Files

 Relationships