Go backward to Declaration Sequences
Go up to Top
Go forward to Eager Evaluation
Substitutions
- Substitution preserves typing of a phrase:
- If p_1 U p_2 |- U:H, then p_2
|- [V_j/I_j]U:H
where p_1 = {j:H_j}_j in I
and p_2 |- V_j:H_j,
for all j in I.
- Proof: induction on typing rules.
- Collorary: copy rule preserves typing
- Program needs to be type checked only once.
- Type assignments "predict" substitutions.
Copy rule is device for understanding programs with abstractions by
corresponding programs in the core language!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine