Version 1 (modified by 9 years ago) (diff) | ,
---|

The only "magic" thing about `GHC.TypeNats`

are the instances of `TypeNat`

. The rest is implemented like this:

newtype Nat (n :: Nat) = Nat Integer natToInteger :: Nat n -> Integer natToInteger (Nat n) = n integerToNat :: Integer -> (forall n. Nat n -> a) -> a integerToNat n k = k (Nat n)

So, now we just need instances like these:

instance TypeNat 0 where nat = Nat 0 instance TypeNat 1 where nat = Nat 1 instance TypeNat 2 where nat = Nat 2 ...

Because we cannot generate this infinite family of instances, we have
some code in GHC which can solve `TypeNat`

predicates on the fly.

The "proof" (aka "dictionary") for `TypeNat n`

is just the number `n`

. This is OK because:

- GHC uses a
`newtype`

to represent the dictionaries for classes that have just a single method and no super-classes.`TypeNat`

is just such a class. `Nat`

is already a`newtype`

for`Integer`

.

Therefore, the dictionaries for class `TypeNat`

are just integers.