Anonymous | Login | Signup for a new account 2016-10-01 03:31 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

 Notes lpw25 (developer) 2012-07-16 14:44 edited on: 2012-07-16 16:11 Typically, straight after posting this I thought of a counter-example:   type +_ foo =     Foo: foo   | NotFoo of int   let m_if_foo: type a. a -> a foo -> int =     fun o g ->     match g with       Foo -> o#m     | NotFoo i -> i   let bad = m_if_foo (object end) (Foo :> < > foo) although all the examples of unsafe GADT variance that I had seen previously had been due to a unification between a type parameter and a different part of the constructor, it seems that unifying the type parameter with any type can cause trouble. Could someone please delete this feature request, or edit it so that it is simply a request for some kind of restriction to allow variance annotations for GADTs. gasche (developer) 2012-07-16 16:11 Unfortunately, I don't think this condition is sound, because you can rebuild the counterexample of the (C : < m : int > -> < m : int > t) constructor from the 0-ary (Foo : < m : int > t) constructor:   type (_, _) eq =     | Refl : ('a, 'a) eq   let cast : ('a, 'b) eq -> 'a -> 'b = function     | Refl -> fun x -> x;;   type +_ foo = Foo : < m : int > foo   let get_eq : 'a foo -> ('a, < m : int >) eq = function     | Foo -> Refl   let downcast : < > -> < m : int > = cast (get_eq Foo) I kept working on variance for GADTs (there will be a presentation at the ML workshop in September: http://www.lexifi.com/ml2012/ [^] ; another reason to come to the colocated OCaml Users and Developers Meeting!), and will publish a technical report with detailed proofs, hopefully in August. Since my last Caml List posts, I have understood some aspects of the problem better, such that how to check that type expressions are upward- and downward-closed (so that they're safe as instances of co- and contra-variant GADTs). I also had to make slight fixes to the last presentation which is therefore not quite correct, so I would like to write down everything more precisely, and then try to contact Jacques to see if it's worth trying to adapt the OCaml typechecker. lpw25 (developer) 2012-07-16 16:57 edited on: 2012-07-16 17:01 I had been hoping to find a way to let some very simple examples be permitted, because a full solution seems very difficult. Having considered the problem some more I realised that the examples I was considering were mostly unsafe anyway. So I no longer have a particular use case in mind. It is still an interesting problem though and I look forward to reading your technical report. gasche (developer) 2012-07-16 17:31 I'm marking the bug as "resolved" to simplify the bug-tracking process, but hopefully we will discuss it again in a reasonable future.

 Issue History Date Modified Username Field Change 2012-07-16 14:38 lpw25 New Issue 2012-07-16 14:44 lpw25 Note Added: 0007758 2012-07-16 16:11 lpw25 Note Edited: 0007758 View Revisions 2012-07-16 16:11 gasche Note Added: 0007759 2012-07-16 16:57 lpw25 Note Added: 0007760 2012-07-16 17:01 lpw25 Note Edited: 0007760 View Revisions 2012-07-16 17:31 gasche Note Added: 0007761 2012-07-16 17:31 gasche Status new => resolved 2012-07-16 17:31 gasche Resolution open => not fixable 2012-07-16 17:31 gasche Assigned To => gasche 2012-07-16 17:31 gasche Resolution not fixable => suspended