...  @@ 5,41 +5,41 @@ We use a family of singleton types to relate typelevel naturals to runtime valu 
...  @@ 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:


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






```wiki


```wiki


newtype Nat (n :: Nat) = Nat Integer


newtypeT Nat (n :: Nat) = Nat Integer






class NatI n where


class NatI n where


nat :: Nat n


tNat :: TNat n






instance NatI 0 where nat = Nat 0


instance NatI 0 where tNat = TNat 0


instance NatI 1 where nat = Nat 1


instance NatI 1 where tNat = TNat 1


...


...






natToInteger :: Nat n > Integer


tNatInteger :: TNat n > Integer


natToInteger (Nat n) = n


tNatInteger (TNat n) = n


```


```










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


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






```wiki


```wiki


data Nat (n :: Nat) = Nat


data TNat (n :: Nat) = TNat






class NatE n where


class NatE n where


natToInteger :: Nat n > Integer


tNatInteger :: TNat n > Integer






instance NatE 0 where natToInteger Nat = 0


instance NatE 0 where tNatInteger TNat = 0


instance NatE 1 where natToInteger Nat = 1


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


```wiki


data Nat1 (n :: Nat) = Nat


data TNat1 (n :: Nat) = TNat1






nat1ToInteger :: NatI n => Nat1 n > Integer


tNat1Integer :: NatI n => TNat1 n > Integer


nat1ToInteger x = natToInteger (cast nat x)


tNat1Integer = tNatInteger . cast


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


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


cast x Nat = x


cast TNat1 = tNat


``` 

``` 



\ No newline at end of file 