Changes between Version 31 and Version 32 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 1:39:19 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v31 v32  
    2828newtype Sing :: a -> * 
    2929}}} 
    30 So, for example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all 
     30For example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all 
    3131singleton types.  The intuition is that the only inhabitant of `Sing n` is the value `n`.  Notice 
    3232that `Sing` has a ''polymorphic kind'' because sometimes we apply it to numbers (which are of 
     
    4747So, if we apply it to a value of type `Sing 3` we get the ''number'' `3`, but, 
    4848if we apply it to a value of type `Sing "hello"` we would get the ''string'' `"hello"`. 
     49 
     50So, how do we make values of type `Sing n` in the first place?  This is done with 
     51a the special overloaded constant `sing`: 
     52{{{ 
     53class SingI a where 
     54  sing :: Sing a 
     55 
     56-- Built-in instances for all type0literals. 
     57instance SingI 0        where sing = // ... the singleton value representing 0 ... 
     58instance SingI 1        where sing = // ... the singleton value representing 1 ... 
     59instance SingI "hello"  where sing = // ... the singleton value representing "hello" ... 
     60// ... etc. 
     61}}} 
    4962 
    5063