[Prev][Next][Index][Thread]
A decidable variant of Fsub
The Fsub subtyping rule for comparing quantified types [CG92]
E |- T1 < S1 E, X<T1 |- S2 < T2
-------------------------------------- (S-All-Orig)
E |- All(X<S1)S2 < All(X<T1)T2
has often been the subject of discussion in this list and elsewhere.
Although it has a natural semantic interpretation, it is responsible
for the loss of many desirable syntactic properties of the type
system: the decidability of subtyping [P92,G92a], the existence of
greatest lower bounds for compatible (i.e. lower-bounded) sets of
types [G90], the minimal typing property for the most natural
formulation of bounded existential types [GP92], etc. Thus, it is
reasonable to look for variants of this rule better properties.
The crux of the problem is that the upper bound of the bound variable
X in S2 changes from S1 in the rule's conclusion to T1 in the
right-hand premise. This "re-bounding" of variables is syntactically
rather bizzarre; in particular, it invalidates a whole class of useful
arguments based on structural induction on types, where the case for a
type variable normally requires applying the induction hypothesis to
its upper bound.
The weaker "equal-bounds subtyping rule" from Cardelli and Wegner's
original Fun calculus [CW85]
E, X<S1 |- S2 < T2
------------------------------- (S-All-Fun)
E |- All(X<S1)S2 < All(X<S1)T2
avoids this confusion and yields a system in which the subtyping
problem can easily be shown to be decidable at the cost of introducing
an ugly syntactic restriction -- that the bounds of the two types must
be *identical* -- with no convincing semantic interpretation.
Other variants of (S-All-Orig) have been proposed [e.g. K92], but we
are not presently aware of any investigation of one especially simple
and appealing alternative,
E |- T1 < S1 E, X<Top |- S2 < T2
--------------------------------------- (S-All-New)
E |- All(X<S1)S2 < All(X<T1)T2
in which the right-hand premise requires that the bodies be
(covariantly) related under *no* assumption about the bound variable.
This essentially amounts to considering the subtyping relation
relative to an unchanging context, since the type variables added to
the context always have trivial bounds; the only type variables with
interesting bounds will be those already present in the environment at
the point where a subtyping check is required. (These are introduced
as usual, by the quantifier introduction rule.)
In the remainder of this note, we give some reasons why this variant
may be worthy of closer consideration by the community interested in
subtyping calculi.
Clearly, the proposed rule is strictly weaker than (S-All-Orig), since
it cannot be used to prove Fsub-inequalities like
|- All(X<T1)X < All(X<T2)T2.
However, it may be argued that this difference in power is not
important for practical situations where bounded quantification is
used. (As a preliminary step toward justifying this claim, we have
checked that the development of object-oriented programming in [PT93]
can all be typed using (S-All-New) instead of (S-All-Orig).)
Moreover, the rule (S-All-New) is arguably more natural than some
other variants, since it embodies a notion of pointwise subtyping
already familiar from the treatment of other type constructors
[B93,PT93].
Most importantly, the system with (S-All-New) appears to enjoy many of
the syntactic properties missing from the standard Fsub. For example:
FACT: The subtyping problem for Fsub with (S-All-New) instead of
(S-All-Orig) is decidable.
FACT: This system also has least upper bounds for all pairs of types
and, for all lower-bounded pairs, greatest lower bounds. Formally,
for all types S and T and contexts E,
1) There is some U such that E |- U > S,T and such that
E |- W > U whenever E |- W > S,T.
2) If there is any V such that E |- V < S,T, then there is some L
such that E |- L < S,T and such that E |- W < L whenever
E |- W < S,T.
(The proof of the first fact is easy; the second proceeds by a
straightforward simultaneous induction on the "size" of S and T with
respect to the given context, where the size of a variable bound in
the given context is defined in terms of the size of its bound and the
size of variables bound in S and T is a constant.)
Similarly, we expect to have a minimal typing property for the natural
extension this system with bounded existential types. This has been
established in [GP92] for Fsub with (S-All-Fun) instead of
(S-All-Orig) by showing the completeness of a type synthesis algorithm
suggested by Dezani; this algorithm can probably be adapted to account
for (S-All-New) instead. We wonder, moreover, whether the
non-conservativity of Fsub with recursive types over ordinary Fsub
[G92b] can be repaired by using (S-All-New).
The key question, of course, is how to characterize the difference in
expressive power between the versions of Fsub with (S-All-Orig) and
(S-All-New): Are there any useful programs in this region? The known
examples suggest not, but we are at a loss to think how this might be
argued in a more rigorous way.
Best regards,
Giuseppe Castagna
Benjamin Pierce
[B93] K. B. Bruce, "Safe Type Checking in a Statically Typed
Object-Oriented Programming Language." POPL, 1993.
[BL90] K. B. Bruce and G. Longo, "A Modest Model of Records,
Inheritance, and Bounded Quantification." Information and
Computation, 87, 1990, pp. 196-240.
[CW85] L. Cardelli and P. Wegner, On Understanding Types, Data
Abstraction, and Polymorphism. ACM Computing Surveys, 17(4), December
1985.
[CG92] P.-L. Curien and G. Ghelli, Coherence of Subsumption in
F$_{\leq}$, Minimum Typing and Type Checking. Mathematical Structures
in Computer Science, 2(1), 1992.
[G90] G. Ghelli, Proof Theoretic Studies about a Minimal Type System
Integrating Inclusion and Parametric Polymorphism. Ph.D. thesis,
Universita di Pisa, 1990. Technical report TD--6/90, Dipartimento di
Informatica, Universita di Pisa.
[G92] G. Ghelli, Divergence of F$_{\leq}$ Type-checking. Unpublished
manuscript, 1992.
[G92b] G. Ghelli, Recursive types are not conservative over F$_{\leq}$.
Unpublished manuscript, 1992.
[GP92] G. Ghelli and B. Pierce "Bounded Existentials and Minimal
Typing." Draft technical report, June 1992. Available from the
authors.
[K92] D. Katiyar and S. Sankar, "Completely Bounded Quantification is
Decidable." Proceedings of the ACM SIGPLAN Workshop on ML and its
Applications, June, 1992.
[P92] B. Pierce, Bounded Quantification is Undecidable. Proceedings
of Principles of Programming Languages, January 1992.
[PT93] B. C. Pierce and D. N. Turner, "Simple Type-Theoretic
Foundations for Object-Oriented Programming." To appear in Journal of
Functional Programming; preliminary version in Principles of
Programming Languages, 1993.