Changes between Version 8 and Version 9 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 5:54:12 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v8 v9  
    2121}}} 
    2222The only "interesting" value of type ''Nat n'' is the number ''n''.  Technically, there is also an undefined element. 
     23The value of a singleton type may be named using ''nat'', which is a bit like a "smart" constructor for ''Nat n''. 
     24Note that because ''nat'' is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example: 
     25{{{ 
     26> natToInteger (nat :: Nat 3) 
     273 
     28}}} 
    2329 
    24 One may think of the smart constructor ''nat'' as being a method of a special built-in class: 
     30One may think of the smart constructor ''nat'' as being a method of a special built-in class, ''NatI'': 
    2531{{{ 
    2632class NatI n where 
     
    3238etc. 
    3339}}} 
     40 
     41The name ''NatI'' is a mnemonic for the different uses of the class: 
     42  * It is the ''introduction'' construct for 'Nat' values, 
     43  * It is an ''implicit'' parameter of kind 'Nat' (link) 
     44 
    3445 
    3546