Helllo, On Sat, Jul 30, 2011 at 2:11 AM, <o...@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.
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
