Changes between Version 5 and Version 6 of TypeNats/Implementation
 Timestamp:
 Apr 9, 2012 2:23:51 AM (2 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Implementation
v5 v6 1 The only "magic" thing about `GHC.TypeLits` are the instances of ` NatI`. The rest is implemented like this:1 The only "magic" thing about `GHC.TypeLits` are the instances of `SingI`. The rest is implemented like this: 2 2 {{{ 3 newtype TNat (n :: Nat) = TNat Integer3 newtype Sing n = Sing (SingRep n) 4 4 5 tNatInteger :: TNat n > Integer 6 tNatInteger (TNat n) = n 5 type family SingRep a 6 type instance SingRep (n :: Nat) = Integer 7 type instance SingRep (n :: Symbol) = String 8 9 fromSing :: Sing n > SingRep n 10 fromSing (Sing n) = n 7 11 }}} 8 12 9 13 So, now we just need instances like these: 10 14 {{{ 11 instance NatI 0 where nat = TNat012 instance NatI 1 where nat = TNat113 instance NatI 2 where nat = TNat 215 instance SingI 0 where sing = Sing 0 16 instance SingI 1 where sing = Sing 1 17 instance SingI "hello" where sing = Sing "hello" 14 18 ... 15 19 }}} 16 20 17 21 Because we cannot generate this infinite family of instances, we have 18 some code in GHC which can solve ` NatI` predicates on the fly.22 some code in GHC which can solve `SingI` predicates on the fly. 19 23 20 The "proof" (aka "dictionary") for ` NatI n` is just the number`n`. This is OK because:24 The "proof" (aka "dictionary") for `SingI n` is just the number (or string) `n`. This is OK because: 21 25 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. ` TNat` is already a `newtype` for `Integer`.26 1. GHC uses a `newtype` to represent the dictionaries for classes that have just a single method and no superclasses. `SingI` is just such a class. 27 2. `Sing` is already a `newtype` for `Integer` or `String`, depending on the kind of its parameter. 24 28 25 Therefore, the dictionaries for class ` NatI` are just integers.29 Therefore, the dictionaries for class `SingI` are just integers or strings, depending on the kind of the parameter. 26 30 27 31