Changes between Version 41 and Version 42 of TypeNats/Basics


Ignore:
Timestamp:
Oct 16, 2012 5:28:33 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v41 v42  
    3333kind `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 overloaded function `fromSing`.  Its type is quite general because
    37 it can support various singleton families, but for the purposes of this explanation
    38 it is sufficient t
    39 
    40 {{{
    41 fromSing :: Sing (a :: Nat) -> Integer
    42 fromSing :: Sing (a :: Symbol) -> String
    43 }}}
    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 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 get the ''string'' `"hello"`.
    49 
    50 So, how do we make values of type `Sing n` in the first place?  This is done with
     35So, how do we make values of type `Sing n`?  This is done with
    5136the special overloaded constant `sing`:
    5237{{{
     
    7358  * It is the ''introduction'' construct for 'Sing' values,
    7459  * It is an ''implicit'' singleton parameter (this is discussed in more detail bellow)
     60
     61
     62It is also useful to get the actual integer or string associated with a singleton.
     63We can do this with the overloaded function `fromSing`.  Its type is quite general because
     64it can support various singleton families, but to start, consider the following two instances
     65of its type:
     66{{{
     67fromSing :: Sing (a :: Nat) -> Integer
     68fromSing :: Sing (a :: Symbol) -> String
     69}}}
     70
     71Notice that the return type of the function is determined by the ''kind'' of the
     72singleton family, not the concrete type.  For example, for any type `n` of
     73kind `Nat` we get an `Integer`, while for any type `s` of kind `Symbol` we get a
     74string.  Based on this idea, here is a more general type for `fromSing`:
     75{{{
     76fromSing :: SingE (KindOf a) => Sing a -> Demote a
     77}}}
     78
    7579
    7680Notice that GHCi could display values of type `Sing`, so they have a `Show` instance.  As another example, here