Changes between Version 33 and Version 34 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 2:13:08 AM (3 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.