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 :: **)
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
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
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
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::**) =
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
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
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
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]
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:
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, ...
**= *,
11 matches
Mail list logo