Typing units correctly

[Andrew Kennedy]

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
system;
(b) not appreciating the need for parametric polymorphism over
dimensions/units.

As others have pointed out, (a) doesn't work because the algebra of units of
measure 
is not free - units form an Abelian group (if integer exponents are used) or
a
vector space over the rationals (if rational exponents are used) and so it's
not
possible to do unit-checking by equality-on-syntax or unit-inference by
ordinary
syntactic unification. Furthermore, parametric polymorphism is essential for
code
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
this
thread have cited :-)

To turn to the original question, I did once give a moment's thought to the
combination
of type classes and types for units-of-measure. I don't think there's any
particular
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
something,
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
>