|Version 1 (modified by diatchki, 6 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.