Changes between Version 24 and Version 25 of TypeNats/Basics


Ignore:
Timestamp:
Mar 21, 2012 1:07:26 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v24 v25  
    2121tNat         :: NatI n => TNat n 
    2222tNatInteger  :: TNat n -> Integer 
     23 
     24-- Convenient derived functions 
     25tNatThat     :: NatI n => (Integer -> Bool) -> Maybe (TNat n) 
     26withTNat     :: NatI n => (TNat n -> a) -> a 
    2327}}} 
    24 The only "interesting" value of type ''TNat n'' is the number ''n''.  Technically, there is also an undefined element. 
    25 The value of a singleton type may be named using ''tNat'', which is a bit like a "smart" constructor for ''TNat n''. 
    26 Note that because ''tNat'' is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example: 
     28The only "interesting" value of type {{{TNat n}}} is the number {{{n}}}.  Technically, there is also an undefined element. 
     29The value of a singleton type may be named using {{{tNat}}}, which is a bit like a "smart" constructor for {{{TNat n}}}. 
     30Note that because {{{tNat}}} is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example: 
    2731{{{ 
    2832> :set -XDataKinds 
     
    3135}}} 
    3236 
    33 One may think of the smart constructor ''tNat'' as being a method of a special built-in class, ''NatI'': 
     37One may think of the smart constructor {{{tNat}}} as being a method of a special built-in class, {{{NatI}}}: 
    3438{{{ 
    3539class NatI n where 
     
    4852== Examples == 
    4953 
    50 Here is how we can use the basic primitives to define a `Show` instance for singleton types: 
     54Here is how we can use the basic primitives to define a {{{Show}}} instance for singleton types: 
    5155{{{ 
    5256instance Show (TNat n) where 
     
    5458}}} 
    5559 
    56 A more interesting example is to define a function which maps integers into singleton types: 
    57 {{{ 
    58 integerToMaybeNat :: NatI n => Integer -> Maybe (TNat n) 
    59 integerToMaybeNat x = tNatThat (== x) 
    60 }}} 
    61 It checks that the value argument `x`, passed at runtime, matches the statically-expected value, returning `Nothing` if not, and a typed singleton if so. 
    62  
    63 The implementation of `integerToMaybeNat` is a little subtle: by using 
    64 the helper function `check`, we ensure that the two occurrences of 
    65 `nat` (aka `y`) both have the same type, namely `Nat n`.  There are other 
    66 ways to achieve the same, for example, by using scoped type variables, 
    67 thus: 
    68 {{{ 
    69 integerToMaybeNat :: forall n. NatI n => Integer -> Maybe (Nat n) 
    70 integerToMaybeNat x  
    71   | x == natToInteger (nat :: Nat n) = Just nat  
    72   | otherwise                        = Nothing 
    73 }}} 
    74  
    75 Now, we can use `integerToNat` to provide a `Read` instance for singleton types: 
     60Here is how to define a {{{Read}}} instance: 
    7661{{{ 
    7762instance NatI n => Read (Nat n) where 
    7863  readsPrec p x       = do (x,xs) <- readsPrec p x 
    79                            case integerToMaybeNat x of 
     64                           case tNatThat (== x) of 
    8065                             Just n  -> [(n,xs)] 
    8166                             Nothing -> [] 
    8267}}} 
     68 
     69The derived function {{{tNatThat}}} is similar to {{{tNat}}} except that it succeeds only if the integer representation 
     70of the singleton type matches the given predicate.  So, in the {{{Read}}} instance we parse an integer and then we check 
     71if it is the expected integer for the singleton that we are trying to parse. 
     72 
    8373 
    8474== Implicit vs. Explicit Parameters == 
     
    9282One approach is to use an explicit parameter of type {{{TNat n}}}.  For example: 
    9383{{{ 
    94 memset :: Storable a => ArrPtr n a -> a -> TNat n -> IO () 
    95 memset (ArrPtr p) a n = mapM_ (\i -> pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n - 1) ] 
     84memset_c :: Storable a => ArrPtr n a -> a -> TNat n -> IO () 
     85memset_c (ArrPtr p) a n = mapM_ (\i -> pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n - 1) ] 
    9686}}} 
    9787 
    9888This style is, basically, a more typed version of what is found in many standard C libraries. 
    9989Callers of this function have to pass the size of the array explicitly, and the type system checks that the 
    100 size matches that of the array.  Note that in the implementation of {{{memset}}} we used {{{tNatInteger}}} 
     90size matches that of the array.  Note that in the implementation of {{{memset_c}}} we used {{{tNatInteger}}} 
    10191to get the concrete integer associated with the singleton type. 
    10292 
    10393Another approach is to let the system infer the parameter by using the class {{{NatI}}}.  For example: 
    10494{{{ 
    105 memsetAuto :: (Storable a, NatI n) => ArrPtr n a -> a -> IO () 
    106 memsetAuto ptr a = withTNat (memset arr a) 
     95memset :: (Storable a, NatI n) => ArrPtr n a -> a -> IO () 
     96memset ptr a = withTNat (memset_c arr a) 
    10797}}} 
    10898 
     
    115105(i.e., GHC does not know which integer it should use).  Another common mistake is to forget that 'tNat' is a polymorphic value and so every time it is used it may refer to a different value. 
    116106 
    117 An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones.  The 
    118 ba 
    119 {{{ 
    120 memsetAuto arr val = memset arr val nat 
    121 }}}