[Haskell-cafe] Rank N Kinds

[Wvv]

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.