Re: [Caml-list] Adding Dimensions to types

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

> 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