Re: [Caml-list] phantom type

[Jiten Pathy <jpathy@fssrv.net>]

It seems this encoding using first-class modules has overheads in the
interpreter(due to the functor), whereas the gadt implementation would
have no overheads.

On Mon, Apr 27, 2015 at 4:51 AM, Stephen Dolan
<stephen.dolan@cl.cam.ac.uk> wrote:
> 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