Changes between Version 30 and Version 31 of TypeNats/Basics


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

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v30 v31  
    1616== Singleton Types == 
    1717 
    18 We use this idea to link the type-level literals to specific run-time values ''singleton types''. 
    19 The singleton types and some useful functions for working with them are defined in module {{{GHC.TypeLits}}}: 
     18We use this idea to link the type-level literals to specific run-time values via ''singleton types''. 
     19The singleton types and some useful functions for working with them are defined in module `GHC.TypeLits`: 
    2020 
    2121{{{ 
     
    2323}}} 
    2424 
    25 A //singleton type// is simply a type that has only one interesting inhabitant.  We define a whole family 
     25A singleton type is simply a type that has only one interesting inhabitant.  We define a whole family 
    2626of singleton types, parameterized by type-level literals: 
    2727{{{ 
     
    2929}}} 
    3030So, for example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all 
    31 singleton types.  The idea is that the only inhabitant of {{{Sing n}}} is the value {{{n}}}.  Notice 
    32 that {{{Sing}}} has a //polymorphic kind// because sometimes we apply it to numbers (which are of 
    33 kind {{{Nat}}}) and sometimes we apply it to symbols (which are of kind {{{Symbol}}}). 
     31singleton types.  The intuition is that the only inhabitant of `Sing n` is the value `n`.  Notice 
     32that `Sing` has a ''polymorphic kind'' because sometimes we apply it to numbers (which are of 
     33kind `Nat`) and sometimes we apply it to symbols (which are of kind `Symbol`). 
    3434 
    35 But, if we have a value of type {{{Sing a}}}, how do we get the actual integer or string? 
    36 We can do this with the function {{{fromSing}}}: 
     35But, if we have a value of type `Sing a`, how do we get the actual integer or string? 
     36We can do this with the function `fromSing`: 
    3737{{{ 
    3838fromSing :: Sing a -> SingRep a 
     
    4343}}} 
    4444 
    45 The function {{{fromSing}}} has an interesting type: it maps singletons to ordinary values, 
    46 but the type of the result depends on the //kind// of the index of the singleton. 
    47 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 singleton parameter. 
     47So, if we apply it to a value of type `Sing 3` we get the ''number'' `3`, but, 
     48if we apply it to a value of type `Sing "hello"` we would get the ''string'' `"hello"`. 
     49 
     50 
    4951 
    5052 
     
    6365The value of a singleton type may be named using {{{tNat}}}, which is a bit like a "smart" constructor for {{{TNat n}}}. 
    6466Note that because {{{tNat}}} is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example: 
    65 {{{ 
    66 > :set -XDataKinds 
    67 > tNatInteger (tNat :: TNat 3) 
    68 3 
    69 }}} 
    7067 
    7168One may think of the smart constructor {{{tNat}}} as being a method of a special built-in class, {{{NatI}}}: