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


Ignore:
Timestamp:
Nov 17, 2010 5:53:14 PM (4 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