Re: Kindness of strangers (or strangeness of Kinds)

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