Re: [Caml-list] phantom type

[Jeremy Yallop <yallop@gmail.com>]

On 27 April 2015 at 11:23, Jiten Pathy <jpathy@fssrv.net> wrote:
> Trying to use phantom types instead of gadt for well-constructed term
> example. Is it possible to define an evaluator eval : 'a term -> 'a
> using phantom types?

No, it's not really possible.  If the 'a parameter to 'term' is
phantom then 'term' is defined using some other unparameterised type
such as your 'expr':

> type expr = Zero | Succ of expr | Iszero of expr;;

and the problem comes down to writing a function of type

   expr -> 'a

which is clearly impossible.

Phantom types only really help with constraints on building or
transforming values, not with deconstructing them.

However, there are various ways of writing well-typed evaluators
without using GADTs, e.g.using a "final" encoding, which represents a
term as an evaluation function:

   Finally Tagless, Partially Evaluated:
   http://okmij.org/ftp/tagless-final/JFP.pdf

or by encoding GADTs using polymorphism:

   First-class modules: hidden power and tantalizing promises
   http://okmij.org/ftp/ML/first-class-modules/first-class-modules.pdf

Jeremy.