From: Madhu
Subject: Re: study #11: type checking physical unit systems: preventing Mars Lander catastrophes
Date:
Message-ID: <m3d4xj9hn5.fsf@robolove.meer.net>
[just for kicks in the spirit of the C++ comment] :)
* Mark Tarver <························@57g2000hsv.XXXX> :
| 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.
|
Here is the standard example from KR (garnet user manual)
(create-schema 'DEGREES
(:fahrenheit
(o-formula (+ (* (gvl :celsius) 9/5) 32)
32))
(:celsius
(o-formula (* (- (gvl :fahrenheit) 32) 5/9)
0)))
(gv DEGREES :celsius) ;==> 0
(gv DEGREES :fahrenheit) ;==> 32
(setf (gv DEGREES :celsius) 20)
(gv DEGREES :fahrenheit) ;==> 68
KR supports type checking and would generate a continuable error if you
tried to store an incompatible type in the slot. However this will not
address the problem of static checking or inference which is what you
folk are after, so I won't try to extend this example by defining types.
[I (naively) understand this specific type of problem is one of
constraints and imagine type theory can be used because those systems
include a constraint solver of sorts.]
--
Regards
Madhu
| 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