Changes between Version 3 and Version 4 of Commentary/Compiler/Coercions

Nov 17, 2010 6:05:46 PM (4 years ago)



  • Commentary/Compiler/Coercions

    v3 v4  
    102102              | Rec [(Id,CoreExpr)] 
    106104data Type          -- in TypeRep.lhs 
    107105  = TyVar TyVar 
    119117Note that 
    120118 * `Var` can be a type variable, coercion variable, or term variable.  You can tell which with a dynamic test (e.g. `isId :: Var -> Bool`). 
    121120 * `Lam` is used for type abstractions, coercion abstractions, and value abstractions.  The `Var` can tell you which. 
    122122 * Type applications (in a term) look like `(App f (Type t))`.  The `(Type t)` part must literally appear there,  with no intervening junk.  This is not statically enforced, but it turns out to be much more convenient than having a constructor `TyApp CoreExpr Type`. 
     124OK now the new proposal is to ''treat equality evidence just like any other sort of evidence''. 
     125   * A coercion variable is treated like term-level identifier, not a type-level identifier. (More on what that means below.) 
    125  * Treat equality evidence just like any other sort of evidence. 
    126    * A coercion variable is an `Id`, not a `TyVar`. 
    127    * A coercion is an `CoreExpr` whose type is `(s ~ t)` or 
    128    * A function can reu 
     127   * A coercion is an `CoreExpr`, of form `Coercion g`, whose type is `(s ~ t)`, of form `PredTy (EqPred s t)`. 
     129   * Unlike type applications, coercion applications are not required to have a `(Coercion g)` as the argument.  For example, suppose we have 
     131f :: forall a. (a~Int) => a -> Int 
     132id :: forall b. b->b 
     133c :: x~Int 
     135Then the term `(f x (id (x~Int) c))` would be fine. Notice that the coercion argument is an appplication of the identity function.  (Yes it's a bit contrived.)  In `CoreExpr` form it would look like: 
     137  App (App (Var f) (Type x)) 
     138      (App (App (Var id) (Type (PredTy (EqPred x Int)))) 
     139           (Var c)) 
     142   * Similarly a let-binding can bind a coercion 
     144  Let (NonRec c (...a coercion-valued term..)) (...body...) 
     147   * Coercion application is call-by value.  Ditto let-bindings.  You must have the evidence before calling the function. 
     149   * So it doesn't make sense to have recursive coercion bindings. 
     151   * If we see `Let (NonRec c (Coercion g)) e` we can substitute `(Coercion g)` for any term-level occurrences of `c` in the term `e`, and `g` for `c` in any occurrences of `c` in coercions inside `e`.  (This seems a bit messy.)