Changes between Version 3 and Version 4 of TypeNats/Implementation

Show
Ignore:
Timestamp:
03/20/12 18:16:01 (15 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeNats/Implementation

    v3 v4  
    11The only "magic" thing about `GHC.TypeNats` are the instances of `NatI`.  The rest is implemented like this: 
    22{{{ 
    3 newtype Nat (n :: Nat) = Nat Integer 
     3newtype TNat (n :: Nat) = TNat Integer 
    44 
    5 natToInteger :: Nat n -> Integer 
    6 natToInteger (Nat n) = n 
     5tNatInteger :: TNat n -> Integer 
     6tNatInteger (TNat n) = n 
    77}}} 
    88 
    99So, now we just need instances like these: 
    1010{{{ 
    11 instance NatI 0 where nat = Nat 0 
    12 instance NatI 1 where nat = Nat 1 
    13 instance NatI 2 where nat = Nat 2 
     11instance NatI 0 where nat = TNat 0 
     12instance NatI 1 where nat = TNat 1 
     13instance NatI 2 where nat = TNat 2 
    1414... 
    1515}}} 
    … …  
    2121 
    2222  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. 
    23   2. `Nat` is already a `newtype` for `Integer`. 
     23  2. `TNat` is already a `newtype` for `Integer`. 
    2424 
    2525Therefore, the dictionaries for class `NatI` are just integers.