Re: [Caml-list] Adding Dimensions to types

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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