Wvv | 26 Jul 22:42 2013
Picon

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 
(Continue reading)

Carter Schonwald | 28 Jul 07:42 2013
Picon

Re: 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 <vitea3v <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Wvv | 28 Jul 20:07 2013
Picon

Re: 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] ([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


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: RE: Re: Rank N Kinds
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
José Pedro Magalhães | 29 Jul 13:26 2013
Picon

Re: Rank N Kinds

Hi,

On Fri, Jul 26, 2013 at 10:42 PM, Wvv <vitea3v <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Wvv | 31 Jul 20:40 2013
Picon

Re: 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] ([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
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Roman Cheplyaka | 31 Jul 21:45 2013

Re: 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 <vitea3v <at> 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+s1045720n5733561h30 <at> 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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
Wvv | 31 Jul 21:56 2013
Picon

Re: 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] ([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
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Wvv | 1 Aug 22:32 2013
Picon

Re: 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 <at> ((Int -> Int) :: **) -> c' <at> ((Int -> Int)  :: **) -> ((Bool -> Bool)
:: **)
	
 f' :: c <at> (Int -> Int)
 f' = (+ 2)
	
 f' :: c' <at> (Int -> Int)
 f' = (* 5)
	
 f' :: Bool -> Bool
 f' = (True &&)

3rd:

 f'' :: c <at> ((Int -> Int) :: **) -> c <at> ((Int -> Int)  :: **) -> c <at> ((Int -> Int) 
:: **)
	
 f'' :: c <at> (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 <at> ((Int -> Int) :: **) -> { -> c }
	
 f''' :: forrec{i=0..3} c. c <at> (Int -> Int)
 f''' = (+ 2)

Let's write `f` function using these quantifications:

 g :: forany i. forrec{i} a c. c <at> (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 <at> ( (a -> b) :: **) { -> c } ->
c' <at> (a :: * :: **) { -> c' } -> c'' <at> (b :: * :: **) { -> c'' }

 fmap :: forany i. forrec{i} a b c c' c''. c <at> ( (a -> b) :: **) { -> c } -> f
(c' <at> (a :: **) { -> c' }) -> f (c'' <at> (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 <at> ( 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.
Wvv | 1 Aug 22:55 2013
Picon

Re: 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.
Daniel Peebles | 2 Aug 04:31 2013
Picon

Re: 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 <vitea3v <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Wvv | 10 Aug 22:04 2013
Picon

Re: 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] ([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
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane