Typing units correctly

Andrew Kennedy akenn@microsoft.com
Wed, 14 Feb 2001 08:10:39 -0800

To be frank, the poster that you cite doesn't know what he's talking
about. He makes two elementary mistakes:

(a) attempting to encode dimension/unit checking in an existing type
(b) not appreciating the need for parametric polymorphism over

As others have pointed out, (a) doesn't work because the algebra of units of
is not free - units form an Abelian group (if integer exponents are used) or
vector space over the rationals (if rational exponents are used) and so it's
possible to do unit-checking by equality-on-syntax or unit-inference by
syntactic unification. Furthermore, parametric polymorphism is essential for
reuse - one can't even write a generic squaring function (say) without it.

Best to ignore the poster and instead read the papers that contributors to
thread have cited :-)

To turn to the original question, I did once give a moment's thought to the
of type classes and types for units-of-measure. I don't think there's any
problem: units (or dimensions) are a new "sort" or "kind", just as "row" is
in various
proposals for record polymorphism in Haskell. As long as this is tracked
through the
type system, everything should work out fine. Of course, I may have missed
in which case I'd be very interested to know about it.

- Andrew Kennedy.

> -----Original Message-----
> From: andrew@andrewcooke.free-online.co.uk
> [mailto:andrew@andrewcooke.free-online.co.uk]
> Sent: Wednesday, February 14, 2001 5:02 PM
> To: haskell-cafe@haskell.org
> Subject: Re: Typing units correctly
> Hi,
> I don't know if this is useful, but in response to a link to that
> article that I posted on Lambda, someone posted a link arguing that
> such an approach (at least in Ada) was impractical.  To be honest, I
> don't find it very convincing, but I haven't been following this
> discussion in detail.  It might raise some problems you have not
> considered.
> Anyway, if you are interested, it's all at
> http://lambda.weblogs.com/discuss/msgReader$818
> Apologies if it's irrelevant or you've already seen it,
> Andrew
> On Mon, Feb 12, 2001 at 01:51:54PM -0500, Dylan Thurston wrote:
> [...]
> > 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.
> [...]
> -- 
> http://www.andrewcooke.free-online.co.uk/index.html