[Haskell-cafe] Rank N Kinds

[Wvv]

Yes,
True :: Bool :: * :: ** :: *** :: **** :: ... in Haskell is the same as

True :: Bool :: Set0 :: Set1 :: Set2 :: Set3 :: ... in Agda

And I'm asking for useful examples for *** (Set2 in Agda) and higher


cheers Wvv

  28 Jul 2013 at 8:44:08, Schonwald [via Haskell]
  (ml-node+s1045720n5733510h49 at n5.nabble.com) wrote:


  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 <[hidden email]> 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
    [hidden email]
    http://www.haskell.org/mailman/listinfo/haskell-cafe



  _______________________________________________
  Haskell-Cafe mailing list
  [hidden email]
  http://www.haskell.org/mailman/listinfo/haskell-cafe


  ----------------------------------------------------------------------------

  If you reply to this email, your message will be added to the discussion
  below:http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733510.html
  To unsubscribe from Rank N Kinds, click here.
  NAML




--
View this message in context: http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733545.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130728/3c9480af/attachment.htm>