# Changes between Version 4 and Version 5 of TypeNats/AlternativeSingletons

Show
Ignore:
Timestamp:
04/08/12 19:20:05 (13 months ago)
Comment:

--

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