By the way, I have been testing your type-nats branch this week. I added my observations to the GHC trac ticket on the feature, as you probably saw. After a discussion with other people here at HacPhi, I've decided that what I'm going to attempt is to add type-level Maybes so that subtraction and other partial operations can exist. This entails adding Maybe as an arity-1 kind constructor, which of course means adding the notion of kind constructors that have nonzero arities at all.
On Sat, Jul 30, 2011 at 1:55 PM, Iavor Diatchki <[email protected]> wrote: > Helllo, > > On Sat, Jul 30, 2011 at 2:11 AM, <[email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-prime > > -- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer) _______________________________________________ Haskell-prime mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-prime
