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

We use a family of singleton types to relate type-level naturals to runtime values.

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

newtypeT Nat (n :: Nat) = Nat Integer class NatI n where tNat :: TNat n instance NatI 0 where tNat = TNat 0 instance NatI 1 where tNat = TNat 1 ... 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:

data TNat (n :: Nat) = TNat class NatE n where tNatInteger :: TNat n -> Integer 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:

data TNat1 (n :: Nat) = TNat1 tNat1Integer :: NatI n => TNat1 n -> Integer tNat1Integer = tNatInteger . cast where cast :: NatI n => TNat1 n -> TNat n cast TNat1 = tNat