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: | -- (:) |
| 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.