Version 4 (modified by diatchki, 2 years ago) (diff) |
---|

The only "magic" thing about `GHC.TypeNats` are the instances of `NatI`. The rest is implemented like this:

newtype TNat (n :: Nat) = TNat Integer tNatInteger :: TNat n -> Integer tNatInteger (TNat n) = n

So, now we just need instances like these:

instance NatI 0 where nat = TNat 0 instance NatI 1 where nat = TNat 1 instance NatI 2 where nat = TNat 2 ...

Because we cannot generate this infinite family of instances, we have
some code in GHC which can solve `NatI` predicates on the fly.

The "proof" (aka "dictionary") for `NatI 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.`NatI`is just such a class. `TNat`is already a`newtype`for`Integer`.

Therefore, the dictionaries for class `NatI` are just integers.