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> -> The idea is to have the compiler complain whenever you try to add <b> to <a> or if you expect something other than 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> = "), but I don't see how the "core" of this "unit verification system" could be placed into a library. - Nils

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

The idea is to have the compiler complain whenever you try to add <b> to <a> or if you expect something other than 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> = "), 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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users