Changes between Version 30 and Version 31 of TypeNats/Basics
 Timestamp:
 Apr 9, 2012 1:27:09 AM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v30 v31 16 16 == Singleton Types == 17 17 18 We use this idea to link the typelevel literals to specific runtime values ''singleton types''.19 The singleton types and some useful functions for working with them are defined in module {{{GHC.TypeLits}}}:18 We use this idea to link the typelevel literals to specific runtime values via ''singleton types''. 19 The singleton types and some useful functions for working with them are defined in module `GHC.TypeLits`: 20 20 21 21 {{{ … … 23 23 }}} 24 24 25 A //singleton type//is simply a type that has only one interesting inhabitant. We define a whole family25 A singleton type is simply a type that has only one interesting inhabitant. We define a whole family 26 26 of singleton types, parameterized by typelevel literals: 27 27 {{{ … … 29 29 }}} 30 30 So, for example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all 31 singleton types. The i dea is that the only inhabitant of {{{Sing n}}} is the value {{{n}}}. Notice32 that {{{Sing}}} has a //polymorphic kind//because sometimes we apply it to numbers (which are of33 kind {{{Nat}}}) and sometimes we apply it to symbols (which are of kind {{{Symbol}}}).31 singleton types. The intuition 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`). 34 34 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}}}: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`: 37 37 {{{ 38 38 fromSing :: Sing a > SingRep a … … 43 43 }}} 44 44 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". 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 singleton parameter. 47 So, if we apply it to a value of type `Sing 3` we get the ''number'' `3`, but, 48 if we apply it to a value of type `Sing "hello"` we would get the ''string'' `"hello"`. 49 50 49 51 50 52 … … 63 65 The value of a singleton type may be named using {{{tNat}}}, which is a bit like a "smart" constructor for {{{TNat n}}}. 64 66 Note that because {{{tNat}}} is polymorphic, we may have to use a type signature to specify which singleton we mean. For example: 65 {{{66 > :set XDataKinds67 > tNatInteger (tNat :: TNat 3)68 369 }}}70 67 71 68 One may think of the smart constructor {{{tNat}}} as being a method of a special builtin class, {{{NatI}}}: