Typing units correctly

[Dylan Thurston]

On Mon, Feb 12, 2001 at 10:08:02AM +0100, Bjorn Lisper wrote:
> >The main complication is that the type system needs to deal with
> >integer exponents of dimensions, if it's to do the job well.
> Andrew Kennedy has basically solved this for higher order languages with HM
> type inference. He made an extension of the ML type system with dimensional
> analysis a couple of years back. Sorry I don't have the references at hand
> but he had a paper in ESOP I think.

The papers I could find (e.g.,
http://citeseer.nj.nec.com/kennedy94dimension.html, "Dimension Types")
mention extensions to ML.  I wonder if it is possible to work within
the Haskell type system, which is richer than ML's type system.

The main problem I see is that the dimensions should commute:
  Length * Time = Time * Length.
I can't think of how to represent Length, Time, and * as types,
type constructors, or whatnot so that that would be true.  You could
put in functions to explicitly do the conversion, but that obviously
gets impractical.

Any such system would probably not be able to type (^), since the
output type depends on the exponent.  I think that is acceptable.

I think you would also need a finer-grained heirarchy in the Prelude
(including than in my proposal) to get this to work.

> It would be quite interesting to have a version of Haskell that would allow
> the specification of differential equations, so one could make use of all
> the good features of Haskell for this. This would allow the unified
> specification of systems that consist both of physical and computational
> components. This niche is now being filled by a mix of special-purpose
> modeling languages like Modelica and Matlab/Simulink for the physical part,
> and SDL and UML for control parts. The result is likely to be a mess, in
> particular when these specifications are to be combined into full system
> descriptions.

My hope is that you wouldn't need a special version of Haskell.

Best,
	Dylan Thurston