GSoC proposal: Units for GHC

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

GSoC proposal: Units for GHC

Nils Schweinsberg
Hi Haskell-Cafe & GHC-users!

I'm looking to apply for the GSoC and since I've worked on GHC before
I'd like to continue to do so. My proposal would be something that
tempted me (as a physics student) for a while: Units for Haskell/GHC.

This project has been suggested for a long time on the GHC wiki, and
there is already a lot of work done for other languages like ML, F#
etc[1]. I have tried to implement e.g. the unification algorithm from
the "Types for Units-of-Measure in F#" talk[2] for an abstract syntax
tree[3] and it was pretty much straight forward. As I see it, the
project would consist of:

  1.) Find appropriate rules/algorithms for unit analysis. Most (if not
all?) of this should be covered in those papers/talks on [1].

  2.) Applying the rules to the Haskell syntax tree used in GHC.

I have approximately 3 years of experience with Haskell, I worked for
the database research group[4] at the University of Tübingen (Germany)
on the Database Supported Haskell[5] library. I've done most of the
coding for the monad comprehension[6] extension, which has been added to
the latest GHC release version. I'm already quite familiar with the GHC
internals of the compiler/typechecker, and even though I'd have to look
up how exactly type interference etc. works in GHC (as I've only *used*
it, but never tried to understand/modify it) I'm confident that the work
on GHC itself should be doable in the given timeframe.

So my questions would be:

Do you think this is a appropriate GSoC project?
What should I include in the application/project proposal?
Anything else? Opinions, suggestions?

I realize that I'm kind of late and probably should have written this
email a long time ago. But there are still 2 days left for the student
application and hopefully I'll get some good feedback by then.



- Nils



[1]: http://research.microsoft.com/en-us/um/people/akenn/units/index.html
[2]:
http://research.microsoft.com/en-us/um/people/akenn/units/MLWorkshop2008.pdf
[3]: https://github.com/mcmaniac/units/blob/master/src/Unification.hs
[4]: http://db.inf.uni-tuebingen.de/team
[5]: http://hackage.haskell.org/package/DSH
[6]: http://db.inf.uni-tuebingen.de/files/giorgidze/haskell2011.pdf

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] GSoC proposal: Units for GHC

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


Jurriën

On 4 Apr 2012, at 13:38, Nils Schweinsberg wrote:

> Hi Haskell-Cafe & GHC-users!
>
> I'm looking to apply for the GSoC and since I've worked on GHC before I'd like to continue to do so. My proposal would be something that tempted me (as a physics student) for a while: Units for Haskell/GHC.
>
> This project has been suggested for a long time on the GHC wiki, and there is already a lot of work done for other languages like ML, F# etc[1]. I have tried to implement e.g. the unification algorithm from the "Types for Units-of-Measure in F#" talk[2] for an abstract syntax tree[3] and it was pretty much straight forward. As I see it, the project would consist of:
>
> 1.) Find appropriate rules/algorithms for unit analysis. Most (if not all?) of this should be covered in those papers/talks on [1].
>
> 2.) Applying the rules to the Haskell syntax tree used in GHC.
>
> I have approximately 3 years of experience with Haskell, I worked for the database research group[4] at the University of Tübingen (Germany) on the Database Supported Haskell[5] library. I've done most of the coding for the monad comprehension[6] extension, which has been added to the latest GHC release version. I'm already quite familiar with the GHC internals of the compiler/typechecker, and even though I'd have to look up how exactly type interference etc. works in GHC (as I've only *used* it, but never tried to understand/modify it) I'm confident that the work on GHC itself should be doable in the given timeframe.
>
> So my questions would be:
>
> Do you think this is a appropriate GSoC project?
> What should I include in the application/project proposal?
> Anything else? Opinions, suggestions?
>
> I realize that I'm kind of late and probably should have written this email a long time ago. But there are still 2 days left for the student application and hopefully I'll get some good feedback by then.
>
>
>
> - Nils
>
>
>
> [1]: http://research.microsoft.com/en-us/um/people/akenn/units/index.html
> [2]: http://research.microsoft.com/en-us/um/people/akenn/units/MLWorkshop2008.pdf
> [3]: https://github.com/mcmaniac/units/blob/master/src/Unification.hs
> [4]: http://db.inf.uni-tuebingen.de/team
> [5]: http://hackage.haskell.org/package/DSH
> [6]: http://db.inf.uni-tuebingen.de/files/giorgidze/haskell2011.pdf
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] GSoC proposal: Units for GHC

Nils Schweinsberg
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
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] GSoC proposal: Units for GHC

Christian Höner zu Siederdissen-2
Hi,

Most, if not all could reasonably be implemented using type families --
though there is a potential O(n^2) instance problem. In KIS:PEY:2010,
there is an example for addition which you could look at.

That is, using the example

(1::Int) + (1::Double) would work out to (2::Double) instead of a
compile-time error.

The paper is probably a very good read for you.

Gruss,
Christian


KIS:PEY:2010
Kiselyov et al, Fun with type functions

* Nils Schweinsberg <[hidden email]> [04.04.2012 14:18]:

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

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

attachment0 (205 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] GSoC proposal: Units for GHC

Richard Eisenberg
In reply to this post by Nils Schweinsberg
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] GSoC proposal: Units for GHC

Roel van Dijk-3
2012/4/4 Richard Eisenberg <[hidden email]>:
> - 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.

I am a happy user of the type family variant of the dimensional
package [1]. It can represent all possible dimensions in the type
system by encoding them as powers of 7 base dimensions. It supports
all SI units and a few non-SI units. One of the limitations of this
approach is that you can not make a distinction between absolute and
relative units (degree Celsius vs Kelvin). I found the wikipedia page
on dimensional analysis [2] to present a good overview of the problem
space.

I share Gregory Collins' question on how your work would differ from
the dimensional package, or what it would add.

1 - https://github.com/bjornbm/dimensional-tf
2 - http://en.wikipedia.org/wiki/Dimensional_analysis

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users