Version 4 (modified by diatchki, 6 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