Changes between Version 30 and Version 31 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 1:27:09 AM (3 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}}}: