# Changes between Version 2 and Version 3 of TypeNats/AlternativeSingletons

Show
Ignore:
Timestamp:
03/20/12 18:46:20 (14 months ago)
Comment:

--

Unmodified
Removed
Modified
• ## TypeNats/AlternativeSingletons

v2 v3
33In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct:
44{{{
5 newtype Nat (n :: Nat) = Nat Integer
5newtypeT Nat (n :: Nat) = Nat Integer
66
77class NatI n where
8   nat :: Nat n
8  tNat :: TNat n
99
10 instance NatI 0 where nat = Nat 0
11 instance NatI 1 where nat = Nat 1
10instance NatI 0 where tNat = TNat 0
11instance NatI 1 where tNat = TNat 1
1212...
1313
14 natToInteger :: Nat n -> Integer
15 natToInteger (Nat n) = n
14tNatInteger :: TNat n -> Integer
15tNatInteger (TNat 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 Nat (n :: Nat) = Nat
20data TNat (n :: Nat) = TNat
2121
2222class NatE n where
23   natToInteger :: Nat n -> Integer
23  tNatInteger :: TNat n -> Integer
2424
25 instance NatE 0 where natToInteger Nat = 0
26 instance NatE 1 where natToInteger Nat = 1
25instance NatE 0 where tNatInteger TNat = 0
26instance NatE 1 where tNatInteger TNat = 1
2727...
2828}}}

3131
3232{{{
33 data Nat1 (n :: Nat) = Nat
33data TNat1 (n :: Nat) = TNat1
3434
35 nat1ToInteger :: NatI n => Nat1 n -> Integer
36 nat1ToInteger x = natToInteger (cast nat x)
37   where cast :: Nat n -> Nat1 n -> Nat n
38         cast x Nat = x
35tNat1Integer :: NatI n => TNat1 n -> Integer
36tNat1Integer = tNatInteger . cast
37  where cast :: NatI n => TNat1 n -> TNat n
38        cast TNat1 = tNat
3939}}}