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.