Changes between Version 14 and Version 15 of TypeNats/Basics

Jan 16, 2011 6:05:16 PM (7 years ago)



  • TypeNats/Basics

    v14 v15  
    4343The name ''NatI'' is a mnemonic for the different uses of the class:
    4444  * It is the ''introduction'' construct for 'Nat' values,
    45   * It is an ''implicit'' parameter of kind 'Nat' (this is discussed in more detail in [wiki:TypeNats/ImplicitExplicit a separate section])
     45  * It is an ''implicit'' parameter of kind 'Nat' (this is discussed in more detail bellow)
    4747== Examples ==
     77== Implicit vs. Explicit Parameters ==
     79There are two different styles of writing functions which need the integer corresponding to a type level natural.
     81One approach is to use an explicit parameter of type `Nat n`.  For example:
     83memset :: Storable a => ArrPtr n a -> a -> Nat n -> IO ()
     84memset = ...
     87This style is, basically, a more typed version of what is found in many standard C libraries.
     88Callers of this function have to pass the size of the array explicitly, and the type system checks that the size matches that of the array.
     89When defining `memset` we can just use `natToInteger` on the `Nat n` parameter to get the actual value of the array size.
     91Another approach is to let the system infer the parameter by using the class `TypeNat`.  For example:
     93memsetAuto :: (Storable a, TypeNat n) => ArrPtr n a -> a -> IO ()
     96In this style, the caller of the function does not need to provide the type of the array explicitly.
     97Instead, it is computed automatically from the type of the array.
     98When defining `memsetAuto` we can use `nat`, the method of `TypeNat`, to get access to the value corresponding to the type level natural.
     100When using the implicit style, it is important that the type of `nat` is specified precisely.  Failing to do so typically results in ambiguity errors
     101(i.e., GHC does not know which integer it should use).  Another common mistake is to forget that 'nat' is a polymorphic value and so every time it is used it may refer to a different value.
     103An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones.  For example, we can implement `memsetAuto` like this:
     105memsetAuto arr val = memset arr val nat