Thomas Braibant <thomas.braibant@gmail.com> writes:

> Hi list,
>
> Following on the thread "Subtyping structurally-equivalent records, or
> something like it?", I made some experimentations with phantom types.
> Unfortunately, I turns out that I do not understand the results I got.
>
> Could someone on the list explain why the first piece of code is well
> typed, while the second one is not ?
>
>
> type p1
> type p2
>
> type 'a t = float
> let x : p1 t = 0.0
> let id : p2 t -> p2 t = fun x -> x
> let _ = id x (* type checks with type p2 t*)

This is actualy a problem, at least for me. Because that is a type error
you usualy want to specifically catch through the use of phantom types.
But ocaml knows that 'a t = float and all floats are compatible. So it
accepts all 'a t as the same.

To make the phantom type checking work for you you need to move the
definition of your phantom type into a submodule and make the type
abstract through its signature. Any functions converting from one 'a t
to 'b t also need to be in there. To avoid having to use the submodule
name all the time you can use something like

module M : sig type 'a t = private float val make : float -> 'a t end = struct
  type 'a t = float
  let make f = f
end
include M

# let x : p1 t = make 0.0;;
val x : p1 t = 0.
# let id : p2 t -> p2 t = fun x -> x;;
val id : p2 t -> p2 t = <fun>
# let _ = id x;;
Error: This expression has type p1 t = p1 M.t
       but an expression was expected of type p2 t = p2 M.t

The "private" tells the type system that nobody (outside the module) is
to create a value of that type. Only inside the module, where the type
isn't private can you create one.

> type 'a t = {l: float}
> let x : p1 t = {l = 0.0}
> let id : p2 t -> p2 t = fun x -> x
> let _ = id x (* ill typed *)

Why it works correctly here is explained nicely in the other mailss in
this thread.

> Any thoughts ?
>
> thomas

MfG
        Goswin