Re: [Caml-list] Conditionals based on phantom types

[bluestorm <bluestorm.dylc@gmail.com>]

Two remarks on Lukasz suggestion :

>   val add : 'a t -> 'a t -> 'a t
>   [..]
>   let add (_,x) (_,y) = x +. y

This does not typecheck. I suggest the following :

let add (ux, x) (uy, y) =
  assert (ux = uy);
  (ux, x +. y)

While the assertion does not seem necessary at first (correct units
are guaranteed by typing !), it may be helpful in case of bug inside
the Units module or signature, wich breaks the typing invariant. If
you're planning to do relatively elaborate things inside the Units, I
strongly recommend to use any kind of dynamic checking available, at
least during development. This is something is understood late in my
own phantom-type project (Macaque), and would have been very useful
for debugging.



On Mon, Aug 2, 2010 at 9:49 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
>   val print : 'a t -> unit
>   [..]
>   type 'a t = 'a * float
>   let print (u,x) = Printf.printf "%f %s" x (to_string u)

Lukasz doesn't give a to_string function. Assuming this one, there is
a typing problem here.

  let to_string = function
    | `Feet -> "feet"
    | `Meters -> "meters"

Values do not match:
   val print : [< `Feet | `Meters ] * float -> unit
is not included in
    val print : 'a t -> unit

The issue is that, with Lukasz definition, 'a is now coupled to the
concrete values (type 'a t = 'a * float), and the to_string function
is *not* polymorphic in 'a as advertised by the interface. I see two
solutions :

1) restrict print to only print the units you directly support :

  val print : [ `Feet | `Meters ] * float -> unit

2) make 'a a phantom type parameter again by decoupling the type
information (the polymoprhic variant) and the runtime information
(another, value-level, variant) :

odule Units : sig
   type 'a t
   val to_feet : float -> [`Feet ] t
   val to_meters : float -> [`Meters] t
   val add : 'a t -> 'a t -> 'a t
   val print : 'a t -> unit
end = struct
   type unit = Feet | Meters
   let string_of_unit = function
     | Feet -> "feet"
     | Meters -> "meters"

   type 'a t = unit * float

   let to_feet x = Feet, x
   let to_meters x = Meters, x

   let add (ux, x) (uy, y) =
     assert (ux = uy);
     (ux, x +. y)

   let print (u, x) =
     Printf.printf "%f (%s)" x (string_of_unit u)
end;;

I would rather go the second way, wich allows for more flexibility in
what runtime informations keep, and what type information you expose.