Type and E ect Systems - Correct System Design: Recent Insights and Advances - page 125

Each of these phases have their own challenges and open problems that we
now consider in some detail; many of these issues are rather orthogonal to the
more syntactic dierences used to distinguish between the formulations used in
Sections 2, 3 and 4.

Semantics. Semantics is a rather well understood area. In principle both deno-
tational and operational semantics can be used as the foundations for type and
eect systems but most papers in the literature take an operational approach.
This is indeed very natural when the analysis needs to express further intensional
details than are normally captured by a denotational semantics. But even when
taking an operational approach one frequently needs to devise it in such a man-
ner that it captures those operational details for which the analysis is intended.
The term instrumented semantics [17] has been coined for a class of denotational
or operational semantics that are more precise about low-level machine detail
(say concerning pipe-lining or the number and nature of registers) than usual.
It is therefore wise to be cautious about the precise meaning of claims stating
that an analysis has been proved correct with respect to \the" semantics.

The inference system. Previous sections have illustrated some of the varia-
tions possible when developing type and eect systems as well as some of the ap-
plications for which they can be used. However, it would be incorrect to surmise
that the selection of components are inherently linked to the example analysis
where they were rst illustrated.

At the same time we illustrated a number of design considerations to be taken
into account when devising a type and eect system. In our view the major
design decisions are as follows:

{ whether or not to incorporate

subeecting,

subtyping,

polymorphism, and

polymorphic recursion,
{ whether or not types are allowed to be influenced by eects (as was the case
in Example 9 and Section 4), and
{ whether or not constraints are an explicit part of the inference system (unlike
what simplicity demanded us to do here).
The choices made have a strong impact on the diculties of obtaining a syntac-
tically sound and complete inference algorithm; indeed, for some combinations
it may be beyond state-of-the-art (or even impossible) and in particular it may
be hard (or impossible) to deal with subtyping without admitting constraints to
the inference system. An important area of further research is how to identify
those features of the annotated type and eect systems that lead to algorithmic
intractability.