Changes between Version 2 and Version 3 of TypeNtas/AlternativeSingletins


Ignore:
Timestamp:
Oct 4, 2015 11:01:03 AM (4 years ago)
Author:
bgamari
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNtas/AlternativeSingletins

    v2 v3  
    1 We use a family of singleton types to related type-level naturals to runtime values.
    2 
    3 In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct:
    4 {{{
    5 newtype Nat (n :: Nat) = Nat Integer
    6 
    7 class NatI n where
    8   nat :: NatI n
    9 
    10 instance NatI 0 where nat = Nat 0
    11 instance NatI 1 where nat = Nat 1
    12 ...
    13 
    14 natToInteger :: Nat n -> Integer
    15 natToInteger (Nat n) n = n
    16 }}}
    17 
    18 It is also possible to make the dual choice, where we provide a polymorphic constructor and an overloaded elimination construct:
    19 {{{
    20 data Nat (n :: Nat) = Nat
    21 
    22 class NatE n where
    23   natToInteger :: Nat n -> Integer
    24 
    25 instance NatE 0 where natToInteger Nat = 0
    26 instance NatE 1 where natToInteger Nat = 1
    27 ...
    28 }}}
    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:
    31 
    32 {{{
    33 data Nat1 (n :: Nat) = Nat
    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 
     1See [[TypeNats/AlternativeSingletons]].