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


Ignore:
Timestamp:
Nov 17, 2010 5:53:14 PM (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/Coercions

    v2 v3  
    8282== Main proposal ==
    8383
     84Recall our basic types
     85{{{
     86type Id    = Var   -- in Var.lhs
     87type TyVar = Var
     88
     89data CoreExpr      -- in CoreSyn.lhs
     90  = Var Var
     91  | Lit Lit
     92  | Type Type
     93  | Coercion Coercion
     94  | App CoreExpr CoreExpr
     95  | Lam Var CoreExpr
     96  | Cast CoreExpr Coercion
     97  | Let CoreBind CoreExpr
     98  | Case... | Note ...
     99
     100
     101data CoreBind = NonRec Var CoreExpr
     102              | Rec [(Id,CoreExpr)]
     103
     104
     105
     106data Type          -- in TypeRep.lhs
     107  = TyVar TyVar
     108  | AppTy Type Type
     109  | FunTy Type Type
     110  | ForAllTy Var Type
     111  | PredTy PredType
     112  | TyConApp TyCon [Type]
     113
     114data PredType
     115  = EqPred Type Type
     116  | ClassP Class [Type]
     117  | IParam Name Type
     118}}}
     119Note that
     120 * `Var` can be a type variable, coercion variable, or term variable.  You can tell which with a dynamic test (e.g. `isId :: Var -> Bool`).
     121 * `Lam` is used for type abstractions, coercion abstractions, and value abstractions.  The `Var` can tell you which.
     122 * 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`.
     123
     124
    84125 * Treat equality evidence just like any other sort of evidence.
    85126   * A coercion variable is an `Id`, not a `TyVar`.
    86    *
     127   * A coercion is an `CoreExpr` whose type is `(s ~ t)` or
     128   * A function can reu