44 | | * type level natural numbers ['''Iavor S. Diatchki'''] |
| 44 | * '''Type level natural numbers'''. Iavor S. Diatchki has been working on a solver for equations involving type-level natural numbers. This allows simplifying and reasoning about type-level terms involving |
| 45 | arithmetic. Currently, the solver can evaluate equations and inequalities mentioning the type functions `(+)`, `(*)`, `(^)`, and `(<=)`. The solver works pretty well when it can use evaluation to prove equalities (e.g., examples like `2 + 5 = x`, `2 + x = 5`). There is also some support for taking advantage of the commutativity and associativity of `(+)`, `(*)`. More experimental features include: support for `(-)`, which, currently is implemented by desugaring to `(+)`; the type-level function `FromNat1`, which has special support for working with natural number literals, and thus can be used to expose some of their inductive structure. This work is currently on the `type-nats` branch, and the plan is to merge it into HEAD into the next few months. |
| 46 | |
| 47 | * '''Kinds without data''' Trevor Elliott, Eric Mertens, and Iavor Diatchki have began implementing support for "data kind" declarations, described in more detail on the GHC wiki: http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData The idea is to allow a new form of declaration that introduces a new kind, whose members are described by the (type) constructors in the declaration. This is similar to promoting `data` declarations, except that no new value-level-constructors are declared, and it also allows the constructors to mention other kinds that do not have corresponding type-level representation (e.g., `*`). |
| 48 | |