Changes between Version 4 and Version 5 of TypeNats/AlternativeSingletons
 Timestamp:
 Apr 9, 2012 2:20:05 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/AlternativeSingletons
v4 v5 3 3 In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct: 4 4 {{{ 5 newtype T Nat (n :: Nat) = Nat Integer5 newtype Sing n = Sing (SingRep n) 6 6 7 class NatI n where8 tNat :: TNatn7 class SingI n where 8 sing :: Sing n 9 9 10 instance NatI 0 where tNat = TNat011 instance NatI 1 where tNat = TNat110 instance SingI 0 where sing = Sing 0 11 instance SingI 1 where sing = Sing 1 12 12 ... 13 13 14 tNatInteger :: TNat n > Integer 15 tNatInteger (TNatn) = n14 fromSing :: Sing n > SingRep n 15 fromSing (Sing n) = n 16 16 }}} 17 17 18 18 It is also possible to make the dual choice, where we provide a polymorphic constructor and an overloaded elimination construct: 19 19 {{{ 20 data TNat (n :: Nat) = TNat20 data Sing n = Sing 21 21 22 class NatE n where23 tNatInteger :: TNat n > Integer22 class SingE n where 23 fromSing :: Sing n > SingRep n 24 24 25 instance NatE 0 where tNatInteger TNat= 026 instance NatE 1 where tNatInteger TNat= 125 instance NatE 0 where fromSing Sing = 0 26 instance NatE 1 where fromSing Sing = 1 27 27 ... 28 28 }}} 29 29 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:30 We 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: 31 31 32 32 {{{ 33 data TNat1 (n :: Nat) = TNat133 data Sing1 = Sing1 34 34 35 tNat1Integer :: NatI n => TNat1 n > Integer 36 tNat1Integer = tNatInteger. cast37 where cast :: NatI n => TNat1 n > TNatn38 cast TNat1 = tNat35 fromSing1 :: SingI n => Sing1 n > SingRep n 36 fromSing1 = fromSing . cast 37 where cast :: SingI n => Sing1 n > Sing n 38 cast Sing1 = sing 39 39 }}}