Changes between Version 16 and Version 17 of Status/May12

Show
Ignore:
Timestamp:
05/10/12 07:53:52 (12 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Status/May12

    v16 v17  
    2222 * '''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 [18]. 
    2323 
    24  * '''Type level literals'''.  Iavor Diatchk has added type-level natural numbers (kind `Nat`) and strings (kind `Symbol`) to GHC.  You can find lots of details on the wiki page [20].  At the moment there is no useful ''computation'' over the type-level naturals, but he is 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 we expect to have something working fairly soon. 
     24 * '''Type level literals'''.  Iavor Diatchki has added type-level natural numbers (kind `Nat`) and strings (kind `Symbol`) to GHC.  You can find lots of details on the wiki page [20].  At the moment there is no useful ''computation'' over the type-level naturals, but he is 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 we expect to have something working fairly soon. 
    2525 
    2626 * '''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)" [19].  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.