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}}}