TypeFamilies vs. FunctionalDependencies & type-level recursion

[Iavor Diatchki]

Helllo,

On Sat, Jul 30, 2011 at 2:11 AM, <oleg at okmij.org> wrote:

>
> Second, what is the status of Nat kinds and other type-level data that
> Conor was/is working on? Nat kinds and optimized comparison of Nat
> kinds would be most welcome. Type level lists are better still
> (relieving us from Goedel-encoding type representations).
>
>
I  did some work on adding a Nat kind to GHC, you can find the
implementation in the "type-nats" branch of GHC.   The code there introduces
a new kind, Nat, and it allows you to write natural numbers in types, using
singleton types to link them to the value level.  The constraint solver for
the type level naturals in that implementation is a bit flaky, so lately I
have been working on an improved decision procedure.  When ready, I hope
that the new solver should support more operations, and it should be much
easier to make it construct explicit proof objects (e.g., in the style of
System FC).
-Iavor
PS: I am going on vacation next week, so I'll probably not make much
progress on the new solver in August.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-prime/attachments/20110730/e123cb98/attachment.htm>