Changes between Version 2 and Version 3 of TypeNats/Implementation


Ignore:
Timestamp:
Jan 27, 2011 6:12:15 AM (3 years ago)
Author:
diatchki
Comment:

--

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: 
     1The only "magic" thing about `GHC.TypeNats` are the instances of `NatI`.  The rest is implemented like this: 
    22{{{ 
    33newtype Nat (n :: Nat) = Nat Integer 
     
    99So, now we just need instances like these: 
    1010{{{ 
    11 instance TypeNat 0 where nat = Nat 0 
    12 instance TypeNat 1 where nat = Nat 1 
    13 instance TypeNat 2 where nat = Nat 2 
     11instance NatI 0 where nat = Nat 0 
     12instance NatI 1 where nat = Nat 1 
     13instance NatI 2 where nat = Nat 2 
    1414... 
    1515}}} 
    1616 
    1717Because we cannot generate this infinite family of instances, we have 
    18 some code in GHC which can solve `TypeNat` predicates on the fly. 
     18some code in GHC which can solve `NatI` predicates on the fly. 
    1919 
    20 The "proof" (aka "dictionary") for `TypeNat n` is just the number `n`.  This is OK because: 
     20The "proof" (aka "dictionary") for `NatI n` is just the number `n`.  This is OK because: 
    2121 
    22   1. GHC uses a `newtype` to represent the dictionaries for classes that have just a single method and no super-classes.  `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 super-classes.  `NatI` is just such a class. 
    2323  2. `Nat` is already a `newtype` for `Integer`. 
    2424 
    25 Therefore, the dictionaries for class `TypeNat` are just integers. 
     25Therefore, the dictionaries for class `NatI` are just integers. 
    2626 
    2727