# study #11: type checking physical unit systems: preventing Mars Lander catastrophes - lisp

This is a discussion on study #11: type checking physical unit systems: preventing Mars Lander catastrophes - lisp ; 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 ...

1. ## study #11: type checking physical unit systems: preventing Mars Lander catastrophes

I got this message as email; the body quoted is taken from a
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

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

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

2. ## Re: study #11: type checking physical unit systems: preventing Mars Lander catastrophes

On Aug 19, 2:50 pm, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:
> I got this message as email; the body quoted is taken from a
> relevant.
> 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.

A comment from programming.reddit:

> If you want actual source code you can use for attaching real world units to numbers, and carrying
> them through the calculations, and getting compile errors on mismatches, see:
>
> http://lss.fnal.gov/archive/1998/conf/Conf-98-328.pdf
>
> "Introduction to the SILibrary of Unit-Based Computation" by WalterE. Brown

3. ## Re: study #11: type checking physical unit systems: preventing Mars Lander catastrophes

[just for kicks in the spirit of the C++ comment]

* Mark Tarver <1187524228.256269.327410@57g2000hsv.XXXX> :
| I got this message as email; the body quoted is taken from a
| 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
|
| 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

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

4. ## Re: study #11: type checking physical unit systems: preventing Mars Lander catastrophes

Emre Sevinc <emre.sevinc@gmail.com> wrote:

> On Aug 19, 2:50 pm, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:
> > 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.
> > 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.

>
> A comment from programming.reddit:
>
>
> > If you want actual source code you can use for attaching real world units to numbers, and carrying
> > them through the calculations, and getting compile errors on mismatches, see:
> >
> > http://lss.fnal.gov/archive/1998/conf/Conf-98-328.pdf
> >
> > "Introduction to the SILibrary of Unit-Based Computation" by WalterE. Brown

[cunis92] R. Cunis, ``A Package for Handling Units of Measure in Lisp'',
ACM Lisp Pointers, vol. 5, no. 2, 1992.

http://www.isi.edu/isd/LOOM/document...mentation.text
http://www.isi.edu/isd/LOOM/document...res-usage.text

http://www.cs.cmu.edu/afs/cs/project...easures/0.html

5. ## Re: study #11: type checking physical unit systems: preventing Mars Lander catastrophes

On 20 Aug, 02:48, Rainer Joswig <jos...@lisp.de> wrote:
> Emre Sevinc <emre.sev...@gmail.com> wrote:
>
>
>
>
>
> > On Aug 19, 2:50 pm, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:
> > > 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.
> > > 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.

>
> > A comment from programming.reddit:

>

>
> > > If you want actual source code you can use for attaching real world units to numbers, and carrying
> > > them through the calculations, and getting compile errors on mismatches, see:

>
> > >http://lss.fnal.gov/archive/1998/conf/Conf-98-328.pdf

>
> > > "Introduction to the SILibrary of Unit-Based Computation" by WalterE. Brown

>
> [cunis92] R. Cunis, ``A Package for Handling Units of Measure in Lisp'',
> ACM Lisp Pointers, vol. 5, no. 2, 1992.
>
> http://www.isi.edu/isd/LOOM/document...res-usage.text
>
> http://www.cs.cmu.edu/afs/cs/project...lisp/code/...- Hide quoted text -
>
> - Show quoted text -

Thanks; I've put these links into the page together with the link to
the 1998 C++ paper.

Mark

Mark