Re: [Caml-list] phantom type

[Jiten Pathy <jpathy@fssrv.net>]

Thanks for the reference.

On Mon, Apr 27, 2015 at 3:36 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> 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.