...  ...  @@ 5,41 +5,41 @@ We use a family of singleton types to relate typelevel naturals to runtime valu 


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



newtypeT Nat (n :: Nat) = Nat Integer






class NatI n where



nat :: Nat n



tNat :: TNat n






instance NatI 0 where nat = Nat 0



instance NatI 1 where nat = Nat 1



instance NatI 0 where tNat = TNat 0



instance NatI 1 where tNat = TNat 1



...






natToInteger :: Nat n > Integer



natToInteger (Nat n) = n



tNatInteger :: TNat n > Integer



tNatInteger (TNat 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



data TNat (n :: Nat) = TNat






class NatE n where



natToInteger :: Nat n > Integer



tNatInteger :: TNat n > Integer






instance NatE 0 where natToInteger Nat = 0



instance NatE 1 where natToInteger Nat = 1



instance NatE 0 where tNatInteger TNat = 0



instance NatE 1 where tNatInteger TNat = 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:



We made this choice, at least in part, because it made the implementation simpler: with our choice 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



data TNat1 (n :: Nat) = TNat1






nat1ToInteger :: NatI n => Nat1 n > Integer



nat1ToInteger x = natToInteger (cast nat x)



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



cast x Nat = x



tNat1Integer :: NatI n => TNat1 n > Integer



tNat1Integer = tNatInteger . cast



where cast :: NatI n => TNat1 n > TNat n



cast TNat1 = tNat



``` 


\ No newline at end of file 