Changes between Version 31 and Version 32 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 1:39:19 AM (3 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