<div dir="ltr">hello Wvv, <div><br></div><div style>a lot of these ideas have been explored before in related (albeit "simpler") languages to haskell, are you familiar with idris, coq, or agda?</div><div style><br>
</div><div style>cheers</div><div style>-Carter</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 26, 2013 at 4:42 PM, Wvv <span dir="ltr"><<a href="mailto:vitea3v@rambler.ru" target="_blank">vitea3v@rambler.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It was discussed a bit here:<br>
<a href="http://ghc.haskell.org/trac/ghc/ticket/8090" target="_blank">http://ghc.haskell.org/trac/ghc/ticket/8090</a><br>
<br>
Rank N Kinds:<br>
Main Idea is:<br>
<br>
If we assume an infinite hierarchy of classifications, we have<br>
<br>
True :: Bool :: * :: ** :: *** :: **** :: ...<br>
<br>
Bool = False, True, ...<br>
* = Bool, Sting, Maybe Int, ...<br>
** = *, *->Bool, *->(*->*), ...<br>
*** = **, **->*, (**->**)->*, ...<br>
...<br>
<br>
RankNKinds is also a part of lambda-cube.<br>
<br>
PlyKinds is just type of ** (Rank2Kinds)<br>
<br>
class Foo (a :: k) where <<==>> class Foo (a :: **) where<br>
<br>
*** is significant to work with ** data and classes;<br>
more general: Rank(N)Kinds is significant to work with Rank(N-1)Kinds<br>
<br>
First useful use is in Typeable.<br>
In GHC 7.8<br>
class Typeable (a::k) where ... <<==>> class Typeable (a ::**) where ...<br>
<br>
But we can't write<br>
data Foo (a::k)->(a::k)->* ... deriving Typeable<br>
<br>
If we redeclare<br>
class Typeable (a ::***) where ...<br>
or even<br>
class Typeable (a ::******) where ...<br>
it becomes far enough for many years<br>
<br>
I'm asking to find other useful examples<br>
<br>
<br>
<br>
--<br>
View this message in context: <a href="http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482.html" target="_blank">http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482.html</a><br>
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>