Changes between Version 15 and Version 16 of Status/May12
- May 10, 2012 2:53:20 PM (22 months ago)
v15 v16 22 22 * '''Holes in terms'''. Thijs Alkemade and Sean Leather have been working on another variant of deferred error messages, that would allow you to write a program that contains as-yet-unwritten sub-terms, or "holes" and have GHC report a fairly precise type for the hole. The idea is inspired by Agda's interactive programming environment, which has a facility of this kind. The more complicated the types get, the more useful this is! Details on their wiki page . 23 23 24 * '''Type level literals'''. (Iavor Diatchki) I added type-level natural numbers (kind `Nat`) and strings (kind `Symbol`) to GHC. You can find lots of details on the wiki page . At the moment there is no useful ''computation'' over the type-level naturals, but I'm currently extending GHC's constraint solver with support for reasoning about type-expressions involving addition, multiplication, and exponentiation. This work is happening on branch 'type-nats' in the repo, and I hopeto have something working fairly soon. 24 * '''Type level literals'''. to have something working fairly soon. 25 25 26 26 * '''Typechecker performance improvements'''. Most of the smarts of type inference are now located in the type constraint solver, described in our paper "Modular type inference with local assumptions: !OutsideIn(X)" . It works just fine for redgular old ML-style programs, but was a bit slow for programs that make heavy use of type-level computation. Dimitrios has been working hard to improve its performance; we have carried out at least three major refactorings, deleted tons of code, and made it faster and more beautiful.