




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 