Changes between Version 33 and Version 34 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 2:13:08 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v33 v34  
    127127 
    128128 
    129  
    130  
    131  
    132  
    133  
    134 == Examples == 
    135  
    136 Here is how we can use the basic primitives to define a {{{Show}}} instance for singleton types: 
    137 {{{ 
    138 instance Show (TNat n) where 
    139   showsPrec p n = showsPrec p (tNatInteger n) 
    140 }}} 
    141  
    142 Here is how to define a {{{Read}}} instance: 
    143 {{{ 
    144 instance NatI n => Read (Nat n) where 
    145   readsPrec p x       = do (x,xs) <- readsPrec p x 
    146                            case tNatThat (== x) of 
    147                              Just n  -> [(n,xs)] 
    148                              Nothing -> [] 
    149 }}} 
    150  
    151 The derived function {{{tNatThat}}} is similar to {{{tNat}}} except that it succeeds only if the integer representation 
    152 of the singleton type matches the given predicate.  So, in the {{{Read}}} instance we parse an integer and then we check 
    153 if it is the expected integer for the singleton that we are trying to parse. 
    154  
    155  
    156129== Implicit vs. Explicit Parameters == 
    157130 
    158 There are two different styles of writing functions which need the integer corresponding to a type level natural. 
     131There are two different styles of writing functions that use singleton types. 
    159132To illustrate the two style consider a type for working with C-style arrays: 
    160133{{{ 
     
    162135}}} 
    163136 
    164 One approach is to use an explicit parameter of type {{{TNat n}}}.  For example: 
     137Now consider the definition of the function `memset`, which sets all elemnts 
     138of the array to a given fixed value. 
     139 
     140One approach is to use an explicit singleton parameter.  For example: 
    165141{{{ 
    166 memset_c :: Storable a => ArrPtr n a -> a -> TNat n -> IO () 
    167 memset_c (ArrPtr p) a n = mapM_ (\i -> pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n - 1) ] 
     142memset_c :: Storable a => ArrPtr n a -> a -> Sing n -> IO () 
     143memset_c (ArrPtr p) a size = mapM_ (\i -> pokeElemOff p i a) [ 0 .. fromIntegral (fromSing size - 1) ] 
    168144}}} 
    169145 
    170146This style is, basically, a more typed version of what is found in many standard C libraries. 
    171147Callers of this function have to pass the size of the array explicitly, and the type system checks that the 
    172 size matches that of the array.  Note that in the implementation of {{{memset_c}}} we used {{{tNatInteger}}} 
    173 to get the concrete integer associated with the singleton type. 
     148size matches that of the array.  Note that in the implementation of `memset_c` we used `fromSing` 
     149to get the concrete integer associated with the singleton type, so that we know how many elements 
     150to set with the given value/ 
    174151 
    175 While the explicit {{{TNat}}} parameter is convenient when we define the function, it is a bit 
    176 tedious to have to provide it all the time---it is easier to let the system infer the value, 
     152While the explicit `Sing` parameter is convenient when we define the function, it is a bit 
     153tedious to have to provide it all the time---it is easier to let the compiler infer the value, 
    177154based on the type of the array: 
    178155{{{ 
    179 memset :: (Storable a, NatI n) => ArrPtr n a -> a -> IO () 
    180 memset ptr a = withTNat (memset_c ptr a) 
     156memset :: (Storable a, SingI n) => ArrPtr n a -> a -> IO () 
     157memset ptr a = withSing (memset_c ptr a) 
    181158}}} 
    182  
    183 The function {{{withTNat}}} is useful when converting from the "explicit" to the "implicit" style 
    184 because it avoids ambiguity errors, scoped type-variables and other complications.