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 and subtyping #6653

Closed
vicuna opened this issue Nov 10, 2014 · 6 comments
Closed

GADT and subtyping #6653

vicuna opened this issue Nov 10, 2014 · 6 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Nov 10, 2014

Original bug ID: 6653
Reporter: @Drup
Assigned to: @gasche
Status: resolved (set by @gasche on 2015-05-24T14:43:39Z)
Resolution: suspended
Priority: normal
Severity: minor
Target version: 4.03.0+dev / +beta1
Category: typing
Monitored by: @gasche @yallop @hcarty

Bug description

Gadt and subtyping don't mix very well in the current form, in particular, this kind of type are not accepted:

type +'a t =
| String : string -> [> String] t | Int : int -> [> Int] t
| Float : float -> [> Float] t | Add : ([< Float | `Int] as 'a) t * 'a t -> 'a t

I know this is a touchy subject (since it's quite easy to do unsound things) but it would be very interesting to support this kind of phantom types.

@vicuna
Copy link
Author

vicuna commented Nov 10, 2014

Comment author: @gasche

I don't think it is sound to claim that this type is covariant, as the Add case restricts its instances to be smaller than [ Float | Int ]. You have [ Float | Int ] <= [ Float | Int | String ] and, if you remove the variance annotation, (Add (Int 1, Float 2.) : [ Float | Int ] t), yet it would be unsound to claim that (Add (Int 1, Float 2.) : [ Float | Int | String ] t), as the following pattern-matching is accepted as total:

let string_is_not_add : [> `String ] t -> unit = function
| String _ -> ()
| Int _ -> ()
| Float _ -> ()

It is unclear to me whether:

  • you actually have a different GADT semantics in mind, that cannot be expressed in OCaml syntax, and that should be soundly accepted as covariant (but then, which is it?)
  • you desire covariance because of the relaxed value restriction, but the types you want to express are fundamentally not covariant (and you should instead long for ways to mark terms as non-expansive to allow generalization in absence of covariance)

@vicuna
Copy link
Author

vicuna commented Nov 10, 2014

Comment author: @Drup

What I wrote is indeed not safe as-is. There are two variations of this type

Variation 1:
type +'a t =
| String : string -> [> String] t | Int : int -> [> Int] t
| Float : float -> [> Float] t | Add : ([< Float | Int] as 'a) t * 'a t -> [> Float | `Int] t

Variation 2:
type +'a t =
| String : string -> [> String] t | Int : int -> [> Int] t
| Float : float -> [> Float] t | Add : ([< Float | `Int] as 'a) t * 'a t -> [> 'a] t (* Not possible to write that for now. *)

The variation 1 is sound (I think) and already more powerful than what is currently possible with GADTs currently.
However, variation 2 is more powerful, since we could add a variant of the following form:

| Succ : [< Int ] t -> [> Int] t

Then "Succ (Add (Int 3, Int 4))" would be accepted, since the type information that Add contains only ints is propagated. It should be sound because [> 'a] contains two row variables, 'a would unify only with Int and Float, but not with `String, hence would not propagate any unintended constructor to the inside of the Add.

I realize this needs several things that are not possible currently, notably the ability to manipulate row variables.

@vicuna
Copy link
Author

vicuna commented Nov 10, 2014

Comment author: @lpw25

I agree with Gabriel that the given type is not actually covariant. However, I think that the following type would be covariant:

type +'a t =
| String : string -> [> String] t | Int : int -> [> Int] t
| Float : float -> [> Float] t | Add : [Int] t * 'a t -> [> `Int] t

and it would be nice to support this case.

Similarly, I personally have types like the following:

type kind = [`String | `Int | `Float]

type 'a t =
  | String : string -> [< kind > `String] t
  | Int : int -> [< kind > `Int] t
  | Float : float -> [< kind > `Float] t
  | Add : [`Int] t * 'a t -> [< kind > `Int] t

and it would be nice to be able to define them as:

type +'a t =
  | String : string -> [< kind > `String] t
  | Int : int -> [< kind > `Int] t
  | Float : float -> [< kind > `Float] t
  | Add : [`Int] t * 'a t -> [< kind > `Int] t
constraint 'a = [< kind]

and have them be treated as covariant, and be able to use them with GADT matching. Unfortunately, the constraint would be required for them to be covariant, and we cannot currently use constrained GADTs because locally abstract types do not match the constraint.

Separately from the above, it would be good to support "subtyping GADTs" as previously discussed by Gabriel and Jacques. Something like:

type +'a t =
  | String : (type a <: string) string -> a t
  | Int : (type a <: int) int -> a t
  | Float : (type a <: float) float -> a t

Which would support code like the following:

let f (type a) (x : a t) : a =
  match x with
  | String s -> (s :> a)
  | Int i -> (i :> a)
  | Float f -> (f :> a)

If we had support for what Gabriel previously called "blind" types (the dual to private types) then the syntax could be something like:

type +'a t =
  | String : (type a = blind string) string -> a t
  | Int : (type a = blind int) int -> a t
  | Float : (type a = blind float) float -> a t

To avoid adding blind as a keyword, we could use an existing one like virtual.

@vicuna
Copy link
Author

vicuna commented Nov 20, 2014

Comment author: @lpw25

I agree with Gabriel that the given type is not actually covariant. However, I think that the following type would be covariant:

type +'a t =
| String : string -> [> String] t | Int : int -> [> Int] t
| Float : float -> [> Float] t | Add : [Int] t * 'a t -> [> `Int] t

Actually, thinking about it this type is only covariant because we do not have the dual to private types (the same goes for drup's "Variation 1"), so I don't think we should support treating them as covariant.

Looks like we'll just have to wait for some kind of support for "subtyping GADTs" before we can give variance to any index parameters.

@vicuna vicuna closed this as completed May 24, 2015
@vicuna
Copy link
Author

vicuna commented May 26, 2015

Comment author: @Drup

Did you really mean to mark that "resolved" ? It's not resolved at all, merely postponed.

@vicuna
Copy link
Author

vicuna commented May 26, 2015

Comment author: @gasche

This is "resolved > suspended".

I think the problem is often ill-posed, and when it is not it is (1) rather a feature request and (2) not something that I think anyone plans to do in a reasonable future -- although you should ask Jacques, just in case.

Leo summarizes it relatively well:

Looks like we'll just have to wait for some kind of support for "subtyping GADTs" before we can give variance to any index parameters.

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