Changes between Version 1 and Version 2 of TypeNats/Naturals


Ignore:
Timestamp:
Jan 16, 2011 6:32:13 PM (3 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