Changes between Version 5 and Version 6 of TypeNats/Implementation


Ignore:
Timestamp:
Apr 9, 2012 2:23:51 AM (3 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