Information Technology Reference
In-Depth Information
The annotation
S
is used to model data that is available statically,
D
is used to
model data that is available dynamically, and
is an annotation variable that
can take its values among
S
and
D
.
' v '
0
may be dened by:
A partial ordering on annotations
' v '
S
v
D
Types contain annotations on the type constructors as well as on the base types;
a static function operating on dynamic integers will thus have the annotated
type
int
D S
!
int
D
. This type system is motivated by applications to partial
evaluation and this suggests imposing a well-formedness condition on types so
as to rule out types like
int
S
D
!
int
S
that are regarded as being meaningless.
This is performed by the auxiliary judgement
b
.'
that additionally extracts
'
the top-level annotation
from the annotated type
b
:
int
'
bool
'
.'
.'
1
.'
1
b
b
2
.'
2
' v '
1
and
' v '
2
if
'
!
b
1
2
.'
b
In short, a static function is allowed to operate on dynamic data but not vice
versa. Since we have annotation variables we can express a limited form of an-
notation polymorphism and we use
to denote the corresponding type schemes;
for simplicity we do not incorporate type variables or type polymorphism.
The typing judgements have the form
Γ `
BTA
e
b
:
where the type environment
b
Γ
maps variables to type schemes (or types) and
is the type scheme (or type)
b
for the expression
. The analysis is specied by the axioms and rules of Table 2
and is explained in the sequel. The rst ve axioms and rules are straightforward;
note that the rule for function abstraction checks that the type is well-formed
and that the rule for
let
makes use of type schemes.
The next rule is a subtyping rule that allows to weaken the information contained
in an annotated type. The subtype ordering
e
0
is given by:
b
b
int
'
0
int
'
' v '
0
if
bool
'
bool
'
0
if
' v '
0
1
b
2
1
2
b
b
b
'
0
!
b
' v '
0
^
b
1
2
.'
0
if
'
0
!
b
'
!
b
1
2
1
2
b
b
This ensures that only well-formed types are produced and that the ordering is
reversed for arguments to functions; we say that
'
!
b
1
2
is
contravariant
in
b
'
0
0
as being
1
but
covariant
in
'
2
. (Think of the annotated type
!
b
b
and
b
b
0
and use that the inference rule
expresses the monotonicity of logical implication.)
b
) '
0
^
b
analogous to the logical formula
The nal two rules are responsible for the polymorphism. The rst rule is the
generalisation rule
that is used to construct type schemes: we can quantify over
Search WWH ::
Custom Search