Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

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 wrote:

Helllo,

On Sat, Jul 30, 2011 at 2:11 AM, 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

-- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer)