[Haskell-cafe] Rank N Kinds
carter.schonwald at gmail.com
Sun Jul 28 07:42:31 CEST 2013
a lot of these ideas have been explored before in related (albeit
"simpler") languages to haskell, are you familiar with idris, coq, or agda?
On Fri, Jul 26, 2013 at 4:42 PM, Wvv <vitea3v at rambler.ru> wrote:
> It was discussed a bit here:
> 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:
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe