






We use a family of singleton types to related typelevel naturals to runtime values.












In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct:








```wiki




newtype Nat (n :: Nat) = Nat Integer








class NatI n where




nat :: NatI n








instance NatI 0 where nat = Nat 0




instance NatI 1 where nat = Nat 1




...








natToInteger :: Nat n > Integer




natToInteger (Nat n) n = n




```












It is also possible to make the dual choice, where we provide a polymorphic constructor and an overloaded elimination construct:








```wiki




data Nat (n :: Nat) = Nat








class NatE n where




natToInteger :: Nat n > Integer








instance NatE 0 where natToInteger Nat = 0




instance NatE 1 where natToInteger Nat = 1




...




```












We made this choice, at least in part, because it made the implementation simpler: the evidence for class `NatI` is just an integer. Note that our choice does not loose any generality because we can define the alternative design in terms of it:








```wiki




data Nat1 (n :: Nat) = Nat








nat1ToInteger :: NatI n => Nat1 n > Integer




nat1ToInteger x = natToInteger (cast nat x)




where cast :: Nat n > Nat1 n > Nat n




cast x Nat = x




``` 



\ No newline at end of file 