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

The use of polymorphic recursion for eect and region annotations allows the
inference system to deal precisely with the allocation of data inside recursive
functions. Furthermore, the inference system implicitly incorporates a notion of
constraint between annotation variables and their meaning (via a dot notation
on function arrows); as discussed in Section 5 this is a common feature of sys-
tems based on subtyping as otherwise principal types may not be expressible.
To obtain eects that are as small as possible, the inference system uses \eect
masking" [21,39,40] for removing internal components of the eect: eect com-
ponents that only deal with regions that are not externally visible. It is unclear
whether or not this system is decidable but nonetheless it has proved quite useful
in practice: a syntactically sound inference algorithm has been devised and it
is suciently accurate that a region-based implementation of Standard ML has
turned out to compete favourably with a heap-based implementation.

t

Mutually Recursive Types and Eects

So far the annotations and eects have not included any type information; as
we shall see in Section 5 this is essential for being able to develop type and
eect inference algorithms using a two-stage approach where rst the types are
determined and next the eects annotating the types. It is possible to be more
permissive in allowing eects to contain type information and in allowing even
the shape of types and type schemes to be influenced by the type information
contained in the eects; as will be explained in Section 5 this calls for a more
complex one-stage approach to type and eect inference algorithms.

Example 9. Polymorphic Typing in Standard ML.
The Hindley/Milner approach to polymorphism was originally conceived only for
pure functional languages. Extending it to deal with side eects in the form of
reference variables has presented quite a few obstacles. As an example consider
the following program fragment in an ML-like language:

let x = new nil in ( x:=cons(7,x) x:=cons(true,x) )

Here x is declared as a new cell whose contents is initially the empty list nil
and it might be natural to let the type of x be something like

list ) ref ;
but then both assignments will typecheck and hence the type system will be
semantically unsound as Standard ML only permits homogeneous lists where all
elements have the same type.
Several systems have been developed for overcoming these problems (see e.g. [42]).
One approach is to restrict the ability to generalise over \imperative" type vari-
ables: these are the type variables that may be used in an imperative manner. It
is therefore natural to adapt the side eect analysis to record the imperative type
variables and to prohibit the generalisation rule from generalising over impera-
tive type variables. In this way the shape of type schemes is clearly influenced

8: (