Changes between Version 1 and Version 2 of TypeNats/MatchingOnNats


Ignore:
Timestamp:
Sep 23, 2012 3:55:09 AM (19 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/MatchingOnNats

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