Version 2 (modified by diatchki, 5 years ago) (diff) |
---|

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:

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:

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:

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