[Caml-list] Adding Dimensions to types

[Caml-list] Adding Dimensions to types

[Roberto Di Cosmo]

[-- Attachment #1: Type: text/plain, Size: 2365 bytes --]

Dear friends OCamlers,
    in a meeting yesterday I had the occasion to listen to a talk by
Frederic Boniol (search for his name in the proceedings below [1]), who
went through some considerable gymnastics to add dimension checking to the
Lustre programming language.

This is work that was quite well pioneered some 20 years ago by Mitch Wand,
Andrew Kennedy and Jean Goubault
for our beloved ML paradigm, and you can still find on Bruno Blanchet's web
page [2] a fully functional version of Caml-light extended to add
dimensions, and you can play with it. More recently, you can find support
for physical dimensions incorporated into F# [3].

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

-- 
Roberto

P.S.: yes, we know that you can somehow play tricks with phantom types to
distinguish a meter from a foot, but checking dimensions is more tricky
than that, consider the issue at stake when you multiply or divide
quantities involving multiple dimensions (like computing an acceleration,
or an energy).

[1] http://afadl2014.lacl.fr/actes_AFADL2014-HAL.pdf
[2] http://prosecco.gforge.inria.fr/personal/bblanche/cldim.html
[3]
http://blogs.msdn.com/b/andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducing-units.aspx

------------------------------------------------------------------
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 320 (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

[-- Attachment #2: Type: text/html, Size: 3451 bytes --]

Re: [Caml-list] Adding Dimensions to types

[David MENTRE]

Hello,

Le 13/06/2014 11:10, Roberto Di Cosmo a écrit :
> More recently, you can find support for physical dimensions incorporated
> into F# [3].

Also in Ada 2012 
(http://www.adacore.com/adaanswers/gems/gem-136-how-tall-is-a-kilogram/) 
or even in some extensions to C (http://mbeddr.com/).

> 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

I am also interested in the answer.

Sincerely yours,
david

Re: [Caml-list] Adding Dimensions to types

[Roberto Di Cosmo]

Thanks David for these pointers!

On Fri, Jun 13, 2014 at 11:42:14AM +0200, David MENTRE wrote:
> Hello,
> 
> Le 13/06/2014 11:10, Roberto Di Cosmo a écrit :
> >More recently, you can find support for physical dimensions incorporated
> >into F# [3].
> 
> Also in Ada 2012
> (http://www.adacore.com/adaanswers/gems/gem-136-how-tall-is-a-kilogram/) or
> even in some extensions to C (http://mbeddr.com/).
> 
> >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
> 
> I am also interested in the answer.
> 
> Sincerely yours,
> david
> 
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

Re: [Caml-list] Adding Dimensions to types

[Gabriel Scherer]

Encoding integers with addition at the type level is easy enough (it
is possible to use a technique akin to difference list where you keep
unary numbers with a unification variable at their tail, to get the
unification engine to do the addition for you). Anything below that,
in particular substraction, cannot be done *conveniently* in the
type-system. It is possible to encode arbitrary operation on
type-level numbers (unary or not), expressed relationally
(Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+'b='c) by a GADT
witnessing the relation, but actually building and using these
operations then requires the programmer to provide those witness terms
that are manipulated at runtime.

This could possibly be hidden under a layer of syntactic sugar; to
generate the correct witness terms, you however need access to the
typing environment or approximate it, so it's hard to do at the
camlp4-ppx layer, and you rather need .cmt-level processing; in fact
the new presentation of formats as GADTs does exactly this). However,
the runtime costs of witness manipulation could be prohibitive for
numerical computations.

I suspect that if for some reason people were to absolutely need this
feature, the easiest path would probably be to extend the type-checker
with support for this. So far, it seems that nobody was interested
enough in this to do the (important) amount of work necessary.

On Fri, Jun 13, 2014 at 11:10 AM, Roberto Di Cosmo <roberto@dicosmo.org> wrote:
> Dear friends OCamlers,
>     in a meeting yesterday I had the occasion to listen to a talk by
> Frederic Boniol (search for his name in the proceedings below [1]), who went
> through some considerable gymnastics to add dimension checking to the Lustre
> programming language.
>
> This is work that was quite well pioneered some 20 years ago by Mitch Wand,
> Andrew Kennedy and Jean Goubault
> for our beloved ML paradigm, and you can still find on Bruno Blanchet's web
> page [2] a fully functional version of Caml-light extended to add
> dimensions, and you can play with it. More recently, you can find support
> for physical dimensions incorporated into F# [3].
>
> 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 :-)
>
> --
> Roberto
>
> P.S.: yes, we know that you can somehow play tricks with phantom types to
> distinguish a meter from a foot, but checking dimensions is more tricky than
> that, consider the issue at stake when you multiply or divide quantities
> involving multiple dimensions (like computing an acceleration, or an
> energy).
>
> [1] http://afadl2014.lacl.fr/actes_AFADL2014-HAL.pdf
> [2] http://prosecco.gforge.inria.fr/personal/bblanche/cldim.html
> [3]
> http://blogs.msdn.com/b/andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducing-units.aspx
>
> ------------------------------------------------------------------
> 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 320 (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

Re: [Caml-list] Adding Dimensions to types

[Roberto Di Cosmo]

On Fri, Jun 13, 2014 at 11:43:20AM +0200, Gabriel Scherer wrote:
> Encoding integers with addition at the type level is easy enough (it
> is possible to use a technique akin to difference list where you keep
> unary numbers with a unification variable at their tail, to get the
> unification engine to do the addition for you). Anything below that,
> in particular substraction, cannot be done *conveniently* in the
> type-system. It is possible to encode arbitrary operation on
> type-level numbers (unary or not), expressed relationally
> (Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+'b='c) by a GADT
> witnessing the relation, but actually building and using these
> operations then requires the programmer to provide those witness terms
> that are manipulated at runtime.

Actually, we want to have dimension checking at compile time, with no
trace of it at runtime.

> This could possibly be hidden under a layer of syntactic sugar; to
> generate the correct witness terms, you however need access to the
> typing environment or approximate it, so it's hard to do at the
> camlp4-ppx layer, and you rather need .cmt-level processing; in fact
> the new presentation of formats as GADTs does exactly this). However,
> the runtime costs of witness manipulation could be prohibitive for
> numerical computations.
> 
> I suspect that if for some reason people were to absolutely need this
> feature, the easiest path would probably be to extend the type-checker
> with support for this. So far, it seems that nobody was interested
> enough in this to do the (important) amount of work necessary.

It seems that there is now a more general interest in this idea, and
I wonder how important this amount of work is... in Bruno's memoire
there is a detailed explanation of the changes, which seem kind of
well isolated, but that was for Caml-Light of course.


> On Fri, Jun 13, 2014 at 11:10 AM, Roberto Di Cosmo <roberto@dicosmo.org> wrote:
> > Dear friends OCamlers,
> >     in a meeting yesterday I had the occasion to listen to a talk by
> > Frederic Boniol (search for his name in the proceedings below [1]), who went
> > through some considerable gymnastics to add dimension checking to the Lustre
> > programming language.
> >
> > This is work that was quite well pioneered some 20 years ago by Mitch Wand,
> > Andrew Kennedy and Jean Goubault
> > for our beloved ML paradigm, and you can still find on Bruno Blanchet's web
> > page [2] a fully functional version of Caml-light extended to add
> > dimensions, and you can play with it. More recently, you can find support
> > for physical dimensions incorporated into F# [3].
> >
> > 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 :-)
> >
> > --
> > Roberto
> >
> > P.S.: yes, we know that you can somehow play tricks with phantom types to
> > distinguish a meter from a foot, but checking dimensions is more tricky than
> > that, consider the issue at stake when you multiply or divide quantities
> > involving multiple dimensions (like computing an acceleration, or an
> > energy).
> >
> > [1] http://afadl2014.lacl.fr/actes_AFADL2014-HAL.pdf
> > [2] http://prosecco.gforge.inria.fr/personal/bblanche/cldim.html
> > [3]
> > http://blogs.msdn.com/b/andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducing-units.aspx
> >
> > ------------------------------------------------------------------
> > 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 320 (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

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

Re: [Caml-list] Adding Dimensions to types

[Nicolas Boulay]

[-- Attachment #1: Type: text/plain, Size: 1547 bytes --]

2014-06-13 11:54 GMT+02:00 Roberto Di Cosmo <roberto@dicosmo.org>:

> On Fri, Jun 13, 2014 at 11:43:20AM +0200, Gabriel Scherer wrote:
> > Encoding integers with addition at the type level is easy enough (it
> > is possible to use a technique akin to difference list where you keep
> > unary numbers with a unification variable at their tail, to get the
> > unification engine to do the addition for you). Anything below that,
> > in particular substraction, cannot be done *conveniently* in the
> > type-system. It is possible to encode arbitrary operation on
> > type-level numbers (unary or not), expressed relationally
> > (Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+'b='c) by a GADT
> > witnessing the relation, but actually building and using these
> > operations then requires the programmer to provide those witness terms
> > that are manipulated at runtime.
>
> Actually, we want to have dimension checking at compile time, with no
> trace of it at runtime.
>

Is it possible to think with dimension inference ? This avoid the need to
give dimension everywhere.

You can have rules like
if "a + b = c" => dim(a) == dim(b) == dim(c).
if(e*f=g) => dim(g) = dim(e) * dim(f)

You can even go further. https://en.wikipedia.org/wiki/Dimensional_analysis
gives some hint :  Position vs displacement.

if T1 and T2 are absolut point in time, (T1-T2) are time offset. But "T1 +
T2"  is a none sense.

You could also extend the check of dimension in space direction (x,y,z).

The idea is to add a check with minimum new user input.

Nicolas

[-- Attachment #2: Type: text/html, Size: 2448 bytes --]

Re: [Caml-list] Adding Dimensions to types

[Leo White]

> 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

Re: [Caml-list] Adding Dimensions to types

[Roberto Di Cosmo]

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                        

Re: [Caml-list] Adding Dimensions to types

[Leo White]

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

Correct.

Regards,

Leo

Re: [Caml-list] Adding Dimensions to types

[Török Edwin]

On 06/13/2014 12:52 PM, 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

For some more information on how this works I found these presentations useful:
http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf
http://homepages.inf.ed.ac.uk/slindley/papers/many-holes.pdf

With your representation '('a,'b) quantity' could be thought of as representing
quantity ** ('b - 'a), or quantity ** 'b / (quantity ** 'a).

I think it still works if you use ('a * 'b) instead of ('a, 'b), so then one could
write SI units using something like (maybe with an 8th unit for scale):
  val of_float: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t
  val m: float -> ('metre * 'metre s, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t
  val kg: float -> ('a * 'a s, 'kilogram * 'kilogram s, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t
  val s: float -> ('a * 'a, 'b * 'b, 'second * 'second s, 'd * 'd, 'e * 'e, 'f * 'f, 'g* 'g) t
  val a: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'ampere * 'ampere s, 'e * 'e, 'f * 'f, 'g* 'g) t
  val k: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'kelvin * 'kelvin s, 'f * 'f, 'g* 'g) t
  val mol: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'mole * 'mole s, 'g* 'g) t
  val cd: float -> ('a * 'a, 'b * 'b, 'c * 'c, 'd * 'd, 'e * 'e, 'f * 'f,'candela * 'candela s) t

The error messages might get hard to understand at some point though, although that might be
solved by pretty-printing / post-processing the compiler's error message somehow.

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

That is interesting, but I'm worried that if for something as simple as x^2 you need to write that
how would it look like when you need to write the type for a real equation?

Best regards,
--Edwin