Playing with OCaml GADTs

nel.ml

type z
type 'a s

(* Sadly enough, without kind restrictions, this still allows nonsense types like *)
type nonsense = int s
(* GHC 7.6 supports this (lifting types to kinds & kind constraints) ;-) *)

type (_, _) llist =
  | Nil : (z, 'a) llist
  | Cons : ('a * ('l, 'a) llist) -> ('l s, 'a) llist

type more_nonsense = (unit, int) llist
type final_nonsense = (float s, int) llist

(* 'take_any' takes 'llist's of any length *)
let take_any : type l. (l, 'a) llist -> unit = fun _ -> ()
(* 'take_non_empty' takes 'llist's of any non-zero length *)
let take_non_empty : type l. (l s, 'a) llist -> unit = fun _ -> ()
(* 'take_at_least_2' take 'llist's of at least 2 elements *)
let take_at_least_2 : type l. ((l s) s, 'a) llist -> unit = fun _ -> ()

(* 'map' is length-preserving *)
let map : type l. ('a -> 'b) -> (l, 'a) llist -> (l, 'b) llist = fun f l ->
  let rec loop : type l. (l, 'a) llist -> (l, 'b) llist = function
    | Nil -> Nil
    | Cons (x, xs) -> Cons (f x, loop xs)
  in
  loop l

(* The 'tail' operation takes an 'llist' of at least one item, and returns an
 * 'llist' of one item less
 *)
let tail : type l. (l s, 'a) llist -> (l, 'a) llist = function
  | Cons (_, xs) -> xs
(* Notice the compiler correctly doesn't warn about a missing pattern match for
 * 'Nil'. What's more: we can't even write one at all! *)

(* Similar, 'head' only works on at-least-one-item lists *)
let head : type l. (l s, 'a) llist -> 'a = function
  | Cons (x, _) -> x


(* It would be nice to be able to define an 'append' function which takes 2
 * lists of length l1 and l2 and returns a list of length (l1 + l2), tracked at
 * type-level, but I'm not sure how to encode this in OCaml... Using Haskell/GHC
 * this would be straight-foward using a type-family, something like (OTOH):

data Z
data S a
-- Not restricting the kind of the 'a' in the S type, although that is possible
-- (and advisable) to avoid 'nonsense' types. Doesn't matter in this example
-- though.

type family Add n1 n2 :: *
type instance Add Z n2 = n2
type instance Add (S n1') n2 = S (Add n1' n2)

append :: LList l1 a -> LList l2 a -> LList (Add l1 l2) a

 * I guess this could be achieved in OCaml using modules and some 'Refl' GADT to
 * pattern-match on type equality?
 *)

let demo () =
  let _ = take_any Nil
  and _ = take_any (Cons (1, Nil))
  and _ = take_non_empty (Cons (1, Nil))
  and _ = take_at_least_2 (Cons (1, Cons (2, Cons (3, Nil))))
  and _ = take_at_least_2 (map (fun a -> a + 1) (Cons (1, Cons (2, Nil))))

  (* 'take_non_empty' doesn't like empty lists: *)

  (* and _ = take_non_empty Nil *)

  (* yields

  Error: This expression has type (z, 'a) llist
         but an expression was expected of type ('b s, 'c) llist
   *)


  (* Similarly, length information is preserved across 'map': *)
  
  (* and _ = take_at_least_2 (map (fun a -> a + 1) (Cons (1, Nil))) *)

  (* yields

  Error: This expression has type (z s, int) llist
         but an expression was expected of type ('a s s, 'b) llist 
   *)

  in ()



(* Here's a stab at 'append' *)

(* 'c = 'a + 'b *)
type ('a, 'b, 'c) add =
  | AZ : (z, 'b, 'b) add
  | AS : ('a, 'b, 'c) add -> ('a s, 'b, 'c s) add

let rec append : type l1 l2 l. (l1, l2, l) add -> (l1, 'a) llist -> (l2, 'a) llist -> (l, 'a) llist = function
  | AZ -> (function Nil -> fun l2 -> l2)
  | AS n -> (function Cons (x, xs) -> fun l2 -> Cons (x, append n xs l2))

(* But this needs a (compile-time-only, but manual) reification of the length of the first
 * list for proof purposes :-/ *)

type zero = z
type one = zero s
type two = one s
type three = two s
type four = three s
type five = four s

let _ =
  let l1 : (two, int) llist = Cons (1, Cons (2, Nil))
  and l2 : (three, int) llist = Cons (3, Cons (4, Cons (5, Nil))) in

  let proof = AS (AS AZ) in

  let l : (five, int) llist = append proof l1 l2 in

  l

+1, would really like more articles/tutorials about type-level computations in ocaml