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_clay...@clear.net.nz
<mailto:anthony_clay...@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
