Changes between Version 2 and Version 3 of TypeNats/Implementation
 Timestamp:
 Jan 27, 2011 6:12:15 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Implementation
v2 v3 1 The only "magic" thing about `GHC.TypeNats` are the instances of ` TypeNat`. The rest is implemented like this:1 The only "magic" thing about `GHC.TypeNats` are the instances of `NatI`. The rest is implemented like this: 2 2 {{{ 3 3 newtype Nat (n :: Nat) = Nat Integer … … 9 9 So, now we just need instances like these: 10 10 {{{ 11 instance TypeNat0 where nat = Nat 012 instance TypeNat1 where nat = Nat 113 instance TypeNat2 where nat = Nat 211 instance NatI 0 where nat = Nat 0 12 instance NatI 1 where nat = Nat 1 13 instance NatI 2 where nat = Nat 2 14 14 ... 15 15 }}} 16 16 17 17 Because we cannot generate this infinite family of instances, we have 18 some code in GHC which can solve ` TypeNat` predicates on the fly.18 some code in GHC which can solve `NatI` predicates on the fly. 19 19 20 The "proof" (aka "dictionary") for ` TypeNatn` is just the number `n`. This is OK because:20 The "proof" (aka "dictionary") for `NatI n` is just the number `n`. This is OK because: 21 21 22 1. GHC uses a `newtype` to represent the dictionaries for classes that have just a single method and no superclasses. ` TypeNat` is just such a class.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 23 2. `Nat` is already a `newtype` for `Integer`. 24 24 25 Therefore, the dictionaries for class ` TypeNat` are just integers.25 Therefore, the dictionaries for class `NatI` are just integers. 26 26 27 27