Re: [Haskell-cafe] Rank N Kinds

2013-08-10 Thread Wvv
Paradoxes there are at logic and math. At programing languages we have bugs or features :)) Higher universe levels are needed first of all for more abstract programming. P.S. By the way, we don't need have extra TupleList, we have already list! t3 :: [ (Int :: **) - (Bool - Bool - Bool :: **)

Re: [Haskell-cafe] Rank N Kinds

2013-08-01 Thread Wvv
I still asking for good examples of ranNkinds data (and classes) But now let's look at my example, TupleList data TupleList (t :: **) = TupleNil | TupleUnit t (TupleList t) we can easily define tupleList tupleL :: TupleList ( (Int :: **) - (String :: **) - (Bool :: **) ) tupleL = TupleUnit 5

Re: [Haskell-cafe] Rank N Kinds

2013-08-01 Thread Wvv
I'm sorry, `instance Functor (TupleList (a :: **)) where ...` isn't right, sure. The right one is `instance Functor TupleList where ...` -- View this message in context: http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733700.html Sent from the Haskell - Haskell-Cafe mailing list

Re: [Haskell-cafe] Rank N Kinds

2013-08-01 Thread Daniel Peebles
The higher universe levels are mostly used to stave off logical paradoxes in languages where you care about that kind of stuff. In a fundamentally impredicative language like Haskell I don't see much point, but I'd be happy to find there is one :) On Thu, Aug 1, 2013 at 4:55 PM, Wvv

Re: [Haskell-cafe] Rank N Kinds

2013-07-31 Thread Wvv
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::**) =

Re: [Haskell-cafe] Rank N Kinds

2013-07-31 Thread Roman Cheplyaka
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

Re: [Haskell-cafe] Rank N Kinds

2013-07-31 Thread 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

Re: [Haskell-cafe] Rank N Kinds

2013-07-29 Thread José Pedro Magalhães
Hi, On Fri, Jul 26, 2013 at 10:42 PM, Wvv vite...@rambler.ru 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

Re: [Haskell-cafe] Rank N Kinds

2013-07-28 Thread 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]

Re: [Haskell-cafe] Rank N Kinds

2013-07-27 Thread Carter Schonwald
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:

[Haskell-cafe] Rank N Kinds

2013-07-26 Thread Wvv
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, ... **= *,