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

[Joseph Young <ocaml@optimojoe.com>]

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

 	I had someone point out that

add (`Meters, 0.5) (`Feet, 0.5);;

will type check by instantiating 'a as [`Feet | `Meters].  Hiding the type 
in a module may fix the example:

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

Then, expressions as the one above can not be written.

Joe

On Tue, 3 Aug 2010, Joseph Young wrote:

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