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

be typed, is the form of the resulting type and ' summarises the overall eect

of the program. In case contains free variables we need preliminary information

about their types and this is provided by the type environment

e

; as a result
of the type inference this preliminary information may need to be modied as
reported in the substitution

Γ

is a set of constraints that record the
meaning of the annotation variables. For eciency the algorithmic techniques
often involve the generation of constraint systems in a program independent
representation.
In the case of polymorphic recursion decidability becomes an issue. Indeed, poly-
morphic recursion over type variables makes the polymorphic type system unde-
cidable. It is therefore wise to restrict the polymorphic recursion to annotation
variables only as in [44]. There the rst stage is still ordinary type inference; the
second stage [43] concerns an algorithm

S . Finally, C

S that generates eect and region vari-

ables and an algorithm that deals with the complications due to polymorphic

recursion (for eects and regions only). The inference algorithm is proved syn-
tactically sound but is known not to be syntactically complete; indeed, obtaining
an algorithm that is syntactically sound as well as complete, seems beyond state-
of-the-art.
Once types and eects are allowed to be mutually recursive, the two-stage ap-
proach no longer works for obtaining an inference algorithm because the eects
are used to control the shape of the underlying types (in the form of which
type variables are included in a polymorphic type). This suggests a one-stage
approach where special care needs to be taken when deciding the variables over
which to generalise when constructing a polymorphic type. The main idea is that
the algorithm needs to consult the constraints in order to determine a larger set
of forbidden variables than those directly occurring in the type environment or
the eect; this can be formulated as a downwards closure with respect to the
constraint set [31,48] or by taking a principal solution of the constraints into
account [39,40].

R

Adding subtyping to this development dramatically increases the complexity of
the development. The integration of shape conformant subtyping, polymorphism
and subeecting is done in [3,31,35] that develop an inference algorithm that is
proved syntactically sound; these papers aimed at integrating the techniques for
polymorphism and subeecting (but no subtyping) from eect systems [39,40,48]
with the techniques for polymorphism and subtyping (but no eects) from type
systems [16,37,38]. A more ambitious development where the inference system
is massaged so as to facilitate developing an inference algorithm that is also
syntactically complete is described in [1]; the inference system used there has
explicit constraints in the inference system (as is usually the case in type systems
based on subtyping).

Syntactic soundness and completeness. The syntactic soundness and com-
pleteness results to be established present a useful guide to developing the infer-