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 <vite...@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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
