... | ... | @@ -25,7 +25,7 @@ Here are the projects we're currently working on: |
|
|
|
|
|
- **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\].
|
|
|
|
|
|
- **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 his wiki page \[20\]. At the moment there is no useful *computation* over the type-level naturals, but there will be soon.
|
|
|
- **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.
|
|
|
|
|
|
- **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.
|
|
|
|
... | ... | |