[Prev][Next][Index][Thread]
Re: semantics for F_{sub,rec} ??
Hi Thomas,
Let me respond to your message as my recent book on the foundations of
object-oriented languages seems to have stimulated your questions, and
you also refer to earlier work that I did with John Mitchell. However,
I should warn you that I haven't looked at the denotational semantics
issues in over 10 years, and so am a bit rusty on the details.
John Mitchell and I began looking at the issues of solving domain
equations in F_{sub} because we needed the solutions to make sense of
equations that were arising in modelling the semantics of
object-oriented languages. We liked the earlier work of Cardone,
Amadio, and Abadi and Plotkin, but found that they couldn't do
everything that we needed (in particular bounded and F-bounded
polymorphism). We were also interested in explaining the metric space
ideas in analogy to the more familiar L_{infinity} construction.
The analogy to the L_{infinity} construction that we presented in our
POPL '92 paper appeared to us to give a good explanation of what was
happening with the metric approach and also allowed us to solve the
extra domain equations that we needed. Unfortunately, they didn't solve
all of them. Here is a quote from that paper that is relevant:
"{W}e show directly in Section 5 that every rank-increasing function
has a unique fixed point, and the collection of rank-increasing
functions has the same abstract structure as an acceptable collection of
nice pers. It is shown in Section 7 that the type constructors for
function space, records, and F-bounded quantification are
rank-increasing. This suggests that we could take the collection of
type functions to be all rank-increasing functions on an acceptable
collection of per's, and repeat the construction through higher kinds.
The only drawback of this is that certain trivial functions, like the
identity map from types to types, only satisfy a weaker rank-preserving
property, and are not rank-increasing. Since the larger class of
``rank-preserving'' functions are also rank-ordered, the more natural
model contains all rank-preserving functions.
"A mild embarrassment we have about this construction is that only the
rank-increasing subset of the rank-preserving functions have unique
fixed points. A mitigating factor is that since all the type
connectives are rank increasing, and the composition of rank-increasing
functions with rank-preserving ones produces a rank increasing function,
the only limitation that this yields is that in applying a recursion
operator to a type function or functional of some order, the body of the
function must involve at least one type connective or operator (such as
-> or F-bounded quantification). While we would like to lift this
restriction on recursion, the only alternative we know of at this point
is to work with the smaller class of type functions described in
\cite{AbadiPlotkin}. However, this would involve dropping even simple
bounded quantification, which is a nontrivial trade-off. In the special
case that we restrict the language to $F_3$, as opposed to $F_\omega$,
we are able to construct a model with unrestricted use of recursion by
adding identity and projection maps to the rank-increasing functions.
Since $F_3$ is adequate for most practical examples, this is an
appealing variant of our construction."
So we didn't quite get everything, but we did get fixed points for all
non-trivial type functions (even those with extra parameters). This
gave me the confidence that what we were doing with the semantics of O-O
languages made sense.
Now, since that time I have focussed on the use of (natural) operational
semantics, in part because of its utility in working with imperative
languages, and in part because of its similarity to denotational
semantics. With that kind of semantics, subject reduction and type
preservation/safety results (as proved for example in Pierce's new book)
provide the bedrock. Thus I don't believe there is any reason to worry
about the correctness of the foundations of this work. [In particular,
for those not familiar with my new book, there I presented a
translational semantics from OO languages to F_{sub,omega}. A type
preservation proposition plus results on subject reduction and
type-safety for F_{sub,omega} yield the desired type-safety results for
the O-O language.]
On the other hand, I would be very pleased to see a denotational model
of the full F_{sub,omega} with solutions to all (higher-order) domain
equations.
Kim Bruce
Thomas Streicher wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>
> In work on semantics of object oriented languages (as e.g. Kim Bruce's
> recent book at MIT press) it turns out as useful to translate some basic
> OOP languages into F_{sub,rec}, i.e. lambda calculus with bounded
> quantification over types and recursive types.
> However, in most of these papers I couldn't find a semantics for F_{sub,rec}.
> What comes most naturally to one's mind (at least to mine and that of a couple
> of colleagues as well, I presume) are realizability models. If one interprets
> types as complete expers, say, (as forcefully suggested in a paper by Mitchell
> and Viswanathan (ICALP'96)) it is more or less obvious that this way one gets
>
> (1) an interpretation of bounded quantification and
>
> (2) bifree solutions of type equations of the form A = F(A,A)
> where F is a mixed variant functor F : Ty^op x Ty -> Ty .
>
> That's essentially the succus of the above mentioned article of Mitchell and
> Viswanathan and the immediate reaction of people having worked in
> realizability semantics and SDT (like me) will be : well, yes, of course!
>
> Thus, everything seems to be ok. At least I thought so for quite some time.
> However, when looking more closely again into F_{sub,rec} I came to the
> conclusion that (1) and (2) above are not sufficient for interpreting the sort
> of recursive types one finds in F_{sub,rec} simply because one want's to solve
> type equations of the form A = T(A) where T(X) can NOT be written as F(X,X)
> for some mixed variant functor F : Ty^op x Ty -> Ty. A typical such example is
>
> A = T(A) := All X <: A. X -> Nat x X
>
> because the natural candidate for a mixed variant functor F with T(A) = F(A,A)
> would be
>
> F(B,A) = All X <: B. X -> Nat x X
>
> and that is NOT functorial in B .
> Well, it is when restricting to coercion maps but not for arbitrary f.
>
> It is true that T may me considered as T : TyL^op -> TyL where TyL is the
> lattice of complete expers under coercion (set inclusion). If T were covariant
> (e.g. when T(A) = Exist X <: A. X -> Nat x X) then Knaster-Tarski provides a
> solution to A = T(A) (but not a bifree one! and therefore not supporting the
> usual desired reasoning principles for recusrive types). But, alas,
>
> T(A) := All X <: A. X -> Nat x X
>
> is contravariant and Knaster-Tarski doesn't help!
>
> I know that people were playing some quite sophisticated tricks endowing the
> collection of types with some metric and applying Banach's fixpoint theorem
> to contractive mappings from types to types. Contractivity is usually ensured
> by guardedness. This is ok when one wants to solve a single type equation
> without parameters. But if we try to solve
>
> A = T(A,B)
>
> this way it may depend on the parameter B whether T(-,B) is contractive.
> This little observation is my main reason for having some doubts in the
> applicability of the results of Bruce and Mitchell in their 1992 article
>
> PER models of subtyping, recursive types and higher order polymorphism
>
> Well, summarizing my somewhat lengthy discussion above my QUESTION is whether
> in the meantime people have found (good) models of F_{sub,rec} not suffering
> from the "little" bugs I mentioned. I think that this question is of some
> relevance because F_{sub,rec} is used intrinsically in contemporary work on
> semantics of OOP and it would be a shame if it turns out as built on sand
> (in the sense that it lacks a good semantics for the target language used in
> these translational interpretations).
>
> I apologize if some of my formulations may appear a bit provocative but I
> wanted to make my point as clear as possible. Needless to say that I would be
> grateful for any clarification of the points I raised.
>
> Thomas Streicher
Follow-Ups: