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.
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
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
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+s1045720n5733510h49@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.
Hi,
On Fri, Jul 26, 2013 at 10:42 PM, Wvv
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
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+s1045720n5733561h30@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.
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
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+s1045720n5733561h30@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
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@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.
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.
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.
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
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
:k t3
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" ] *
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+s1045720n5733708h87@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.
participants (5)
-
Carter Schonwald -
Daniel Peebles -
José Pedro Magalhães -
Roman Cheplyaka -
Wvv