writes:

Quoting AntC :

...

{-# 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

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 otherway around; I can't remember). http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsu...

José Pedro Magalhães writes: 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

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-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@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 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

On Mon, Jun 11, 2012 at 9:58 PM, AntC wrote:

Simon Peyton-Jones writes:

...

There is a little, ill-documented, sub-kind hierarchy in GHC. I'm trying

...

possible, and it is much less important than it used to be. It's always been

hard to get rid of it as much as 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

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 mailto:anthony_clayden@clear.net.nz> 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#Kindsu...

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 http://www.cis.upenn.edu/%7Eeir/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

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