[Haskell-cafe] Rank N Kinds

[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 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.