Changes between Version 1 and Version 2 of TypeNtas/AlternativeSingletins


Ignore:
Timestamp:
Jan 16, 2011 5:20:45 PM (5 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