TypeFamilies vs. FunctionalDependencies & type-level recursion

Dan Knapp dankna at gmail.com
Sat Jul 30 20:05:58 CEST 2011


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
<iavor.diatchki at gmail.com> wrote:
> 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.
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at 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)



More information about the Haskell-prime mailing list