|Version 4 (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: 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:
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