[Haskell-cafe] Rank N Kinds

[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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Carter Schonwald]

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

[Wvv]

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] ([hidden email]) 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

[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: RE: Re: Rank N Kinds

[José Pedro Magalhães]

Hi,

On Fri, Jul 26, 2013 at 10:42 PM, Wvv <vit...@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

[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] ([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: RE: Re: Rank N Kinds

[Roman Cheplyaka]

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 <vit...@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+s1045...@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.

[Wvv]

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] ([hidden email]) 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: RE: Re: 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.

_______________________________________________
Haskell-Cafe mailing list

Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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

[Daniel Peebles]

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 :)

[Wvv]

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] ([hidden email]) 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: RE: Re: Rank N Kinds