Changes between Version 1 and Version 2 of TypeNats/MatchingOnNats
 Timestamp:
 Sep 23, 2012 3:55:09 AM (19 months ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/MatchingOnNats
v1 v2 41 41 }}} 42 42 43 This kind smakes it easy to define class instances or typefunctions using natural numbers.43 This kind makes it easy to define class instances or typefunctions using natural numbers. 44 44 For examples, here is a function that selects a type from a list of types: 45 45 {{{ … … 49 49 }}} 50 50 51 Such a function might be useful if we were defining some sort safe interface 52 to a foreign struct: 53 {{{ 54 getField :: Selector n > Ptr (Struct fields) > Ptr (Get n fields) 55 }}} 56 (This is just an exampleto make this work for real we'd probably 57 have to use a type class, so that we can determine the sizes of struct fields.) 51 58 59 Unfortunately, if `getField` was defined with this type signature, we 60 wouldn't be able to use it with the typelevel natural number literals 61 because `Selector` expects a type of kind `Nat1` and not a `Nat`. 52 62 53 54 55 63 To work around this, we can provide a typefunction that relates the 64 two representations of natural numbers: 56 65 {{{ 57 66 type family FromNat1 (n :: Nat1) :: Nat … … 60 69 }}} 61 70 71 By using `FromNat1`, we can give `getField` a type that will allow 72 for the use of ordinary typelevel literals: 73 {{{ 74 getField :: Selector (FromNat1 n) > Ptr (Struct fields) > Ptr (Get n fields) 75 }}} 62 76 77 There is one final detail that needs to be explained: if we were to try the 78 definitions presented so far without any further modifications, we would get 79 ambiguity errors when trying to use `getField`. The reason for this is that 80 the type variable `n` appears only in arguments to typefunctions so GHC 81 has no way to determine its value from the result of the type function. 82 83 The good news is that the function `FromNat1` is injective so, in fact, 84 it is possible to determine the input from the output. We modified GHC's 85 type checker to make it aware of this fact. These changes are captured 86 by the following two rules: 63 87 {{{ 64 88 forall a b. (FromNat1 a ~ FromNat1 b) => (a ~ b) 65 forall a b. exists c. (1 <= FromNat1 a) => (a ~ Succ b)89 forall a. exists b. (1 <= FromNat1 a) => (a ~ Succ b) 66 90 }}} 91 92 93