Information Technology Reference
In-Depth Information
Γ ` BTA c :
Γ ` BTA x : Γ ( x )
b c
Γ [ x 7! b x ] ` BTA e 0 :
b 0
'
! b 0 ) .'
if (
b x
Γ ` BTA fn x => e 0 :
'
! b 0
b x
Γ` BTA e 1 :
Γ ` BTA e 2 :
'
! b 0
b 2
b 2
Γ ` BTA e 1 e 2 :
b 0
Γ ` BTA e 1 :
Γ
b 1
[
x 7! b 1 ]
` BTA e 2 :
b 2
Γ ` BTA let x = e 1 in e 2 :
b 2
Γ ` BTA e :
b
0
if
b b
Γ ` BTA e :
b 0
Γ ` BTA e :
b
Γ ` BTA e : 8 ( 1 ; ; n ) : b
1 ; ; n do not occur free in Γ
if
Γ ` BTA e : 8 ( 1 ; ; n ) : b
Γ ` BTA e :( b )
if dom ( ) f 1 ;; n g and 9' :( b ) .'
Table 2. Binding Time Analysis: Γ ` BTA e
:
&
'
(Example 3).
b
any annotation variable that does not occur free in the type environment; this
rule is usually used immediately before the rule for the let -construct. The sec-
ond rule is the instantiation rule that can be used to turn type schemes into
annotated types: we just apply a substitution in order to replace the bound an-
notation variables with other annotations; this rule is usually used immediately
after the axiom for variables.
t
References for type systems with subtyping include [9,10,23] as well as the more
advanced [16,37,38] that also deal with Hindley/Milner polymorphism (as found
in Standard ML). To allow a general treatment of subtyping, these papers gen-
erally demand constraints to be an explicit part of the inference system and this
is somewhat more complex than the approach taken here; such considerations
are mainly motivated by the desire to obtain principal types and in order to
develop syntactically sound and complete type inference algorithms as will be
discussed in Section 5. Indeed, our formulation of subtyping only allows shape
conformant subtyping , where the underlying type system does not make use of
any form of subtyping, and is thus somewhat simpler than atomic subtyping ,
where an ordering is imposed upon base types, and general subtyping , where an
ordering may be imposed between arbitrary types.
Strictness analyses and classical data flow analyses can also be expressed as
annotated type systems but to be useful they may require the type system to
be extended with conjunction or disjunction types [4,5,14,15] thereby touching
Search WWH ::




Custom Search