[Haskell-cafe] GSoC proposal: Units for GHC
eir at seas.upenn.edu
Wed Apr 4 14:59:20 CEST 2012
I think this is a great idea, and something I have on my longer-term
to-think-about-hard list. I experimented with an implementation of this
a few months ago, and I can try to recap, briefly, what I learned.
- A first crack at units in Haskell has already been done (by Bjorn
Buckwalter) and made public at http://code.google.com/p/dimensional/
This implementation uses functional dependencies heavily and is
restricted to only a specific 7 units.
- The version I hacked together used a whole lot of type families and
type level integers to track the degree of the different units. It
mostly worked, with a few caveats:
- Type inference sometimes got held up around the type families.
- The set of units to be used was user-definable, but all the units
had to be declared in the same place. This was because, under the hood,
each unit was assigned a number. I spent a while trying to get it all to
work without needing this internal representation, but failed.
- It was necessary to be very careful about ordering and such -- the
system naturally couldn't figure out that a + b = b + a.
I would recommend you check out
http://hackage.haskell.org/trac/ghc/wiki/TypeNats, a new development
already merged into HEAD that adds some mathematical axioms into the
constraints checker (solving the last problem I mentioned above). I also
believe there is work on type-level strings (which might be a solution
to the second problem), but I don't know much about it.
I guess my bottom-line conclusion is that with all the features that
Haskell already has, it may be possible to do this in a separate
library, if type inference is up to the challenge. I agree with Jurriën
that a library is better than a compiler update.
Looking forward to seeing the finished product!
On 4/4/12 8:17 AM, Nils Schweinsberg wrote:
> Am 04.04.2012 13:48, schrieb Jurriën Stutterheim:
>> This sounds pretty cool and useful. How much of this can be
>> implemented in a library and how much of this would need to be
>> supported on a compiler level? Ideally, most of this would be solved
>> on the library level.
> The compiler would have to know how to "typecheck" units, e.g. the
> addition (+) would combine two values of the same unit, the (/)
> operation would divide them:
> (+) :: <a> -> <a> -> <a>
> (/) :: <a> -> <b> -> <a/b>
> The idea is to have the compiler complain whenever you try to add <b>
> to <a> or if you expect something other than <a/b> as result from a
> division. This would require modifications to GHC at compiler level. A
> library could offer some basic units (SI units for example) and maybe
> even unit aliases ("<N> = <kg*m/s^2>"), but I don't see how the "core"
> of this "unit verification system" could be placed into a library.
> - Nils
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
More information about the Glasgow-haskell-users