[Haskell-cafe] Rank N Kinds

[Carter Schonwald]

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 <vitea3v at rambler.ru> 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130728/1688f0cf/attachment.htm>