Conditionals based on phantom types

Conditionals based on phantom types

[Joseph Young]

Hi,
 	Is there any way to write a conditional based on the type 
information of a value?  Specifically, if we use phantom types to write a 
module such as

module 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 'a t = float
     let to_feet x=x
     let to_meters x=x
     let add x y = x +. y
     let print x = Printf.printf "%f (units)" x
end;;

is there anyway to modify the print statement to correctly denote which 
units are used?

 	Thanks.

Joe

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

[Lukasz Stafiniak]

You can index values by types, i.e. store the units with the floats in
the values. Otherwise, types are erased and not accessible.

module 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 'a t = 'a * float
   let to_feet x= `Feet, x
   let to_meters x= `Meters, x
   let add (_,x) (_,y) = x +. y
   let print (u,x) = Printf.printf "%f %s" x (to_string u)
end;;


On Mon, Aug 2, 2010 at 9:07 AM, Joseph Young <ocaml@optimojoe.com> wrote:
> Hi,
>        Is there any way to write a conditional based on the type information
> of a value?  Specifically, if we use phantom types to write a module such as
>
> module Units : sig
[...]

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

[bluestorm]

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.

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

[Joseph Young]

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

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

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

[Joseph Young]

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

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

[bluestorm]

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)

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

[Goswin von Brederlow]

Joseph Young <ocaml@optimojoe.com> writes:

> Hi,
> 	Is there any way to write a conditional based on the type
> information of a value?  Specifically, if we use phantom types to
> write a module such as

No, there is no way to write a conditional based on the type
information. In trivial cases the hypothetical conditional could be
evaluated by the compiler but only in trivial cases. The more complex
cases would require a runtime evaluation of the type and the type
information simply isn't there at runtime to do this.

> module 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 'a t = float
>     let to_feet x=x
>     let to_meters x=x
>     let add x y = x +. y
>     let print x = Printf.printf "%f (units)" x
> end;;
>
> is there anyway to modify the print statement to correctly denote
> which units are used?
>
> 	Thanks.
>
> Joe

Instead of a phantom type use a real type. See other mails for examples.

MfG
        Goswin

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

[Goswin von Brederlow]

bluestorm <bluestorm.dylc@gmail.com> writes:

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

I tend to hide the phantom tpyes in a submodule with just the bare
minimum of function (creation and access) included and then use the
submodule in the actual module. That way the phantom types are verified
in the actual module too. Instead of assertion failures at runtie you
get compiler errors.

MfG
        Goswin

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

[Joseph Young]

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