19.5 Properties

< Free Open Study >

We can prove a standard type-preservation theorem for FJ.

19.5.1 Theorem [Preservation]

If Г ⊢ t : C and t → t′, then Г ⊢ t′ : C′ for some C′ <: C.

Proof: Exercise [⋆⋆⋆].

We can also show a variant of the standard progress theorem: if a program is well typed, then the only way it can get stuck is if it reaches a point where it cannot perform a downcast. We use the mechanism of evaluation contexts to identify the failing downcast in the latter case.

19.5.2 Lemma

Suppose t is a well-typed term.

If , then and .
If , then and .

Proof: Straightforward.

19.5.3 Definition

The set of evaluation contexts for FJ is defined as follows:

 E  ::=        []        E.f        E.m ()        v.m (, E, )        new C (, E, )        (C) E

evaluation contexts:

hole

field access

method invocation (receiver)

method invocation (arg)

object creation (arg)

cast

Each evaluation context is a term with a hole (written []) somewhere inside it. We write E[t] for the ordinary term obtained by replacing the hole in E with t.

Evaluation contexts capture the notion of the "next subterm to be reduced," in the sense that, if t → t′, then we can express t and t′ as t = E[r] and t′ = E[r′] for a unique E, r, and r′, with r → r′ by one of the computation rules E-PROJNEW, E-INVKNEW, or E-CASTNEW.

19.5.4 Theorem [Progress]

Suppose t is a closed, well-typed normal form. Then either (1) t is a value, or (2) for some evaluation context E, we can express t as , with D ≮: C.

Proof: Straightforward induction on typing derivations.

The progress property can be sharpened a little: if t contains only upcasts, then it cannot get stuck (and, if the original program contains only upcasts, then evaluation will never produce any casts that are not upcasts). But, in general, we want to use casting to lower the static types of objects, and so we must live with the possibility that casts can fail at run time. In full Java, of course, a cast failure does not stop the whole program: it generates an exception that can be caught by a surrounding exception handler.

19.5.5 Exercise [⋆⋆⋆ ↛]

Starting from one of the lambda-calculus typecheckers, build a typechecker and interpreter for Featherweight Java.

19.5.6 Exercise [⋆⋆⋆⋆ ↛]

The original FJ paper (Igarashi, Pierce, and Wadler, 1999) also formalizes polymorphic types in the style of GJ. Extend the typechecker and interpreter from Exercise 19.5.5 to include these features. (You will need to read Chapters 23, 25, 26 and 28 before attempting this exercise.)

< Free Open Study >