Changes between Version 21 and Version 22 of TypeNats/Basics


Ignore:
Timestamp:
Mar 21, 2012 12:53:39 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v21 v22  
    3636  tNat :: TNat n 
    3737 
    38 instance NatI 0 where tNat = "singleton 0 value" 
    39 instance NatI 1 where tNat = "singleton 1 value" 
    40 instance NatI 2 where tNat = "singleton 2 value" 
     38instance NatI 0 where tNat = ...singleton 0 value... 
     39instance NatI 1 where tNat = ...singleton 1 value... 
     40instance NatI 2 where tNat = ...singleton 2 value... 
    4141etc. 
    4242}}} 
     
    8585 
    8686There are two different styles of writing functions which need the integer corresponding to a type level natural. 
     87To illustrate the two style consider a type for working with C-style arrays: 
     88{{{ 
     89newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) 
     90}}} 
    8791 
    88 One approach is to use an explicit parameter of type `Nat n`.  For example: 
     92One approach is to use an explicit parameter of type {{{TNat n}}}.  For example: 
    8993{{{ 
    90 memset :: Storable a => ArrPtr n a -> a -> Nat n -> IO () 
     94memset :: Storable a => ArrPtr n a -> a -> TNat n -> IO () 
    9195memset = ... 
    9296}}} 
    9397 
    9498This style is, basically, a more typed version of what is found in many standard C libraries. 
    95 Callers 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. 
    96 When defining `memset` we can just use `natToInteger` on the `Nat n` parameter to get the actual value of the array size. 
     99Callers of this function have to pass the size of the array explicitly, and the type system checks that the 
     100size matches that of the array. When defining {{{memset}}} we can just use {{{tNatInteger}}}` on the {{{TNat n}}} 
     101parameter to get the actual value of the array size. 
    97102 
    98103Another approach is to let the system infer the parameter by using the class `NatI`.  For example: 
    99104{{{ 
    100105memsetAuto :: (Storable a, NatI n) => ArrPtr n a -> a -> IO () 
     106memsetAuto = ... 
    101107}}} 
    102108 
    103109In this style, the caller of the function does not need to provide the size of the array explicitly. 
    104110Instead, it is computed automatically from the type of the array. 
    105 When defining `memsetAuto` we can use `nat`, the method of `NatI`, to get access to the value corresponding to the type level natural. 
     111When defining {{{memsetAuto}}} we can use {{{{tNat}}}, the method of {{{NatI}}}, to get access to the value 
     112corresponding to the type level natural. 
    106113 
    107 When using the implicit style, it is important that the type of `nat` is specified precisely.  Failing to do so typically results in ambiguity errors 
    108 (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. 
     114When using the implicit style, it is important that the type of {{{tNat}}} is specified precisely.  Failing to do so typically results in ambiguity errors 
     115(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. 
    109116 
    110 An 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: 
     117An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones.  The 
     118ba 
    111119{{{ 
    112120memsetAuto arr val = memset arr val nat 
    113121}}} 
    114