Changes between Version 1 and Version 2 of TypeNtas/AlternativeSingletins
 Timestamp:
 Jan 16, 2011 5:20:45 PM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNtas/AlternativeSingletins
v1 v2 1 1 We use a family of singleton types to related typelevel naturals to runtime values. 2 2 3 In our design, we chose to provide a n overloaded "smart" constructor and a polymorphic elimination construct:3 In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct: 4 4 {{{ 5 5 newtype Nat (n :: Nat) = Nat Integer … … 28 28 }}} 29 29 30 We made this choice, at least in part, because it made the implementation simpler: 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 31 32 {{{ 33 data Nat1 (n :: Nat) = Nat 31 34 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 39 }}} 40