[Prev][Next][Index][Thread]
doing without F-bounded quantification
Date: Mon, 3 Feb 92 11:27:24 PST
Follow a remark and a question on F-bounded polymorphism.
F-bounded quantification has been used to model certain features of
object-oriented programming in the lambda calculus. F-bounded
quantification is quantification over types where the bound variable
may occur in its bound, e.g. (forall X < Nat -> X. Bool -> X).
Some time ago, Luca Cardelli and John Mitchell observed that F-bounded
quantification could be replaced with higher-order quantification.
They replaced
forall X < F(X). M(X)
with
forall G < F. M(fix G)
Here G and F are type operators, and the order on them is pointwise;
fix G is the fixpoint of G, which we assume unique for now. (This
technique is described in the recent paper by Kim Bruce and John
in POPL92.)
This replacement worked, in that it did the job for modelling
object-oriented features. I had then noticed that in many models
the two type expressions are actually equal as sets of values, when
forall is interpreted as an intersection. Here is a quick proof.
* (forall G < F. M(fix G)) is included in (forall X < F(X). M(X)):
If A < F(A) then there is a G s.t. G < F and (fix G) = A. An
appropriate choice is: G(X) is defined as F(X) /\ A, where /\
denotes type intersection. Clearly, G < F; in addition,
G(A) = F(A) /\ A (by def. of G) = A (since A < F(A)) so A is
a fixpoint of G.
* (forall G < F. M(fix G)) includes (forall X < F(X). M(X)):
It suffices to notice that if G < F then (fix G) = G(fix G) <
F(fix G). Therefore, given a G < F, there exists an A < F(A)
such that A = (fix G), as needed.
Let's now reconsider the semantics of forall G < F. M(fix G). One
should wonder over what class of type operators G ranges, and how
to know that there is a well-defined fix G. The proof of the second
inclusion above works for any reasonable definition, but the first
one is problematic. In ideal models or in per models based on metric
methods (e.g., Amadio's, Cardone's), one would naturally interpret
the forall G as a quantifier over all contractive operators; if
F itself is contractive then the G defined is contractive and all
is well---it has a unique fixpoint. In more categorical models,
it may not even make sense to talk about intersection (because of
functoriality concerns). But in any model where the G defined exists
A is the largest (!) fixpoint of G.
After these arguments, we may feel that it is not so surprising that
Luca's and John's replacement worked. Yet these arguments are a
bit ad hoc, as they are quite far away from the syntax of the lambda
calculus. It would be nice to have a more syntactic proof of
equivalence, that would work for larger classes of models.
Martin Abadi