Re: [Caml-list] Adding Dimensions to types

[Leo White <lpw25@cam.ac.uk>]

> 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