type-nats/alternative-singletons.md

+
+We use a family of singleton types to related type-level 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