hello Wvv,

a lot of these ideas have been explored before in related (albeit "simpler") languages to haskell, are you familiar with idris, coq, or agda?

cheers

-Carter

On Fri, Jul 26, 2013 at 4:42 PM, Wvv <[hidden email]> wrote:

It was discussed a bit here:
http://ghc.haskell.org/trac/ghc/ticket/8090

Rank N Kinds:
Main Idea is:

If we assume an infinite hierarchy of classifications, we have

True :: Bool :: * :: ** :: *** :: **** :: ...

Bool = False, True, ...
* = Bool, Sting, Maybe Int, ...
** = *, *->Bool, *->(*->*), ...
*** = **, **->*, (**->**)->*, ...
...

RankNKinds is also a part of lambda-cube.

PlyKinds is just type of ** (Rank2Kinds)

class Foo (a :: k) where <<==>> class Foo (a :: **) where

*** is significant to work with ** data and classes;
more general: Rank(N)Kinds is significant to work with Rank(N-1)Kinds

First useful use is in Typeable.
In GHC 7.8
class Typeable (a::k) where ... <<==>> class Typeable (a ::**) where ...

But we can't write
data Foo (a::k)->(a::k)->* ... deriving Typeable

If we redeclare
class Typeable (a ::***) where ...
or even
class Typeable (a ::******) where ...
it becomes far enough for many years

I'm asking to find other useful examples

--
View this message in context: http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

If you reply to this email, your message will be added to the discussion below:

http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733510.html

To unsubscribe from Rank N Kinds, click here.
NAML