Changes between Version 8 and Version 9 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 5:54:12 PM (5 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