Aviation has inherited a bewildering mix of units of measurement from its roots in marine navigation and engineering in Imperial/U.S. units. Distances between airports may be in statute miles, kilometres, or nautical miles, while altitudes are in feet, or flight levels, or metres. Speed is measured in knots, which is nautical miles per hour, unless it’s measured by Mach number, which varies with altitude and temperature. And fuel? They may pay for it as so much per gallon or litre, but they measure fuel load for weight and balance calculations as pounds, kilograms, or tonnes.
How did this mess come about, and is there any prospect for simplifying it?
4 Likes
Given that there appears to be a bug in the set theoretic foundation of mathematics that sends it, thence software engineering off in the direction of dimensionless numbers, probably the lowest hanging fruit for insurance companies – if not international standards agencies – is prioritizing the use of F# in critical software engineering.
Type systems for programming languages with numeric types can be extended to support the checking of units of measure. Quantification over units then introduces a new kind of parametric polymorphism with a corresponding Reynolds-style representation independence principle: that the behaviour of programs is invariant under changes to the units used. We prove this ‘dimensional invariance’ result and describe four consequences. The first is that the type of an expression can be used to derive equations which describe its properties with respect to scaling (akin to Wadler’s ‘theorems for free’ for System F). Secondly there are certain types which are inhabited only by trivial terms. For example, we prove that a fully polymorphic square root function cannot be written using just the usual arithmetic primitives. Thirdly we exhibit interesting isomorphisms between types and for first-order types relate these to the central theorem of classical dimensional analysis. Finally we suggest that for any expression whose behaviour is dimensionally invariant there exists some equivalent expression whose type reflects this behaviour, a consequence of which would be a full abstraction result for a model of the language.
Andrew Kennedy PhD Thesis, University of Cambridge, 1995
Andrew Kennedy Lecture notes , for CEFP’09, Revised July 2010
2 Likes
