Changes between Version 1 and Version 2 of TypeNtas/AlternativeSingletins


Ignore:
Timestamp:
Jan 16, 2011 5:20:45 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNtas/AlternativeSingletins

    v1 v2  
    11We use a family of singleton types to related type-level naturals to runtime values. 
    22 
    3 In our design, we chose to provide an overloaded "smart" constructor and a polymorphic elimination construct: 
     3In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct: 
    44{{{ 
    55newtype Nat (n :: Nat) = Nat Integer 
     
    2828}}} 
    2929 
     30We 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: 
    3031 
     32{{{ 
     33data Nat1 (n :: Nat) = Nat 
    3134 
     35nat1ToInteger :: NatI n => Nat1 n -> Integer 
     36nat1ToInteger x = natToInteger (cast nat x) 
     37  where cast :: Nat n -> Nat1 n -> Nat n 
     38        cast x Nat = x 
     39}}} 
     40