Phantom types and polymorphic variants

Phantom types and polymorphic variants

[Daniel Bünzli]

Hello,

Suppose I have the following (well-typed) definitions

> type tool = [`Spoon | `Fork]
>
> type 'a t = unit constraint 'a = [< tool]
>
> type 'a toolspec = unit constraint 'a = [< tool]
>
> let spoon : [< tool > `Spoon ] toolspec = ()
> let fork : [< tool > `Fork ] toolspec = ()
>
> let create : ([< tool ] as 'a) -> 'a t = fun t -> ()
> let create' : ([< tool ] as 'a) toolspec -> 'a t = fun t -> ()

I don't really understand why the type of the value returned by create 
and create' differ :

> # create `Spoon;;
> - : [< Test.tool > `Spoon ] Test.t = ()
> # create' spoon;;
> - : [< Test.tool ] Test.t = ()

I expected the second value to have the same type as the first.

Thanks for your explanations,

Daniel

Re: [Caml-list] Phantom types and polymorphic variants

[Jacques Garrigue]

From: Daniel Bünzli <daniel.buenzli@epfl.ch>

> Suppose I have the following (well-typed) definitions
> 
> > type tool = [`Spoon | `Fork]
> >
> > type 'a t = unit constraint 'a = [< tool]
> >
> > type 'a toolspec = unit constraint 'a = [< tool]
> >
> > let spoon : [< tool > `Spoon ] toolspec = ()
> > let fork : [< tool > `Fork ] toolspec = ()
> >
> > let create : ([< tool ] as 'a) -> 'a t = fun t -> ()
> > let create' : ([< tool ] as 'a) toolspec -> 'a t = fun t -> ()
> 
> I don't really understand why the type of the value returned by create 
> and create' differ :
> 
> > # create `Spoon;;
> > - : [< Test.tool > `Spoon ] Test.t = ()
> > # create' spoon;;
> > - : [< Test.tool ] Test.t = ()
> 
> I expected the second value to have the same type as the first.

The problem is that what you define here is not a phantom type.
To behave properly, phantom types must be abstract types (or, in ocaml
3.09, private types).
In particular, if they are simple type abbreviations, the type checker
will expand them before unification, and the parameters will never be
unified. This is why you get the type you gave as annotation, and
nothing more.
Even with normal sum types, unification would work, but variance
information  would allow to change the parameter through coercions,
making it useless as phantom type.

Jacques Garrigue