Information Technology Reference
In-Depth Information
scheme (or type). The clauses are as in Table 3 with the addition of the following
rules:
Γ `
SE
e
1
:
Γ
b
1
&
'
1
[
x 7!
b
1
]
`
SE
e
2
:
b
2
&
'
2
Γ `
SE
let
x
=
e
1
in
e
2
:
2
&
'
1
[ '
2
b
Γ `
SE
e
:
&
'
b
1
; ;
n
do not occur free in
Γ
'
if
and
Γ `
SE
e
:
8
(
1
; ;
n
)
:
b
&
'
Γ `
SE
e
:
8
(
1
; ;
n
)
:
b
&
'
if
dom
(
)
f
1
;;
n
g
Γ `
SE
e
:(
b
)&
'
The second and third rules are responsible for the polymorphism and are exten-
sions of the last two rules of Table 2. The second rule is the
generalisation rule
:
we can quantify over any type, annotation or region variable that does not occur
free in the assumptions
or in the eect
. The third rule is the
instantiation rule
:
we just apply a substitution in order to replace the bound type, annotation and
region variables with other types, annotations and regions.
t
Both subtyping and polymorphism improve subeecting by giving ner control
over when to \enlarge" the types; we already explained the advantage: that more
informative types and eects can be used in subprograms. Since the mechanisms
used are incomparable it clearly makes sense to combine both. However, as dis-
cussed in Section 5, it may be quite challenging to develop a type and eect
inference algorithm that is both syntactically sound and complete.
Example 8. Region Inference.
The
let
-construct can be used to give polymorphic types to functions. But in the
Hindley/Milner approach a recursive function can only be used polymorphically
outside of its own body { inside its own body it must be used monomorphically.
The generalisation to allow recursive functions to be used polymorphically also
inside their own bodies is known as
polymorphic recursion
but gives rise to an
undecidable type system; this means that no terminating type inference algo-
rithm can be both syntactically sound and complete. This insight is a useful
illustration of the close borderline between decidability and undecidability that
holds for the inference based approach to the static analysis of programs.
Even though we abstain from using polymorphic recursion for ordinary types
there is still the possibility of using polymorphic recursion for the eects an-
notating the ordinary and possibly polymorphic types given to recursive func-
tions. In this way, distinct uses of a recursive function inside its body can still
be analysed in dierent ways. This approach is taken in an analysis known as
region inference [44] that is used when implementing functional languages in a
stack-based regime rather than a heap-based regime. More precisely, the memory
model is a stack of regions of data items, and the analysis facilitates determining
at compile-time in which region to allocate data and when to deallocate a region
(rather than using a garbage collector at run-time).
Search WWH ::
Custom Search