Changes between Version 3 and Version 4 of TypeNats/Implementation
 Timestamp:
 Mar 21, 2012 1:16:01 AM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Implementation
v3 v4 1 1 The only "magic" thing about `GHC.TypeNats` are the instances of `NatI`. The rest is implemented like this: 2 2 {{{ 3 newtype Nat (n :: Nat) =Nat Integer3 newtype TNat (n :: Nat) = TNat Integer 4 4 5 natToInteger ::Nat n > Integer6 natToInteger (Nat n) = n5 tNatInteger :: TNat n > Integer 6 tNatInteger (TNat n) = n 7 7 }}} 8 8 9 9 So, now we just need instances like these: 10 10 {{{ 11 instance NatI 0 where nat = Nat 012 instance NatI 1 where nat = Nat 113 instance NatI 2 where nat = Nat 211 instance NatI 0 where nat = TNat 0 12 instance NatI 1 where nat = TNat 1 13 instance NatI 2 where nat = TNat 2 14 14 ... 15 15 }}} … … 21 21 22 22 1. GHC uses a `newtype` to represent the dictionaries for classes that have just a single method and no superclasses. `NatI` is just such a class. 23 2. ` Nat` is already a `newtype` for `Integer`.23 2. `TNat` is already a `newtype` for `Integer`. 24 24 25 25 Therefore, the dictionaries for class `NatI` are just integers.