5 - Parameterized Semantics

Summary

We want to interpret the run-time constructs of our language in different ways depending on the task at hand and at the same time we want the meaning of the compile-time constructs to be fixed. To make this possible we shall parameterize the semantics on an interpretation that specifies the meaning of the run-time level. The interpretation will define

• the meaning of the run-time function types, and

• the meaning of the combinators.

Relative to an interpretation one can then define the semantics of all well-formed 2-level types, of all well-formed 2-level expressions in combinator form and of all well-formed 2-level programs in combinator form. In this chapter we shall provide the detailed development of this framework and illustrate it by definitions of various forms of eager and lazy semantics. In the following chapters we shall use the framework to specify various forms of code generation and abstract interpretation; this will substantiate the claim that the development of parameterized semantics gives the desired flexibility.

In Section 5.1 we concentrate on the 2-level types. This begins with covering the required domain theory, defining the semantics of 2-level types relative to an interpretation and then providing examples of eager and lazy interpretations. In Section 5.2 we perform an analogous development for 2-level expressions in combinator form. We conclude with a treatment of 2-level programs and a discussion of our approach to semantics.