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

Nov 17, 2010 6:05:46 PM (7 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.)