Browse thread
Conditionals based on phantom types
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-08-02 (08:03) |
From: | bluestorm <bluestorm.dylc@g...> |
Subject: | Re: [Caml-list] Conditionals based on phantom types |
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.