Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Oleg <oleg@okmij.org>]

> What I'm unsure of is how this generalizes to additional functions on
> expressions. For instance, suppose I also wanted to define a function
> which computed the set of int literals that appear in the (unreduced)
> expression?  ... 
> More pressingly, I think, is what operations such as `map_ints : (int
> -> int) -> 'a exp -> 'a exp` would look like.

Frankly speaking, after re-reading the message I sent back in June, I
found it rather confusing. It didn't say what the main idea was and
the talk about Reducer was too long and unenlightening. Luckily, this
time I have your excellent questions, and so get another chance to
explain the approach, hopefully better.

The basic set up is a little language with int, float and string
literals, and the addition operation. The user should be able to add
(and keep adding) ints and floats, but attempting to add strings
should raise a clear error message. The language expressions should be
first-class, that is, we should be able to put them into a list, among
other things. (I too find Francois' example superb, but I already had
the code for the earlier example).

Here is the definition of the language: its operations. The type
parameter of t enforces the constraint: ints and floats can be
(recursively) added in any combination but strings may not.

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

Here are sample expressions:

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
                ^^
  Error: This expression has type [> `float | `int | `string ] t list
       but an expression was expected of type [ `float | `int ] t list
       The second variant type does not allow tag(s) `string
  *)
end

One doesn't have to use the functor as I just did. First-class modules,
or even records/objects will work too.

It is useful to see the expressions. Hence the first implementation of
the signature exp:

module Show : (exp with type 'a t = string) = struct
   type 'a t = string
   let int      = string_of_int 
   let float    = string_of_float
   let string x = "\"" ^ String.escaped x ^ "\""
   let add x y  = Printf.sprintf "Add(%s,%s)" x y
end

Here is how the sample expressions look like:

let _ = let module M = Ex1(Show) in M.l1
(* - : string list = ["1"; "2."; "Add(Add(3,1.),4)"] *)
let _ = let module M = Ex1(Show) in M.l2
(* - : string list = ["\"str\""; "1"; "2."; "Add(Add(3,1.),4)"] *)
let _ = let module M = Ex1(Show) in M.l1v
(* - : string = "Add(Add(Add(0,1),2.),Add(Add(3,1.),4))" *)

Now, to your questions.

``suppose I also wanted to define a function which computed the set of
int literals that appear in the (unreduced) expression?''

That is easy: we just interpret the same expressions in a different
way: instead of showing them, we compute the set of integers that occur in
their literals.

module IntSet = Set.Make(struct type t = int let compare = compare end)

module CollectInts : (exp with type 'a t = IntSet.t) = struct
   type 'a t = IntSet.t
   let int x    = IntSet.singleton x
   let float x  = IntSet.empty
   let string x = IntSet.empty
   let add x y  = IntSet.union x y
end

let _ = let module M = Ex1(CollectInts) in List.map IntSet.elements M.l1
(* - : int list list = [[1]; []; [3; 4]] *)
let _ = let module M = Ex1(CollectInts) in IntSet.elements M.l1v
(* - : int list = [0; 1; 3; 4] *)

The second question: ``More pressingly, I think, is what operations such as
`map_ints : (int -> int) -> 'a exp -> 'a exp` would look like. With an
initial style representation, this could be defined by traversing the
abstract syntax and rebuilding it with the updated `int`s.''

In tagless-final, it looks essentially like this, only simpler.
There is no need to write any traversal (a tagless-final term
itself specifies the traversal of itself)

module MapInts(Map:sig val f : int -> int end)(I:exp) = struct
   type 'a t = 'a I.t
   let int x  = I.int (Map.f x)
   let float  = I.float
   let string = I.string
   let add    = I.add
end

let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l1
(* - : string list = ["2"; "2."; "Add(Add(4,1.),5)"] *)
let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l2
(* - : string list = ["\"str\""; "2"; "2."; "Add(Add(4,1.),5)"] *)
let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l1v
(* - : string = "Add(Add(Add(1,2),2.),Add(Add(4,1.),5))" *)

The central idea is this:

        eval (map f exp) === (compose eval (map f)) exp ===
        let eval' = compose eval (map f) in eval' exp

Instead of transforming expressions we transform interpreters
(eval). Since evaluation is essentially folding, two foldings may be
fused.

I have updated
        http://okmij.org/ftp/tagless-final/subtyping.ml
to include your questions.