Re: [Caml-list] Adding Dimensions to types

["Török Edwin" <edwin+ml-ocaml@etorok.net>]

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