Kindness of strangers (or strangeness of Kinds)

[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 <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).
> 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 
> <http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper.pdf>
>
>
> Cheers,
> Pedro
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120608/cf0ac8fc/attachment.htm>