Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Variance annotations for GADTs #5688

Closed
vicuna opened this issue Jul 16, 2012 · 4 comments
Closed

Variance annotations for GADTs #5688

vicuna opened this issue Jul 16, 2012 · 4 comments

Comments

@vicuna
Copy link

vicuna commented Jul 16, 2012

Original bug ID: 5688
Reporter: @lpw25
Assigned to: @gasche
Status: resolved (set by @gasche on 2012-07-16T15:31:02Z)
Resolution: suspended
Priority: normal
Severity: feature
Category: typing
Related to: #7494
Monitored by: @lpw25

Bug description

I 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 .

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.

@vicuna
Copy link
Author

vicuna commented Jul 16, 2012

Comment author: @lpw25

Typically, straight after posting this I thought of a counter-example:

type +_ foo =
Foo: <m: int> 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.

@vicuna
Copy link
Author

vicuna commented Jul 16, 2012

Comment author: @gasche

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.

@vicuna
Copy link
Author

vicuna commented Jul 16, 2012

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Jul 16, 2012

Comment author: @gasche

I'm marking the bug as "resolved" to simplify the bug-tracking process, but hopefully we will discuss it again in a reasonable future.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants