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