type-nats/alternative-singletons.md

@@ -5,41 +5,41 @@ We use a family of singleton types to relate type-level 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