[Haskell-cafe] Rank N Kinds

[Wvv]

How about this, I found it bt myself:


data TupleList (t :: **) = TupleNil | TupleUnit t (TupleList t)

fstL :: TupleList (a -> **) -> a
fstL TupleNil = error "TupleList2 is TupleNil"
fstL (TupleUnit a _ ) = a

sndL :: TupleList (* -> a -> **) -> a
sndL TupleNil = error "TupleList2 is TupleNil"
sndL (TupleUnit a TupleNil ) = error "TupleList2 is TupleUnit a TupleNil"
sndL (TupleUnit _ (TupleUnit a _ ) ) = a

headL :: TupleList (a -> **) -> a
headL TupleNil = error "TupleList2 is TupleNil"
headL (TupleUnit a _ ) = a

tailL :: TupleList (* -> a) -> a
tailL TupleNil = error "TupleList2 is TupleNil"
tailL (TupleUnit _ a ) = a

instance Functor (TupleList (a :: **)) where
fmap _ TupleNil = TupleNil
fmap f (TupleUnit x xs) = TupleUnit (f x) (fmap xs)


tupleL :: TupleList ( (Int :: *) -> (String :: *) -> (Bool :: *) )
tupleL = TupleUnit 5 (TupleUnit "inside tuple" (TupleUnit True TupleNil)))

fstTuppleL :: Int
fstTuppleL = fstL tupleL -- = 2

sndTuppleL :: String
sndTuppleL = sndL tupleL -- = "inside tuple"

tlTuppleL :: TupleList ( (String :: *) -> (Bool :: *) )
tlTuppleL = tailL tupleL -- = TupleUnit "inside tuple" (TupleUnit True TupleNil))

cheers, Wvv

  31 Jul 2013 at 22:48:19, Roman Cheplyaka-2 [via Haskell]
  (ml-node+s1045720n5733671h40 at n5.nabble.com) wrote:


  That's because types that belong to most non-star kinds cannot have
  values.

  data Foo (a :: k) = Foo

  is okay,

  data Foo (a :: k) = Foo a

  is bad because there cannot be a field of type a :: k.

  So no, no useful examples exist, because you wouldn't be able to use
  such a data constructor even if you could declare it.

  Roman

  * Wvv <[hidden email]> [2013-07-31 11:40:17-0700]
  > OMG!
  > I still have 7.6.3. It has old Typeable.
  >
  > I misunderstood PolyKinds a bit. It looks like k /= **, k ~ *******...
  >
  > But we cannot use "CloseKinds" like
  >
  > data Foo (a::k) = Foo a -- catch an error "Expected kind `OpenKind', but
  `a' has
  > kind `k'"
  >
  >
  > with RankNKinds we could write:
  > data Foo (a::**) = Foo a
  > data Bar (a::***) = Bar a
  >
  > So, now the task is more easy:
  > I'm asking for useful examples with "CloseKinds" with ** and higher, and
  any
  > useful examples for *** and higher
  >
  > cheers, Wvv
  >
  > 29 Jul 2013 at 14:44:50, José Pedro Magalhães [via Haskell]
  > ([hidden email]) wrote:
  >
  > Hi,
  >
  > On Fri, Jul 26, 2013 at 10:42 PM, Wvv <[hidden email]> wrote:
  >
  > 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
  >
  >
  > Why not? This works fine in 7.7, as far as I know.
  >
  >
  > Cheers,
  > Pedro
  >
  >
  >
  >
  > --
  > View this message in context:
  http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733667.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




--
View this message in context: http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733672.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/20130731/9f531c19/attachment.htm>