[Caml-list] Adding Dimensions to types

[Roberto Di Cosmo <roberto@dicosmo.org>]

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