Nice phantom type example

A nice example of phantom types:  forcing lambda terms to be closed.  
Lifted from an email from Neek Krishnaswami.


type void   (* Empty type *)

type 'a debruijn =  (* Debruijn with nested datatypes *)
 | Var of 'a
 | App of 'a debruijn * 'a debruijn
 | Lam of ('a option) debruijn

let omega : void debruijn =  (* Typechecking ensures omega has no free vars *)
 App(Lam(App(Var None, Var None)), Lam(App(Var None, Var None)))


Note that a free variable, for instance, Var None : void option debruijn.  
Neel used the example to describe a polymorphic recursion workaround in ocaml.


(* Suppose we want a size function...

let rec size = function
 | Var _ -> 1
 | App(e,e') -> 1 + size e + size e'
 | Lam e -> 1 + size e

This won't typecheck, we need polymorphic recursion!
*)

(* Caml allows polymorphic record fields, so declare one with the
polymorphism
  we want in debruijn. *)

type 'b sizerec = {fn: 'a. ('a debruijn -> 'b)}

(* Now we can define a recursive function by going through this record *)

let size =
 let rec s =
   {fn = function
      | Var _ -> 1
      | App(e,e') -> 1 + s.fn e + s.fn e'
      | Lam e -> 1 + s.fn e}
 in
 s.fn