| Mark Tarver 2007-08-19, 8:04 am |
| I got this message as email; the body quoted is taken from a
comp.lang.functional post. The poster asked if I had written anything
relevant.
QUOTE
I'm after a general recipe how to design a set of types that are
incompatible (to prevent accidental mixup) but are more-or-less
automagically converted between each other. I don't care too much
about the concrete language.
Example 1: Physical unit systems.
E.g. temperature. You can have Kelvin, degrees Fahrenheit, and
degrees Celsius.
I'd like to pass a temperature to a function and have somebody
(system, function itself, whatever) automagically convert the
temperature to the type that the function's logic expects.
Similar issues exist for other unit systems. There's even a famous
failed Mars mission where software modules didn't interoperate
properly because one used metric and the other used nonmetric length
units.
UNQUOTE
I did in fact have such a paper which I wrote in 2006 and never got to
finishing. But having a couple of days spare I finished it while my
current guest was busy I filled in the spaces.
The paper deals with the construction of type systems designed for
safety-critical engineering applications like the Mars Lander
project.
The material described in that paper overlap with the goals of the Sun
Fortress project. It requires some type theory well beyond that
current in ML, O'Caml or Haskell, but there is a working program
demoed in Qi that juggles two different unit systems and you can
download it from that paper.
This is the title page of a new science so I've written DRAFT on it;
reflecting not only the limited time I have spent on it but also the
possible size of the task. The page is
http://www.lambdassociates.org/studies/study11.htm
hope this is of use
Mark
|