[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-05-17 (16:37) |
From: | Goswin von Brederlow <goswin-v-b@w...> |
Subject: | Re: [Caml-list] Phantom types |
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