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 |
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 |
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 |
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 |
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 |
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 |
Free forum by Nabble | Edit this page |