Kindness of strangers (or strangeness of Kinds)

Richard Eisenberg eir at cis.upenn.edu
Fri Jun 8 11:52:08 CEST 2012

```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

Richard

On 6/7/12 8:28 AM, José Pedro Magalhães wrote:
> Hi,
>
> On Thu, Jun 7, 2012 at 2:46 AM, AntC <anthony_clayden at clear.net.nz
> <mailto:anthony_clayden at 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).
>
> You might also want to have a look at Richard and Stephanie's latest
> 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
>
>
>
> _______________________________________________