|Version 4 (modified by 5 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
newtypeto represent the dictionaries for classes that have just a single method and no super-classes.
NatIis just such a class.
TNatis already a
Therefore, the dictionaries for class
NatI are just integers.