Re: [Caml-list] Adding Dimensions to types

[Roberto Di Cosmo <roberto@dicosmo.org>]

Thanks Leo for this answer: basically, following your code,
if I want n dimension, I will need a phantom type with 2*n
variables, and define the units by putting a difference
in the right 'field', right?

It is not really readable, and has limitations, but it
is a nice encoding nonetheless.

On Fri, Jun 13, 2014 at 10:52:23AM +0100, Leo White wrote:
> > Now the question that arose yesterday, and that we could not answer right away, is whether it is possible to encode
> > such dymension checking in OCaml today using only the existing type-system features, so I am passing it over to the
> > list :-)
> 
> You can do something reasonable using difference lists to encode a
> dimension in a phantom type. For example, the following module (based on
> an initial version by Stephen Dolan):
> 
>     module Unit : sig
>       type +'a suc
>       type (+'a, +'b) quantity
> 
>       val of_float : float -> ('a, 'a) quantity
>       val metre : ('a, 'a suc) quantity
>       val mul : ('a, 'b) quantity -> ('b, 'c) quantity -> ('a, 'c) quantity
>       val add : ('a, 'b) quantity -> ('a, 'b) quantity -> ('a, 'b) quantity
>       val neg : ('a, 'b) quantity -> ('a, 'b) quantity
>       val inv : ('a, 'b) quantity -> ('b, 'a) quantity
>     end = struct
>       type 'a suc = unit
>       type ('a, 'b) quantity = float
>       let of_float x = x
>       let metre = 1.
>       let mul x y = x *. y
>       let add x y = x +. y
>       let neg x = 0. -. x
>       let inv x = 1. /. x
>     end
> 
> This successfully tracks the dimension of quatities:
> 
>     # open Unit;;
> 
>     # let m10 = mul (of_float 10.) metre;;
>     val m10 : ('a, 'a Unit.suc) Unit.quantity = <abstr>
> 
>     # let sum = add m10 m10;;
>     val sum : ('a, 'a Unit.suc) Unit.quantity = <abstr>
> 
>     # let sq = mul m10 m10;;
>     val sq : ('a, 'a Unit.suc Unit.suc) Unit.quantity = <abstr>
> 
>     # let cube = mul m10 (mul m10 m10);;
>     val cube : ('a, 'a Unit.suc Unit.suc Unit.suc) Unit.quantity = <abstr>
> 
>     # let _ = add (mul sq (inv cube)) (inv m10);;
>     - : ('a Unit.suc, 'a) Unit.quantity = <abstr>
> 
> and it will give errors if they are used incorrectly:
> 
>     # let _ = add sq cube;;
>     Characters 15-19:
>       let _ = add sq cube;;
>                      ^^^^
>     Error: This expression has type
>              ('a, 'a Unit.suc Unit.suc Unit.suc) Unit.quantity
>            but an expression was expected of type
>              ('a, 'a Unit.suc Unit.suc) Unit.quantity
>            The type variable 'a occurs inside 'a Unit.suc
> 
>     # let _ = add m10 (mul m10 m10);;
>     Characters 16-29:
>       let _ = add m10 (mul m10 m10);;
>                       ^^^^^^^^^^^^^
>     Error: This expression has type ('a, 'a Unit.suc Unit.suc) Unit.quantity
>            but an expression was expected of type ('a, 'a Unit.suc) Unit.quantity
>            The type variable 'a occurs inside 'a Unit.suc
> 
> However, it will infer too restrictive types for some things:
> 
>     # let sq x = mul x x;;
>     val sq : ('a, 'a) Unit.quantity -> ('a, 'a) Unit.quantity = <fun>
> 
> The "real" type of `sq` requires higher-kinded and higher-rank
> polymorphism. Using functors you can encode `sq` thus:
> 
>     # module Sq (X : sig type 'a t end) = struct
>         type arg = {x: 'a. ('a, 'a X.t) quantity}
>         let sq {x} = mul x x
>       end;;
> 
> and apply it like so:
> 
>     # module AppSq = Sq(struct type 'a t = 'a suc end);;
> 
>     # let x = AppSq.sq {AppSq.x = m10};;
>     val x : ('a, 'a Unit.suc Unit.suc) Unit.quantity = <abstr>
> 
> It is also worth noting that -rectypes breaks this encoding:
> 
>     #rectypes;;
> 
>     # let _ = add sq cube;;
>     - : ('a Unit.suc as 'a, 'a Unit.suc Unit.suc) Unit.quantity = <abstr>
> 
> 
> Regards,
> 
> Leo

-- 
Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 3020 (3rd floor)
Batiment Sophie Germain
Avenue de France
Metro Bibliotheque Francois Mitterrand, ligne 14/RER C
-----------------------------------------------------------------
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3