Re: [Caml-list] phantom type

[Stephen Dolan <stephen.dolan@cl.cam.ac.uk>]

To expand a little on Jeremy's answer, you can encode the expr type as
a module signature, and then pass terms around as first-class modules.

First, you make a module signature that describes the ways of
constructing a term:

    module type Ctors = sig
      type 'a term
      val zero : int term
      val succ : int term -> int term
      val iszero : int term -> bool term
    end

Next, a Term is something which can construct a term using any set of Ctors:

    module type Term = sig
      type a
      module Build : functor (C : Ctors) -> sig
        val x : a C.term
      end
    end

You can make a normal datatype from this using first-class modules:

    type 'a term = (module Term with type a = 'a)

We're jumping between the module and the core language, so the
wrapping and unwrapping makes things a bit verbose. Here's the
value-level "succ" operation, the other two are similar:

    let succ ((module T) : int term) : int term =
      (module struct
        type a = int
        module Build = functor (C : Ctors) -> struct
          module TC = T.Build (C)
          let x = C.succ TC.x
        end
      end)

Evaluation is one particular implementation of the term constructors,
which implements the type 'a term as just 'a:

    module Eval = struct
      type 'a term = 'a
      let zero = 0
      let succ n = n + 1
      let iszero n = (n = 0)
    end

Finally, you can use this evaluation module to interpret any term:

let eval (type a) ((module T) : a term) : a =
  let module M = T.Build (Eval) in M.x

Stephen