Go backward to Subtyping of Function Types
Go up to Top
Go forward to Record Introduction Principle

The Copy Rule for Blocks

Copy rule for lazy evaluated abstractions also applies when abstractions are locally defined within a block:
- begin define I₁=U₁, ..., define I_n=U_n
  in V end
  $=>$ [U₁/I₁, ..., U_n/I_n]V
Example:
- begin const A=2, const B=3
     in begin fun F(X:intexp) = X+A+B
        in begin const A=4 in F(A)+B end
     end
  end
- $=>$ ...
- $=>$ (lambdaX. X+2+3)(4)+3

Does not apply to eagerly evaluated abstractions!

Id: qualification.tex,v 1.2 1996/05/02 11:53:49 schreine Exp schreine