Changes between Version 2 and Version 3 of TypeNats/AlternativeSingletons


Ignore:
Timestamp:
Mar 21, 2012 1:46:20 AM (3 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}}}