[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