11.3 Derived Forms: Sequencing and Wildcards

< Free Open Study >

In languages with side effects, it is often useful to evaluate two or more expressions in sequence. The sequencing notation t₁ ; t₂ has the effect of evaluating t₁, throwing away its trivial result, and going on to evaluate t₂.

There are actually two different ways to formalize sequencing. One is to follow the same pattern we have used for other syntactic forms: add t₁ ; t₂ as a new alternative in the syntax of terms, and then add two evaluation rules

and a typing rule

capturing the intended behavior of ;.

An alternative way of formalizing sequencing is simply to regard t₁ ; t₂ as an abbreviation for the term (λx:Unit.t₂) t₁, where the variable x is chosen fresh—i.e., different from all the free variables of t₂.

It is intuitively fairly clear that these two presentations of sequencing add up to the same thing as far as the programmer is concerned: the high-level typing and evaluation rules for sequencing can be derived from the abbreviation of t₁ ; t₂ as (λx:Unit.t₂) t₁. This intuitive correspondence is captured more formally by arguing that typing and evaluation both "commute" with the expansion of the abbreviation.

11.3.1 Theorem [Sequencing is a Derived Form]

Write λ^E ("E" for external language) for the simply typed lambda-calculus with the Unit type, the sequencing construct, and the rules E-SEQ, E-SEQNEXT, and T-SEQ, and λ^I ("I" for internal language) for the simply typed lambda-calculus with Unit only. Let e Î λ^E → λ^I be the elaboration function that translates from the external to the internal language by replacing every occurrence of t₁ ; t₂ with (λx:Unit.t₂) t₁, where x is chosen fresh in each case. Now, for each term t of λ^E, we have

t → _E t′ iff e(t) → _I e(t′)
Г ⊢^E t : T iff Г ⊢^I e(t) : T

where the evaluation and typing relations of λ^E and λ^I are annotated with E and I, respectively, to show which is which.

Proof: Each direction of each "iff" proceeds by straightforward induction on the structure of t.

Theorem 11.3.1 justifies our use of the term derived form, since it shows that the typing and evaluation behavior of the sequencing construct can be derived from those of the more fundamental operations of abstraction and application. The advantage of introducing features like sequencing as derived forms rather than as full-fledged language constructs is that we can extend the surface syntax (i.e., the language that the programmer actually uses to write programs) without adding any complexity to the internal language about which theorems such as type safety must be proved. This method of factoring the descriptions of language features can already be found in the Algol 60 report (Naur et al., 1963), and it is heavily used in many more recent language definitions, notably the Definition of Standard ML (Milner, Tofte, and Harper, 1990; Milner, Tofte, Harper, and MacQueen, 1997).

Derived forms are often called syntactic sugar, following Landin. Replacing a derived form with its lower-level definition is called desugaring.

Another derived form that will be useful in examples later on is the "wild-card" convention for variable binders. It often happens (for example, in terms created by desugaring sequencing) that we want to write a "dummy" lambda-abstraction in which the parameter variable is not actually used in the body of the abstraction. In such cases, it is annoying to have to explicitly choose a name for the bound variable; instead, we would like to replace it by a wildcard binder, written _. That is, we will write λ_:S.t to abbreviate λx:S.t, where x is some variable not occurring in t.

11.3.2 Exercise [⋆]

Give typing and evaluation rules for wildcard abstractions, and prove that they can be derived from the abbreviation stated above.

< Free Open Study >