[Caml-list] phantom type

[Caml-list] phantom type

[Jiten Pathy]

Hello,
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? Something like following doesn't work.

type expr = Zero | Succ of expr | Iszero of expr;;
type 'a term = Expr of expr;;

(* ways to construct a term *)
let zero : int term = Expr Zero;;
let succ : int term -> int term = fun (Expr x) -> Expr (Succ x);;
let iszero : int term -> bool term = fun (Expr x) -> Expr (Iszero x);;

let rec eval : 'a.'a term -> 'a = fun (type a) (t : a term) -> match t with
| Expr Zero -> 0
| Expr (Succ e) -> eval (Expr e) + 1
| Expr (Iszero e) -> if (eval (Expr e) == 0) then true else false
;;

Re: [Caml-list] phantom type

[Jeremy Yallop]

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.

Re: [Caml-list] phantom type

[Jiten Pathy]

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.

Re: [Caml-list] phantom type

[Stephen Dolan]

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

Re: [Caml-list] phantom type

[Jiten Pathy]

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

Re: [Caml-list] phantom type

[Jeremy Yallop]

On 27 April 2015 at 13:17, Jiten Pathy <jpathy@fssrv.net> wrote:
> 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.

Have you measured it?

Re: [Caml-list] phantom type

[Jiten Pathy]

No, it was just a speculation as a new record is created for every
sub-term evaluation.

On Mon, Apr 27, 2015 at 5:30 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> On 27 April 2015 at 13:17, Jiten Pathy <jpathy@fssrv.net> wrote:
>> 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.
>
> Have you measured it?