Re: [Caml-list] Phantom types

[Jon Harrop <jon@jdh30.plus.com>]

On Saturday 31 July 2004 17:31, Markus Mottl wrote:
> module type PHANTOM_INT = sig
>   type 'p t
> ...

Right, I've had a bit more of a chance to play with phantom types now, and I'm 
quite confused. :-)

As far as I can tell, there were a few errors in Markus' original (I may well 
be wrong, of course), so here is my altered version:

module PhantomInt : sig
  type 'p t
	
  val add : 'p t -> 'p t -> 'p t
      
  val add_even_even : [ `Even ] t -> [ `Even ] t -> [ `Even ] t
  val add_even_odd : [ `Even ] t -> [ `Odd ] t -> [ `Odd ] t
  val add_odd_even : [ `Odd ] t -> [ `Even ] t -> [ `Odd ] t
  val add_odd_odd : [ `Odd ] t -> [ `Odd ] t -> [ `Even ] t
  val neg : 'a t -> 'a t
  val make_even : int -> [ `Even ] t
  val make_odd : int -> [ `Odd ] t
end = struct
  type 'p t = int
	
  let add = (+)
  let add_even_even = add
  let add_even_odd = add
  let add_odd_even = add
  let add_odd_odd = add
  let neg n = -n
  let make_even n = if n mod 2 = 0 then n else failwith "not even"
  let make_odd n = if n mod 2 <> 0 then n else failwith "not odd"
end;;

So I've changed the types to be [ `Even ] instead of [> `Even ] and the "make" 
functions to be "int -> ...". This appear to work as desired:

# let i = PhantomInt.make_even 2;;
val i : [ `Even ] PhantomInt.t = <abstr>
# let j = PhantomInt.make_odd 3;;
val j : [ `Odd ] PhantomInt.t = <abstr>
# PhantomInt.add_even_odd i j;;
- : [ `Odd ] PhantomInt.t = <abstr>
# PhantomInt.add_even_even i j;;
This expression has type [ `Odd ] PhantomInt.t but is here used with type
  [ `Even ] PhantomInt.t
These two variant types have no intersection

Now, there are some subtle peculiarities of these which I don't understand. 
Firstly, the type checking of the phantom types only seems to work if the 
type is made abstract in the module signature. I can't think why this should 
make a difference though. For example, changing "type 'p t" to "type 'p t = 
int" in "PhantomInt : sig" then allows:

# PhantomInt.add_even_even i j;;
- : [ `Even ] PhantomInt.t = 5

which is clearly undesirable.

Secondly, specifying the types as Markus did (e.g. [> `Even]), which I think 
should have been correct, leads to some kind of monomorphic type:

# PhantomInt.add_even_odd i j;;
- : _[> `Odd ] PhantomInt.t = <abstr>

Note the "_" preceding the "[> `Odd]". I'm not sure what the implications of 
this are.

Can someone explain these to me, please?

Cheers,
Jon.

PS: I'm using 3.08.0, in case that makes a difference.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners