[Caml-list] GADT example for universal list

[Goswin von Brederlow <goswin-v-b@web.de>]

Hi,

I played some more with GADTs, this time with an universal list. Well,
not truely universal as you can't store arbitrary types. Only Int and
Float are allowed here:

type _ kind = (* used for searching in the list *)
  | Int_kind : int kind
  | Float_kind : float kind

type value = (* box the values so we have runtime type information *)
  | Int of int
  | Float of float

type list = (* the universal list *)
  | Nil : list
  | Cons : value * list -> list

(* find the first value in the list of a given kind *)
let rec get : type a . list -> a kind -> a = fun l k ->
  match (k, l) with
    | (_, Nil) -> raise Not_found
    | (Int_kind, Cons (Int x, xs)) -> x
    | (Float_kind, Cons (Float x, xs)) -> x
    | (_, Cons (_, xs)) -> get xs k

(* print out list *)
let rec print = function
  | Nil -> print_newline ()
  | Cons ((Int x), xs) -> Printf.printf "%d " x; print xs
  | Cons ((Float x), xs) -> Printf.printf "%f " x; print xs

(* testing *)
let empty = Nil
let l1 = Cons ((Int 1), empty)
let l2 = Cons ((Float 2.), l1)
let () = print l2
let i = get l2 Int_kind
let f = get l2 Float_kind;;

(*
                                                          2.000000 1 
type _ kind = Int_kind : int kind | Float_kind : float kind
type value = Int of int | Float of float
type list = Nil : list | Cons : value * list -> list
val get : list -> 'a kind -> 'a = <fun>
val print : list -> unit = <fun>
val empty : list = Nil
val l1 : list = Cons (Int 1, Nil)
val l2 : list = Cons (Float 2., Cons (Int 1, Nil))
val i : int = 1
val f : float = 2.
*)

At first glance you might think: Why does that need GADTs? Why not
simply use 

    type value = Int of int | Float of float

for this?


Take a close look at the get funktion:

    val get : list -> 'a kind -> 'a = <fun>

It does not return a value but directly the unboxed type. Because the
value is unboxed you can directly use it and ocaml will detect if you
screw up the type like in:

    let () = Printf.printf "%d\n" (get l2 Float_kind);;
    Error: This expression has type float but an expression was expected
           of type int

MfG
        Goswin