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