Changes between Version 2 and Version 3 of TypeNats/AlternativeSingletons
 Timestamp:
 Mar 21, 2012 1:46:20 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/AlternativeSingletons
v2 v3 3 3 In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct: 4 4 {{{ 5 newtype Nat (n :: Nat) = Nat Integer5 newtypeT Nat (n :: Nat) = Nat Integer 6 6 7 7 class NatI n where 8 nat ::Nat n8 tNat :: TNat n 9 9 10 instance NatI 0 where nat =Nat 011 instance NatI 1 where nat =Nat 110 instance NatI 0 where tNat = TNat 0 11 instance NatI 1 where tNat = TNat 1 12 12 ... 13 13 14 natToInteger ::Nat n > Integer15 natToInteger (Nat n) = n14 tNatInteger :: TNat n > Integer 15 tNatInteger (TNat 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 Nat (n :: Nat) =Nat20 data TNat (n :: Nat) = TNat 21 21 22 22 class NatE n where 23 natToInteger ::Nat n > Integer23 tNatInteger :: TNat n > Integer 24 24 25 instance NatE 0 where natToIntegerNat = 026 instance NatE 1 where natToIntegerNat = 125 instance NatE 0 where tNatInteger TNat = 0 26 instance NatE 1 where tNatInteger TNat = 1 27 27 ... 28 28 }}} … … 31 31 32 32 {{{ 33 data Nat1 (n :: Nat) = Nat33 data TNat1 (n :: Nat) = TNat1 34 34 35 nat1ToInteger :: NatI n =>Nat1 n > Integer36 nat1ToInteger x = natToInteger (cast nat x) 37 where cast :: Nat n > Nat1 n >Nat n38 cast x Nat = x35 tNat1Integer :: NatI n => TNat1 n > Integer 36 tNat1Integer = tNatInteger . cast 37 where cast :: NatI n => TNat1 n > TNat n 38 cast TNat1 = tNat 39 39 }}}