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

GADT variance #7004

Closed
vicuna opened this issue Oct 1, 2015 · 4 comments
Closed

GADT variance #7004

vicuna opened this issue Oct 1, 2015 · 4 comments

Comments

@vicuna
Copy link

vicuna commented Oct 1, 2015

Original bug ID: 7004
Reporter: lavi
Assigned to: @lpw25
Status: closed (set by @xavierleroy on 2017-02-16T14:14:53Z)
Resolution: not a bug
Severity: feature
Category: typing
Related to: #7494

Bug description

Currently, variance on GADT are only allowed when the type is used like in a normal ADT.
I know variance in GADT is tricky, but a small and safe improvement would be to allow variance on parameters that appears only on result type.

@vicuna
Copy link
Author

vicuna commented Oct 1, 2015

Comment author: @yallop

The improvement you suggest is actually not sound, at least where the parameter appears more than once in the result type. Consider the equality GADT:

type (+,) eql = Refl : ('a, 'a) eql

If you make the first parameter covariant (for example) then you can coerce (x, x) t to (y, x) t whenever x is a subtype of y, which then allows you to convert freely between x and y when you match against Refl.

@vicuna
Copy link
Author

vicuna commented Oct 1, 2015

Comment author: lavi

Yes you are right, the parameter should only appear once.

@vicuna
Copy link
Author

vicuna commented Oct 1, 2015

Comment author: @lpw25

Parameters which only appear once in the output and are not specialised can already be given a variance:

type +_ t = T : 'a t

If the variable is specialised:

type _ t = T : <foo : int; bar : float> t

then giving it a variance would be unsound:

let f (type a) (x : a t) : a -> unit =
match x with
| T -> fun y ->
print_int y#foo;
print_float y#bar

f (T :> < foo: int > t) (object method foo = 4 end)

@vicuna
Copy link
Author

vicuna commented Oct 2, 2015

Comment author: lavi

Right, sorry, for the noise.
I generalized too quickly the case I encountered:
type _ foobar =
| Foo1 : [> Foo] foobar | Foo2 : [> Foo] foobar
| Bar : [> `Bar] foobar

In this case it is possible to write the cast:
let cast : [Foo] foobar -> [Foo | `Bar] foobar = fun (Foo1 | Foo2 as x ) -> x
But unfortunately this does not scale well.

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