Re: Kindness of strangers (or strangeness of Kinds)

7 Jun 2012

       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