A constraint consists of an n-ary constraint constructor applied to n constraint
variables
.
The semantics of an n-ary constraint c is an n-ary
relation
on type terms. A solution
of a constraint set C is
a substitution which maps constraint variables to types such that for
each constraint
the types
are related by
.
Figure 13
summarizes syntax and semantics of the constraints for our type
system. We omit the tedious specification of
and simply state the
corresponding condition on solutions.
The equality constraint denotes equality of its arguments. The function constraint specifies a function which may be static, memoized, or dynamic. S-function specifies a function which may be completely static or dynamic. M-function specifies a function which may be memoized or dynamic. Structure specifies a static or dynamic data structure. The base value constraint specifies a static or dynamic base value. An S-dependency states that staticness of implies staticness of . Likewise, an M-dependency states that memoizability of implies memoizability of . The constraint states that is not completely static and states that must be memoizable. Both do not occur in initial constraint sets, but are introduced later on. A dependency states that if is dynamic then so is . An L-dependency is needed to specify the type constraints for apply: If is dynamic then is a list of dynamic elements; if both are lists then their elements are equal. A lift constraint states that either is a static base value and is dynamic or that both and are equal.
By collapsing the different typing rules for a construct and its different overlined and underlined versions into one we can generate the constraint set which must be solved by a type derivation for some expression E. A minimal solution of the resulting constraint set can be found using methods similar to those in Henglein's work [19]. However, the resulting type inference algorithm is at least quadratic in the size of the input program, due to the dependency on the environment. Details may be found in a companion technical report [30].