Re: [Caml-list] Subtyping of phantom GADT indices?

[Oleg <oleg@okmij.org>]

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.