Changes between Version 2 and Version 3 of TypeNats/Implementation


Ignore:
Timestamp:
Jan 27, 2011 6:12:15 AM (5 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