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

[Joseph Young <ocaml@optimojoe.com>]

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

On Tue, 3 Aug 2010, bluestorm wrote:

> On Tue, Aug 3, 2010 at 8:15 AM, Joseph Young <ocaml@optimojoe.com> wrote:
>> module Units : sig
>>    type t
>>    val to_feet : float -> [`Feet]*t
>>    val to_meters : float -> [`Meters]*t
>>    [..]
>> end
>
> With this type, the value representation of units is not abstract
> anymore (and it is not very useful to have still t abstract). The user
> can analyse the values you give him and access the unit member. This
> is the difference with the ('a t) representation were the relation
> between 'a and values is hidden outside the module.
>
> For example, your user can write something like that, wich could be
> indesirable :
>
> let convert [ `Feet ] * Units.t -> [ `Meters ] * Units.t =
>  function (`Feet, t) -> (`Meters, t)
>

 	You are correct and that could be problematic.  Combining the two 
ideas from above gives:

type units=[`Feet | `Meters];;
let unit_to_string=function
     | `Feet -> "ft"
     | `Meters -> "m"
;;
module Units : sig
     type 'a t
     val to_feet : float -> ([`Feet] as 'a)*'a t
     val to_meters : float -> ([`Meters] as 'a)*'a t
     val add : (([<units] as 'a)*'a t as 'b) -> 'b -> 'b
     val print : ([<units] as 'a)*'a t -> unit
end = struct
     type 'a 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

which hopefully insures that the exposed and hidden unit are required to 
be the same in order to use these functions.  To be sure, functions such 
as:

let convert (u,x:[ `Feet ] * 'a Units.t) : [ `Meters ] * 'a Units.t = 
`Meters,x

are possible.  However, I believe that the type checker should throw an 
error if the above functions are called on converted values.  Mostly, I'm 
trying to force the type checker to insure there are valid values without 
using runtime assertions as you suggested above.

 	Thanks again for the help.

Joe