[Haskell-cafe] Type-level Nat to Integer

Gautier DI FOLCO gautier.difolco at gmail.com
Thu Jul 3 21:03:18 UTC 2014

Hi all,

I'm trying to change type-level Nat to Integer as following:
{-# LANGUAGE DataKinds, KindSignatures, GADTs, PolyKinds #-}

data Nat = Z | S Nat

class NatToInt n where
    natToInt :: n -> Int

instance NatToInt Z where
    natToInt _ = 0

instance NatToInt (S n) where
    natToInt = 1 + natToInt (undefined :: n)

I understand why it fails (Z and S have not the right kind).
How to specify that NatToInt is Nat-specific?
Moreover, if you have any advanced explanations/links which could give me a
deeper understanding on what going on, I'll take them.

Thanks in advance for your help.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140703/74de80b3/attachment.html>

More information about the Haskell-Cafe mailing list