Changes between Version 1 and Version 2 of TypeNats/Naturals


Ignore:
Timestamp:
Jan 16, 2011 6:32:13 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Naturals

    v1 v2  
    11== Natural Numbers ==
    22
     3We may define the type of (value level) natural numbers in terms of singleton types.
     4The idea is that a natural number is, basically, an unknown singleton type.
     5This is why we use an existential construct in the definition:
    36{{{
    47data Natural = forall n . Natural !(Nat n)
    58
     9instance Enum Natural   
     10instance Eq Natural     
     11instance Integral Natural       
     12instance Num Natural     
     13instance Ord Natural     
     14instance Read Natural   
     15instance Real Natural   
     16instance Show Natural   
     17}}}
     18The instances make it possible to work with 'Naturals' as with any other numeric type.
     19Note, however, that some of the operations are partial.
     20For example, subtracting a larger number from a smaller one results in the undefined value of type ''Natural''.
     21
     22We also provide some functions for converting ''Interger'' values into their corresponding ''Natural'' ones.
     23We do this by using an intermediate representation for integers in terms of naturals, ''NaturalInteger''.  This type
     24is intended to be used only for the conversion.  While, in principle, we could provide numeric instances for the type,
     25we chose not to, because we would be duplicating functionality provided by the type 'Integer'.
     26
     27{{{
    628data NaturalInteger
    729  = Negative Natural
     
    1234subNatural :: Natural -> Natural -> NaturalInteger
    1335}}}
     36