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 

	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