Changes between Version 2 and Version 3 of TypeNats/AlternativeSingletons


Ignore:
Timestamp:
Mar 21, 2012 1:46:20 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/AlternativeSingletons

    v2 v3  
    33In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct: 
    44{{{ 
    5 newtype Nat (n :: Nat) = Nat Integer 
     5newtypeT Nat (n :: Nat) = Nat Integer 
    66 
    77class NatI n where 
    8   nat :: Nat n 
     8  tNat :: TNat n 
    99 
    10 instance NatI 0 where nat = Nat 0 
    11 instance NatI 1 where nat = Nat 1 
     10instance NatI 0 where tNat = TNat 0 
     11instance NatI 1 where tNat = TNat 1 
    1212... 
    1313 
    14 natToInteger :: Nat n -> Integer 
    15 natToInteger (Nat n) = n 
     14tNatInteger :: TNat n -> Integer 
     15tNatInteger (TNat n) = n 
    1616}}} 
    1717 
    1818It is also possible to make the dual choice, where we provide a polymorphic constructor and an overloaded elimination construct: 
    1919{{{ 
    20 data Nat (n :: Nat) = Nat 
     20data TNat (n :: Nat) = TNat 
    2121 
    2222class NatE n where 
    23   natToInteger :: Nat n -> Integer 
     23  tNatInteger :: TNat n -> Integer 
    2424 
    25 instance NatE 0 where natToInteger Nat = 0 
    26 instance NatE 1 where natToInteger Nat = 1 
     25instance NatE 0 where tNatInteger TNat = 0 
     26instance NatE 1 where tNatInteger TNat = 1 
    2727... 
    2828}}} 
     
    3131 
    3232{{{ 
    33 data Nat1 (n :: Nat) = Nat 
     33data TNat1 (n :: Nat) = TNat1 
    3434 
    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 
     35tNat1Integer :: NatI n => TNat1 n -> Integer 
     36tNat1Integer = tNatInteger . cast 
     37  where cast :: NatI n => TNat1 n -> TNat n 
     38        cast TNat1 = tNat 
    3939}}}