Re: [Haskell-cafe] Rank N Kinds
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 :: **) - (String :: **) ] t3 = [42 :: Int, (), This is true *** type ] :k t3 * head t3 42 :: Int (head $ tail t3) True True True :: Bool Wvv 2 Aug 2013 at 5:34:26, Daniel Peebles [via Haskell] (ml-node+s1045720n5733708...@n5.nabble.com) wrote: 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 [hidden email] wrote: The right one is `instance Functor TupleList where ...` -- View this message in context: http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5734055.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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 (TupleUnit inside tuple (TupleUnit True TupleNil)))
And we can easily define rankNkinds functions, which can only work with
rankNkinds data,
like fstL, sndL, headL, tailL (see my previous letter)
But Haskell is weak to work with truly rankNkinds functions.
Let's look at Functor
instance Functor (TupleList (a :: **)) where
fmap :: ?
fmap = tmap
What's the signature of fmap? Even with rankNkinds we can't define a
signature. Without new extensions.
Let's look at tmap ~ map for list.
It's bit simplier for us
tmap ::
tmap _ TupleNil = TupleNil
tmap f (TupleUnit x xs) = TupleUnit (f x) (tmap f xs)
If we wish to work with `f` like in this example, we must use
`rankNkindsFunctions` extension.
It's very hard to implement this extension into Haskell (imho)
Let's think we've already had this extension and we have a `tmap`
Let's try to write rankNkinds functions for next tupleLists:
tupleL :: TupleList ( (Int :: **) - (String :: **) - (Bool :: **) )
tupleL = TupleUnit 5 (TupleUnit inside tuple (TupleUnit True TupleNil)))
tupleL' :: TupleList ( (Int :: **) - (Int :: **) - (Bool :: **) )
tupleL' = TupleUnit 5 (TupleUnit 42 (TupleUnit True TupleNil)))
tupleL'' :: TupleList ( (Int :: **) - (Int :: **) - (Int :: **) )
tupleL'' = TupleUnit 5 (TupleUnit 42 (TupleUnit 777 TupleNil)))
here they are:
f :: ((Int - Int) :: **) - ((String - String) :: **) - ((Bool - Bool)
:: **)
f :: Int - Int
f = (+ 2)
f :: String - String
f = (Hello ++)
f :: Bool - Bool
f = (True )
2nd:
f' :: c@((Int - Int) :: **) - c'@((Int - Int) :: **) - ((Bool - Bool)
:: **)
f' :: c@(Int - Int)
f' = (+ 2)
f' :: c'@(Int - Int)
f' = (* 5)
f' :: Bool - Bool
f' = (True )
3rd:
f'' :: c@((Int - Int) :: **) - c@((Int - Int) :: **) - c@((Int - Int)
:: **)
f'' :: c@(Int - Int)
f'' = (+ 2)
These functions not only look weird, they look like overloading, but they
are not.
But truly, they are really weird.
Le's look deeply at line `tmap f (TupleUnit x xs) = TupleUnit (f x) (tmap f
xs)`
Truly rankNkinds functions works like ST Monad and partly applied function
together!
This is awesome!
((Int - Int) :: **) - ((String - String) :: **) - ((Bool - Bool) ::
**) `op` (Int ::*) =
(Int :: **) - ((String - String) :: **) - ((Bool - Bool) :: **)
(Int :: **) - ((String - String) :: **) - ((Bool - Bool) :: **)
`op` (String ::*) =
(Int :: **) - (String :: **) - ((Bool - Bool) :: **)
(Int :: **) - (String :: **) - ((Bool - Bool) :: **) `op` (Bool ::*)
=
(Int :: **) - (String :: **) - (Bool :: **)
== TupleUnit (f x) (TupleUnit (f x') (TupleUnit (f x'') TupleNil))
Ok. Now we are ready to redefine f'' in a general way.
We need to have one extra extension: RecursiveSignatures.
We add 2 quantifications: 'forany' and 'forrec' (it's just my suggestion,
may be is too complicated and exists easier way to do this):
f''' :: forany i. forrec{i} c. c@((Int - Int) :: **) - { - c }
f''' :: forrec{i=0..3} c. c@(Int - Int)
f''' = (+ 2)
Let's write `f` function using these quantifications:
g :: forany i. forrec{i} a c. c@(a - a :: **) { - c }
g :: forrec c{0}. Int - Int == g :: forrec c{0} (a{0} ~ Int). a -
a
g = (+ 2)
g :: forrec c{1}. String - String
g = (Hello ++)
g :: forrec c{2}. Bool - Bool
g = (True )
And now it is possible to write signatures to `tmap` and `fmap`
tmap :: forany i. forrec{i} a b c c' c''. c@( (a - b) :: **) { - c } -
c'@(a :: * :: **) { - c' } - c''@(b :: * :: **) { - c'' }
fmap :: forany i. forrec{i} a b c c' c''. c@( (a - b) :: **) { - c } - f
(c'@(a :: **) { - c' }) - f (c''@(b :: **) { - c'' })
P.S. We could write foldr function for our tupleLists as:
folded :: Bool
folded = foldr h True tupleL
h :: forany i. forrec{i} a c. c@( a - b - b :: **) { - c }
h :: forrec c{0}. Int- Bool - Bool
h :: forrec c{1}. String - Bool - Bool
h :: forrec c{2}. Bool - Bool - Bool
P.S.S. All this staff is open for discussion ))
cheers, Wvv
--
View this message in context:
http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733699.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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 archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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 vite...@rambler.ru wrote: 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 archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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] (ml-node+s1045720n5733561...@n5.nabble.com) 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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 vite...@rambler.ru [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] (ml-node+s1045720n5733561...@n5.nabble.com) 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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+s1045720n5733671...@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.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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 as I know. Cheers, Pedro ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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...@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.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank N Kinds
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: 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Rank N Kinds
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
