[Haskell-cafe] GSoC proposal: Units for GHC

[Richard Eisenberg]

Hi Nils,

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!
Richard

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
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>