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

[Joseph Young <ocaml@optimojoe.com>]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 3287 bytes --]

 	I appreciate the reply and the suggestions.  After looking over 
your responses, could everything be simplified by removing the phantom 
types?  In other words, is there a draw back to using the definition:

type units=[`Feet | `Meters];;
let to_feet x : [`Feet]*float=`Feet,x;;
let to_meters x : [`Meters]*float=`Meters,x;;
let add (u,x:'a*float) (_,y:'a*float) = u,x +. y;;
let unit_to_string=function
     | `Feet -> "ft"
     | `Meters -> "m"
;;
let print (u,x:[< units]*float) = Printf.printf "%f (%s)" x
 	(unit_to_string u);;

which instead of phantom types relies on polymorphic variants that contain 
only a single value?

Joe

On Mon, 2 Aug 2010, bluestorm wrote:

> 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.
>