Changes between Version 3 and Version 4 of TypeNats/Implementation


Ignore:
Timestamp:
Mar 21, 2012 1:16:01 AM (3 years 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.