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 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 wrote: >

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 ar

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

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" sn

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 if

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

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] (ml-node+s1045720n5733510

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 wrote: > It was discussed a bit here: > http://ghc.haskell.org/trac/ghc/ticket/8090 > >

[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, ... **= *, *->B