Skip to content

Instantly share code, notes, and snippets.

@NicolasT
Last active May 28, 2019 18:48
Show Gist options
  • Save NicolasT/5373649 to your computer and use it in GitHub Desktop.
Save NicolasT/5373649 to your computer and use it in GitHub Desktop.
Playing with OCaml GADTs
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
@olleharstedt
Copy link

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment