Changes between Version 4 and Version 5 of TypeNats/AlternativeSingletons


Ignore:
Timestamp:
Apr 9, 2012 2:20:05 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/AlternativeSingletons

    v4 v5  
    33In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct: 
    44{{{ 
    5 newtypeT Nat (n :: Nat) = Nat Integer 
     5newtype Sing n = Sing (SingRep n) 
    66 
    7 class NatI n where 
    8   tNat :: TNat n 
     7class SingI n where 
     8  sing :: Sing n 
    99 
    10 instance NatI 0 where tNat = TNat 0 
    11 instance NatI 1 where tNat = TNat 1 
     10instance SingI 0 where sing = Sing 0 
     11instance SingI 1 where sing = Sing 1 
    1212... 
    1313 
    14 tNatInteger :: TNat n -> Integer 
    15 tNatInteger (TNat n) = n 
     14fromSing :: Sing n -> SingRep n 
     15fromSing (Sing n) = n 
    1616}}} 
    1717 
    1818It is also possible to make the dual choice, where we provide a polymorphic constructor and an overloaded elimination construct: 
    1919{{{ 
    20 data TNat (n :: Nat) = TNat 
     20data Sing n = Sing 
    2121 
    22 class NatE n where 
    23   tNatInteger :: TNat n -> Integer 
     22class SingE n where 
     23  fromSing :: Sing n -> SingRep n 
    2424 
    25 instance NatE 0 where tNatInteger TNat = 0 
    26 instance NatE 1 where tNatInteger TNat = 1 
     25instance NatE 0 where fromSing Sing = 0 
     26instance NatE 1 where fromSing Sing = 1 
    2727... 
    2828}}} 
    2929 
    30 We made this choice, at least in part, because it made the implementation simpler: with our choice the evidence for class {{{NatI}}} is just an integer.  Note that our choice does not loose any generality because we can define the alternative design in terms of it: 
     30We made this choice, at least in part, because it made the implementation simpler: with our choice the evidence for class {{{SingI}}} is just an integer or a string.  Note that our choice does not loose any generality because we can define the alternative design in terms of it: 
    3131 
    3232{{{ 
    33 data TNat1 (n :: Nat) = TNat1 
     33data Sing1 = Sing1 
    3434 
    35 tNat1Integer :: NatI n => TNat1 n -> Integer 
    36 tNat1Integer = tNatInteger . cast 
    37   where cast :: NatI n => TNat1 n -> TNat n 
    38         cast TNat1 = tNat 
     35fromSing1 :: SingI n => Sing1 n -> SingRep n 
     36fromSing1 = fromSing . cast 
     37  where cast :: SingI n => Sing1 n -> Sing n 
     38        cast Sing1 = sing 
    3939}}}