Changes between Version 28 and Version 29 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 1:20:55 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v28 v29  
    66
    77{{{
    8 0, 1, 2, ... :: Nat
     80, 1, 2, ...                            :: Nat
    99"hello", "world", "some string literal" :: Symbol
    1010}}}
     
    4343}}}
    4444
    45 While the type of {{{fromSing}}} looks a bit complex at first it is actually quite simple:
    46 given a singleton type, it will return either an integer or a string, depending on the //kind// of
    47 its index.  So, if we apply it to a value of type {{{Sing 3}}} we would get the number {{{3}}}, but,
    48 if we apply to a value of type {{{Sing "hello"}}} we would get the string "hello".
     45The function {{{fromSing}}} has an interesting type: it maps singletons to ordinary values,
     46but the type of the result depends on the //kind// of the index of the singleton.
     47So, if we apply it to a value of type {{{Sing 3}}} we would get the //number// {{{3}}}, but,
     48if we apply to a value of type {{{Sing "hello"}}} we would get the //string// "hello".
    4949
    5050