Changes between Version 5 and Version 6 of TypeNats/Implementation


Ignore:
Timestamp:
Apr 9, 2012 2:23:51 AM (2 years ago)
Author:
diatchki
Comment:

--

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: 
     1The only "magic" thing about `GHC.TypeLits` are the instances of `SingI`.  The rest is implemented like this: 
    22{{{ 
    3 newtype TNat (n :: Nat) = TNat Integer 
     3newtype Sing n = Sing (SingRep n) 
    44 
    5 tNatInteger :: TNat n -> Integer 
    6 tNatInteger (TNat n) = n 
     5type family SingRep a 
     6type instance SingRep (n :: Nat) = Integer 
     7type instance SingRep (n :: Symbol) = String 
     8 
     9fromSing :: Sing n -> SingRep n  
     10fromSing (Sing n) = n 
    711}}} 
    812 
    913So, now we just need instances like these: 
    1014{{{ 
    11 instance NatI 0 where nat = TNat 0 
    12 instance NatI 1 where nat = TNat 1 
    13 instance NatI 2 where nat = TNat 2 
     15instance SingI 0       where sing = Sing 0 
     16instance SingI 1       where sing = Sing 1 
     17instance SingI "hello" where sing = Sing "hello" 
    1418... 
    1519}}} 
    1620 
    1721Because we cannot generate this infinite family of instances, we have 
    18 some code in GHC which can solve `NatI` predicates on the fly. 
     22some code in GHC which can solve `SingI` predicates on the fly. 
    1923 
    20 The "proof" (aka "dictionary") for `NatI n` is just the number `n`.  This is OK because: 
     24The "proof" (aka "dictionary") for `SingI n` is just the number (or string) `n`.  This is OK because: 
    2125 
    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. 
    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 super-classes.  `SingI` is just such a class. 
     27  2. `Sing` is already a `newtype` for `Integer` or `String`, depending on the kind of its parameter. 
    2428 
    25 Therefore, the dictionaries for class `NatI` are just integers. 
     29Therefore, the dictionaries for class `SingI` are just integers or strings, depending on the kind of the parameter. 
    2630 
    2731