Information Technology Reference
In-Depth Information
contravariant
in
1
but
covariant
in
'
and
2
.Also
%
is both covariant
b
b
b
ref
in
(when the reference variable is used for accessing its value as in
!
x
)and
b
contravariant in
(when the reference variable is used for assignments as in
b
x
) whereas it is only covariant in
%
. This form of subtyping amounts
:=
to
shape conformant subtyping
because
1
b
2
implies that the two annotated
b
t
types have the same underlying types.
Subeecting alone suces for obtaining a conservative extension of the under-
lying type system { provided that we regard the use of
in the rule for
new
as being an integral part of subeecting; the general idea is that subeecting
allows to \enlarge" the eects at an
early
point so that they do not conflict
with the demands of the type and eect system. This reduces the usefulness of
the eects but by incorporating subtyping we can \enlarge" the types at a
later
point; hence more informative types and eects can be used in subprograms.
Coming back to our treatment of control flow analysis in Example 2 we note
that basically it is a subeecting analysis.
%
Polymorphism and Polymorphic Recursion
Subtyping is one of the classical techniques for making a type more useful by
allowing to adapt it to dierent needs. Another classical technique is Hind-
ley/Milner polymorphism as found in Standard ML and other functional lan-
guages. Both techniques are useful for increasing the precision of the information
obtainable from type and eect systems.
Example 7. Polymorphism for Side Eect Analysis.
We now once more extend the language of Examples 5 and 6 with a polymorphic
let
-construct:
e
j
x
e
1
in
e
2
::=
let
=
We also allow types to contain type variables
, eects to contain annotation
variables
and regions to contain region variables
:
::=
j
'
::=
j
%
::=
j
b
We can then dene type schemes: a type scheme is a type where a (possible
empty) list
1
; ;
n
of type, eect and region variables has been quantied
over:
::=
8
(
1
; ;
n
)
:
b
b
If the list is empty we simply write
for
8
()
:
b
.
b
Γ `
SE
e
The typing judgements will be of the form
:
&
'
where the type
b
environment
Γ
now maps variables to type schemes (or types) and
is a type
b
Search WWH ::
Custom Search