Re: Kindness of strangers (or strangeness of Kinds)

2012-06-11 Thread AntC
Edward Kmett  gmail.com> writes:

> On Mon, Jun 11, 2012 at 9:58 PM, AntC  clear.net.nz> 
wrote:
>>
>> [snip ...]
>>
>> Could we have :k (->) :: OpenKind -> * -> *  -- why not?
> 
> I don't quite understand why you would want arbitrary kinded arguments, but 
only in negative position. 
>

Thanks Edward, oops I've used the wrong terminology, sorry for the confusion. 
I didn't mean OpenKind but AnyKind. I put that only in a negative position 
more to sharpen the question, but also because I assumed the result from (->) 
would have to be grounded in Kind *; and then at least one of its arguments 
would also have to be grounded in Kind *.


I think perhaps(?) more PolyKindness is on the horizon: 
http://hackage.haskell.org/trac/ghc/wiki/GhcKinds  (section on GADKs, and sub-
pages on KindPolymorphism and ExplicitTypeApplication). I guess GHC is getting 
there by small steps, and doesn't yet have powerful enough Kind refinement nor 
Kind equality constraints, nor interleaving of Type and Kind inference.



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-11 Thread Edward Kmett
On Mon, Jun 11, 2012 at 9:58 PM, AntC  wrote:

> Simon Peyton-Jones  microsoft.com> writes:
>
> >
> > There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying
> hard to get rid of it as much as
> > possible, and it is much less important than it used to be. It's always
> been
> there, and is nothing to do with polykinds.
> >
> > I've extended the commentary a bit: see "Types" and "Kinds" here
> > http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
> >
> > The ArgKind thing has gone away following Max's recent unboxed-tuples
> patch,
> so we now only have OpenKind
> > (described on the above pages).
>
> Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)
>
> It's not that I have a specific problem (requirement) I'm trying to solve.
> It's more that I'm trying to understand how this ladder of
> Sorts/Kinds/Types/values hangs together.
>
> With Phantom types, we've been familiar for many years with uninhabited
> types,
> so why are user-defined (promoted) Kinds/Types different?
>
> The Singletons stuff shows there are use cases for mapping from uninhabited
> types to values -- but it seems to need a lot of machinery (all those
> shadow
> types and values). And indeed TypeRep maps from not-necessarily-inhabited
> types to values.
>
> Is it that we really need to implement type application in the surface
> language to get it all to come together? Then we won't need functions
> applying
> to dummy arguments whose only purpose is to carry a Type::Kind.
>
> To give a tight example:
>
>data MyNat = Z | S MyNat-- to be promoted
>
>data ProxyNat (a :: MyNat) = ProxyNat   -- :k ProxyNat :: MyNat -> *
>
>proxyNat :: n -> ProxyNat n -- rejected: Kind mis-match
>proxyNat _ = ProxyNat
>
> The parallel of that with phantom types (and a class constraint for MyNat)
> seems unproblematic -- albeit with Kind *.
>
> Could we have :k (->) :: OpenKind -> * -> *  -- why not?


I don't quite understand why you would want arbitrary kinded arguments, but
only in negative position.

Internally its already more like (->) :: OpenKind -> OpenKind -> * at the
moment. The changes simply permitted unboxed tuples in argument position,
relaxing a previous restriction. OpenKind is just a superkind of * and #,
not every kind. Kinds other than * and # just don't have a term level
representation. (Well kind Constraint is inhabited by dictionaries for
instances after a fashion, but you don't get to manipulate them directly.)

I'm a lot happier with the new plumbing than I was with the crap I've been
able to write by hand over the years for natural number types/singletons,
and I'm actually pretty happy with the fact that it makes it clearer that
there is a distinction between the type level and the term level, and I
can't say that I buy the idea of just throwing things open like that.

In particular, the "OpenKind" for all kinds that you seem to be proposing
sounds more like letting (->) :: forall (a :: BOX?) (b :: BOX?). a -> b ->
* (or (->) :: forall (a :: BOX?). a -> * -> *) than OpenKind, which exists
to track where unboxed types can lurk until polymorphism forces it to *.

With the 'more open' OpenKind you propose, it no longer collapses to * when
used in a polymorphic fashion, but merely dumbs down to forall (a :: BOX).
a, which strikes me as a particularly awkward transition. At the least,
you'd need to actually break the 'BOX is the only superkind' rule to
provide the quantification that can span over unboxed types and any boxed
type, (scribbled as BOX? above).

That seems to be a pretty big mess for something that can be solved readily
with simpler tools.

Mind you there is another case for breaking the BOX is the only superkind
rule (that is the horrible syntax hack that requires monomorphization of
the kinds of the results of type/data families can be cleaned up), but once
you have more than one superkind, you start complicating type equality,
needing other coercions, so it really shouldn't be done lightly.

-Edward
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-11 Thread AntC
Simon Peyton-Jones  microsoft.com> writes:

> 
> There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying 
hard to get rid of it as much as
> possible, and it is much less important than it used to be. It's always been 
there, and is nothing to do with polykinds.
> 
> I've extended the commentary a bit: see "Types" and "Kinds" here
> http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
> 
> The ArgKind thing has gone away following Max's recent unboxed-tuples patch, 
so we now only have OpenKind
> (described on the above pages).
> 

Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)

It's not that I have a specific problem (requirement) I'm trying to solve. 
It's more that I'm trying to understand how this ladder of 
Sorts/Kinds/Types/values hangs together.

With Phantom types, we've been familiar for many years with uninhabited types, 
so why are user-defined (promoted) Kinds/Types different?

The Singletons stuff shows there are use cases for mapping from uninhabited 
types to values -- but it seems to need a lot of machinery (all those shadow 
types and values). And indeed TypeRep maps from not-necessarily-inhabited 
types to values.

Is it that we really need to implement type application in the surface 
language to get it all to come together? Then we won't need functions applying 
to dummy arguments whose only purpose is to carry a Type::Kind.

To give a tight example:

data MyNat = Z | S MyNat-- to be promoted

data ProxyNat (a :: MyNat) = ProxyNat   -- :k ProxyNat :: MyNat -> *

proxyNat :: n -> ProxyNat n -- rejected: Kind mis-match
proxyNat _ = ProxyNat

The parallel of that with phantom types (and a class constraint for MyNat) 
seems unproblematic -- albeit with Kind *.

Could we have :k (->) :: OpenKind -> * -> *  -- why not?


AntC


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Edward Kmett
ghci> :k Maybe
Maybe :: * -> *

On Sat, Jun 9, 2012 at 1:34 AM, Rustom Mody  wrote:

> On Thu, Jun 7, 2012 at 7:16 AM, AntC  wrote:
>
>> I'm confused about something with promoted Kinds (using an example with
>> Kind-
>> promoted Nats).
>>
>> This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already
>> explained somewhere
>>
>
> Is there a way of seeing kinds in ghci?
> [In gofer I could do :s +k -- yeah this was 20 years ago :-) ]
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Rustom Mody
On Thu, Jun 7, 2012 at 7:16 AM, AntC  wrote:

> I'm confused about something with promoted Kinds (using an example with
> Kind-
> promoted Nats).
>
> This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already
> explained somewhere
>

Is there a way of seeing kinds in ghci?
[In gofer I could do :s +k -- yeah this was 20 years ago :-) ]
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Richard Eisenberg
Yes, I think using a singleton will solve your problem. It essentially 
acts like Proxy but keeps the parallelism between types and terms.


Here would be the definitions:

data Nat = Z | S Nat

-- This is the singleton type
data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: forall (n :: Nat). SNat n -> SNat (S n)

class NatToIntN (n :: Nat) where
  natToIntN :: SNat n -> Int
instance NatToIntN Z where
  natToIntN _ = 0
instance (NatToIntN n) => NatToIntN (S n) where
  natToIntN (SS n) = 1 + natToIntN n

-
It might be worth noting that there is no need for a class to define 
natToIntN. The following would also work:


natToIntN :: SNat n -> Int
natToIntN SZ = 0
natToIntN (SS n) = 1 + natToIntN n


Please do check out our paper for more info at the link Pedro sent out.

Richard

On 6/7/12 8:28 AM, José Pedro Magalhães wrote:

Hi,

On Thu, Jun 7, 2012 at 2:46 AM, AntC > wrote:



What does the `ArgKind' message mean?


`ArgKind` and `OpenKind` is what previously was called `?` and `??` 
(or the other

way around; I can't remember).
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubtyping

You might also want to have a look at Richard and Stephanie's latest 
paper draft, about

singletons, which is related to what you are trying in your example:
http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf 




Cheers,
Pedro



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


RE: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Simon Peyton-Jones
There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying hard 
to get rid of it as much as possible, and it is much less important than it 
used to be. It's always been there, and is nothing to do with polykinds.

I've extended the commentary a bit: see "Types" and "Kinds" here
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler

The ArgKind thing has gone away following Max's recent unboxed-tuples patch, so 
we now only have OpenKind (described on the above pages).

Simon

| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of AntC
| Sent: 08 June 2012 00:37
| To: glasgow-haskell-users@haskell.org
| Subject: Re: Kindness of strangers (or strangeness of Kinds)
| 
| José Pedro Magalhães  cs.uu.nl> writes:
| 
| > On Thu, Jun 7, 2012 at 2:46 AM, AntC 
| > clear.net.nz>
| wrote:
| >
| > What does the `ArgKind' message mean?
| >
| > `ArgKind` and `OpenKind` is what previously was called `?` and `??`
| > (or the
| otherway around; I can't remember).
| http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Ki
| ndsubty
| ping
| 
| Thanks Pedro, I'm trying to understand what's changing and why. (And I'd
| better repeat that I'm looking at 7.4.1, not HEAD; and SPJ's being
| perfectly clear that the promoted Kind stuff is not yet officially
| approved for prime
| time):
| 
| GHC 7.2.1> :k (->) :: ?? -> ? -> *
| 
| GHC 7.4.1> :k (->) :: * -> * -> *
| 
| At first sight (->) is becoming less polyKinded. Is the eventual aim to
| be:
| 
| GHC 7.6+> :k (->) :: AnyKind1 -> AnyKind2 -> *
| 
| 
| 
| >You might also want to have a look at Richard and Stephanie's latest
| >paper
| draft, about singletons, which is related to what you are trying in your
| example:http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf
| >
| 
| That's what I'm doing, and trying to understand the machinery behind it.
| The
| naieve approach I started with was how to get one-way from type to its
| single
| value -- I wasn't aiming for the whole singleton gig.
| 
| AntC
| 
| 
| 
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-07 Thread wagnerdm

Quoting AntC :


GHC 7.2.1> :k (->) :: ?? -> ? -> *

GHC 7.4.1> :k (->) :: * -> * -> *

At first sight (->) is becoming less polyKinded. Is the eventual aim to be:

GHC 7.6+> :k (->) :: AnyKind1 -> AnyKind2 -> *


I sort of doubt it. After all, the prototypical thing to do with a  
function is to apply it to something, and Haskell expressions are  
categorized by types of OpenKind -- the new kinds you create with the  
new extension don't classify inhabited types.


It looks to me like "a -> b" and "(->) a b" are just different  
syntactic classes now, not interconvertible with each other:


Prelude GHC.Exts> :set -XMagicHash
Prelude GHC.Exts> :k Int# -> Int#
Int# -> Int# :: *
Prelude GHC.Exts> :k (->) Int# Int#

:1:6:
Expecting a lifted type, but `Int#' is unlifted
In a type in a GHCi command: (->) Int# Int#

Perhaps this is a side-effect of the introduction of PolyKinds; from  
the release notes:


"There is a new feature kind polymorphism (-XPolyKinds): Section  
7.8.1, ?Kind polymorphism?. A side-effect of this is that, when the  
extension is not enabled, in certain circumstances kinds are now  
defaulted to * rather than being inferred."


Though I must say it's not 100% clear to me exactly what's changed, or  
whether it was intentional.

~d

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-07 Thread AntC
José Pedro Magalhães  cs.uu.nl> writes:

> On Thu, Jun 7, 2012 at 2:46 AM, AntC  clear.net.nz> 
wrote:
> 
> What does the `ArgKind' message mean?
> 
> `ArgKind` and `OpenKind` is what previously was called `?` and `??` (or the 
otherway around; I can't remember). 
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubty
ping

Thanks Pedro, I'm trying to understand what's changing and why. (And I'd 
better repeat that I'm looking at 7.4.1, not HEAD; and SPJ's being perfectly 
clear that the promoted Kind stuff is not yet officially approved for prime 
time):

GHC 7.2.1> :k (->) :: ?? -> ? -> *

GHC 7.4.1> :k (->) :: * -> * -> *

At first sight (->) is becoming less polyKinded. Is the eventual aim to be:

GHC 7.6+> :k (->) :: AnyKind1 -> AnyKind2 -> *



>You might also want to have a look at Richard and Stephanie's latest paper 
draft, about singletons, which is related to what you are trying in your 
example:http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf
> 

That's what I'm doing, and trying to understand the machinery behind it. The 
naieve approach I started with was how to get one-way from type to its single 
value -- I wasn't aiming for the whole singleton gig.

AntC



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-07 Thread José Pedro Magalhães
Hi,

On Thu, Jun 7, 2012 at 2:46 AM, AntC  wrote:

>
> What does the `ArgKind' message mean?
>

`ArgKind` and `OpenKind` is what previously was called `?` and `??` (or the
other
way around; I can't remember).
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubtyping

You might also want to have a look at Richard and Stephanie's latest paper
draft, about
singletons, which is related to what you are trying in your example:
http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf


Cheers,
Pedro
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-06 Thread AntC
  seas.upenn.edu> writes:

> 
> Quoting AntC  clear.net.nz>:
> 
> > {-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures#-}
> >
> > data MyNat = Z | S MyNat
> >
> > class NatToIntN (n :: MyNat)
> > where natToIntN :: (n :: MyNat) -> Int
> > instance NatToIntN Z
> > where natToIntN _ = 0
> > instance (NatToIntN n) => NatToIntN (S n)
> > where natToIntN _ = 1 + natToInt (undefined :: n)
> >
> > But GHC rejects the class declaration (method's type):
> > "Kind mis-match
> >  Expected kind `ArgKind', but `n' has kind `MyNat'"
> > (Taking the Kind signature out of the method's type gives same message.)
> 
> At a guess, (->) :: * -> * -> *, but n :: MyNat, not n :: *, so (->) n  
> is badly kinded. In comparison:
> 
> > data Proxy a = Proxy
> >
> > class NatToInt (n :: MyNat)
> > where natToInt :: Proxy (n :: MyNat) -> Int
> > instance NatToInt Z
> > where natToInt _ = 0
> > instance (NatToInt n) => NatToInt (S n)
> > where natToInt _ = 1 + natToInt (Proxy :: Proxy n)
> 
> Here Proxy n :: *, even if n :: MyNat, so Proxy n is a fine argument  
> to hand to (->).
> 
> ~d
> 

Thanks for the prompt response, and yes, you're right, so says GHCi:

:k (->) :: * -> * -> *  -- so `ArgKind` in the message means `*'

:k Proxy :: AnyK -> *   -- which answers what is `AnyKind'

So Proxy is a kind-level wormhole: forall k. k -> *
Singleton types are a wormhole from types to values.

For the natToInt method, it's a shame having to insert Proxy's everywhere -- 
it takes away from the parallel to value-level equations.

Perhaps I need promoted GADT's?

Or perhaps PolyKinded (->) :: k1 -> k2 -> k3?

AntC


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Kindness of strangers (or strangeness of Kinds)

2012-06-06 Thread wagnerdm

Quoting AntC :


{-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures#-}

data MyNat = Z | S Nat

class NatToIntN (n :: MyNat)
where natToIntN :: (n :: MyNat) -> Int
instance NatToIntN Z
where natToIntN _ = 0
instance (NatToIntN n) => NatToIntN (S n)
where natToIntN _ = 1 + natToInt (undefined :: n)

But GHC rejects the class declaration (method's type):
"Kind mis-match
 Expected kind `ArgKind', but `n' has kind `MyNat'"
(Taking the Kind signature out of the method's type gives same message.)


At a guess, (->) :: * -> * -> *, but n :: MyNat, not n :: *, so (->) n  
is badly kinded. In comparison:



data Proxy a = Proxy

class NatToInt (n :: MyNat)
where natToInt :: Proxy (n :: MyNat) -> Int
instance NatToInt Z
where natToInt _ = 0
instance (NatToInt n) => NatToInt (S n)
where natToInt _ = 1 + natToInt (Proxy :: Proxy n)


Here Proxy n :: *, even if n :: MyNat, so Proxy n is a fine argument  
to hand to (->).


~d

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Kindness of strangers (or strangeness of Kinds)

2012-06-06 Thread AntC
I'm confused about something with promoted Kinds (using an example with Kind-
promoted Nats).

This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already 
explained somewhere -- I know 7.4.1 is relatively experimental. I have 
searched the bug tracs and discussions I could find.)

Starting with nats at type level, this works fine:

{-# OPTIONS_GHC -XTypeFamilies -XFlexibleInstances -XUndecidableInstances
-XScopedTypeVariables #-}

data ZeT;   data SuT n

class NatToIntT n
where natToIntT :: n -> Int
instance NatToIntT ZeT
where natToIntT _ = 0
instance (NatToIntT n) => NatToIntT (SuT n)
where natToIntT _ = 1 + natToIntT (undefined :: n)

I converted naively to promoted Kinds:

{-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures#-}

data MyNat = Z | S Nat

class NatToIntN (n :: MyNat)
where natToIntN :: (n :: MyNat) -> Int
instance NatToIntN Z
where natToIntN _ = 0
instance (NatToIntN n) => NatToIntN (S n)
where natToIntN _ = 1 + natToInt (undefined :: n)

But GHC rejects the class declaration (method's type):
"Kind mis-match
 Expected kind `ArgKind', but `n' has kind `MyNat'"
(Taking the Kind signature out of the method's type gives same message.)

Eh? MyNat is what I want the argument's Kind to be.


A PolyKinded version (cribbed from 'Giving Haskell a Promotion' on multi-
kinded TypeRep) also works fine:

data Proxy a = Proxy

class NatToInt (n :: MyNat)
where natToInt :: Proxy (n :: MyNat) -> Int
instance NatToInt Z 
where natToInt _ = 0
instance (NatToInt n) => NatToInt (S n)
where natToInt _ = 1 + natToInt (Proxy :: Proxy n)

But this seems too Kind. I only ever want to supply Nats as arguments.

What does the `ArgKind' message mean?

(I've also seen messages with `AnyKind' -- what that?)

There's a discussion in SPJ's Records proposal last year 
http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Shouldg
ethaveaproxyargument
Is that related?

Do I need explicit Type/Kind application for this to work?

AntC




___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users