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