Changes between Version 41 and Version 42 of TypeNats/Basics


Ignore:
Timestamp:
Oct 16, 2012 5:28:33 AM (19 months 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