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
Comments
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 [ let string_is_not_add : [> `String ] t -> unit = function It is unclear to me whether:
|
Comment author: @Drup What I wrote is indeed not safe as-is. There are two variations of this type Variation 1: Variation 2: The variation 1 is sound (I think) and already more powerful than what is currently possible with GADTs currently. | Succ : [< 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 I realize this needs several things that are not possible currently, notably the ability to manipulate row variables. |
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 = and it would be nice to support this case. Similarly, I personally have types like the following:
and it would be nice to be able to define them as:
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:
Which would support code like the following:
If we had support for what Gabriel previously called "blind" types (the dual to private types) then the syntax could be something like:
To avoid adding |
Comment author: @lpw25
Actually, thinking about it this type is only covariant because we do not have the dual to 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. |
Comment author: @Drup Did you really mean to mark that "resolved" ? It's not resolved at all, merely postponed. |
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:
|
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 tI 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.
The text was updated successfully, but these errors were encountered: