I wonder if anyone has any suggestions on approaches to use GADTs with a type parameter that is phantom and allows subtyping. (My understanding is that the approach described in "Gabriel Scherer, Didier Rémy. GADTs meet subtyping. ESOP 2013" hasn't entirely been settled on as something that ought to be implemented in the compiler. Right? Is there anything more recent describing alternatives, concerns or limitations, etc.?) As a concrete example, consider something like: ``` type _ exp = | Integer : int -> [> `Integer] exp | Float : float -> [> `Float] exp | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp | String : string -> [> `String] exp ``` The intent here is to use polymorphic variants to represent a small (upper semi-) lattice, where basically each point corresponds to a subset of the constructors. The type definition above is admitted, but while the index types allow subtyping: ``` let widen_index x = (x : [`Integer] :> [> `Integer | `Float]) ``` this does not extend to the base type: ``` # let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);; Line 1, characters 18-67: 1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Type [ `Integer ] exp is not a subtype of ([> `Float | `Integer ] as 'a) exp The first variant type does not allow tag(s) `Float ``` This makes sense since `type _ exp` is not covariant. But trying to declare it to be covariant doesn't fly, yielding: ``` Error: In this GADT definition, the variance of some parameter cannot be checked ``` I'm not wedded to using polymorphic variants here, but I have essentially the same trouble using a hierarchy of class types (with different sets of `unit` methods to induce the intended subtype relation) to express the index lattice. Are there other options? I also tried using trunk's injectivity annotations (`type +!_ exp = ...`) on a lark since I'm not confident that I fully understand what happens to the anonymous type variables for the rows in the polymorphic variants. But that doesn't seem to change things. Is this sort of use case something for which there are known encodings? In a way I'm trying to benefit from some of the advantages of polymorphic variants (subtyping) without the drawbacks such as weaker exhaustiveness and less compact memory representation by keeping the polymorphic variants in a phantom index. Is this approach doomed? Cheers, Josh

Josh Berdine has posed a problem: > As a concrete example, consider something like: > ``` > type _ exp = > | Integer : int -> [> `Integer] exp > | Float : float -> [> `Float] exp > | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp > | String : string -> [> `String] exp > ``` > The intent here is to use polymorphic variants to represent a small > (upper semi-) lattice, where basically each point corresponds to a > subset of the constructors. The type definition above is admitted, but > while the index types allow subtyping ... > this does not extend to the base type: > ``` > # let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);; > Line 1, characters 18-67: > 1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);; > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > Error: Type [ `Integer ] exp is not a subtype of > ([> `Float | `Integer ] as 'a) exp > The first variant type does not allow tag(s) `Float > ``` > This makes sense since `type _ exp` is not covariant. But trying to > declare it to be covariant doesn't fly, yielding: > ``` > Error: In this GADT definition, the variance of some parameter > cannot be checked > ``` We demonstrate three solutions to this problem. The first has an imperfection, but is easier to explain. The second removes the imperfection. The third one is verbose, but requires the least of language features and can be implemented in SML or perhaps even Java. All three solutions give the end user the same static guarantees, statically preventing building of senseless expressions. All three rely on the tagless-final style, in effect viewing the problem as a language design problem -- designing a DSL with subtyping. It has been my experience that the tagless-final, algebraic point of view typically requires less fancy typing. Incidentally, the third solution, of explicit coercions, can be combined with GADTs and is hence the general solution to the posed problem, showing how to do phantom index subtyping with GADTs. Presenting all three solutions is too long for a message, so one should look at the complete code with many comments: http://okmij.org/ftp/tagless-final/subtyping.ml Below is the outline of the first solution, the easiest to explain. (The others just add slight variations; the main example looks almost the same in all three). We will think of the problem as a DSL with subtyping. Let's define its syntax and the type system, as an OCaml signature: module type exp = sig type +'a t val int : int -> [> `int] t val float : float -> [> `float] t val add : ([< `int | `float] as 'n) t -> 'n t -> [> `int | `float] t val string : string -> [> `string] t end The language expressions are indexed with a subset of tags `int, `float, `string. The language has the obvious subtyping: [> `int] can be weakened to [> `int | `float]. This weakening, and general typechecking of our DSL is performed by OCaml's type checker for us. Let's see an example module Ex1(I:exp) = struct open I (* We can put expressions of different sorts into the same list *) let l1 = [int 1; float 2.0; add (add (int 3) (float 1.0)) (int 4)] (* val l1 : [> `float | `int ] I.t list *) let l2 = string "str" :: l1 (* val l2 : [> `float | `int | `string ] I.t list *) (* An attempt to build an invalid expression fails, with a good error message: let x = add (int 1) (string "s") ^^^^^^^^^^^^ Error: This expression has type [> `string ] t but an expression was expected of type [< `float | `int > `int ] t The second variant type does not allow tag(s) `string *) (* We can define a function to sum up elements of a list of expressions, returning a single expression with addition *) let rec sum l = List.fold_left add (int 0) l (* val sum : [ `float | `int ] I.t list -> [ `float | `int ] I.t *) (* We can sum up l1 *) let l1v = sum l1 (* val l1v : [ `float | `int ] I.t *) (* but, predictably, not l2 let l2v = sum l2 *) end Now, what we can do with the expressions? We can print/show them module Show : (exp with type 'a t = string) = struct type 'a t = string ... elided ... end let _ = let module M = Ex1(Show) in M.l1 (* - : string list = ["1"; "2."; "Add(Add(3,1.),4)"] *) We can also reduce them. The following is the reducer -- although in reality it does the normalization-by-evaluation (NBE) A subset of expressions: values module type vals = sig type +'a t val int : int -> [> `int] t val float : float -> [> `float] t val string : string -> [> `string] t end module Reducer(I:vals) : (sig include exp val observe : ([> `float | `int ] as 'a) t -> 'a I.t end) = struct type 'a t = Unk of 'a I.t | Int of int | Float of float let observe = function | Unk x -> x | Int x -> I.int x | Float x -> I.float x let int x = Int x let float x = Float x let string x = Unk (I.string x) let add x y = match (x,y) with | (Int x, Int y) -> Int (x+y) | (Float x, Float y) -> Float (x+.y) | (Int x, Float y) | (Float y, Int x) -> Float (float_of_int x +. y) (* This is the imperfection. We know that the case cannot happen, but this is not clear from the type system. We should stress that this imperfection does not compromise the guarantees offered to the end user, who never sees the internals of Reducer, and can't even access them. *) | _ -> assert false end (* We can now evaluate exp to values. We need a way to show them though. Luckily, exp is a superset of values, and we already wrote the show interpreter for exp *) let _ = let module I = Reducer(Show) in let module M = Ex1(I) in List.map I.observe M.l1 (* - : string list = ["1"; "2."; "8."] *) The second solutions removes the imperfection in Reduce, making Reduce.add total, by making the types more phantom. The third solution does the obvious thing: implementing subtyping using explicit coercions. In the given example, it doesn't add too much annoyance to the user. It does however remove the reliance on variance and so is applicable to GADTs in general. One can imagine more solutions along the shown lines.