[Prev][Next][Index][Thread]

Re: semantics for F_{sub,rec} ??

Dear Thomas,

If I understand your message correctly, you may be rediscovering a
known difficulty in interpreting systems with bounded quantifiers and
recursion using categorical methods. (I probably learned about it from
Gordon Plotkin, Luca Cardelli, or Peppe Longo in the late 80s; see for
example the introduction of my paper with Gordon in Lics 90.)
You are of course right in recalling the application of metric
methods, as in the work of Bruce and Mitchell. I would also mention
Amadio and Cardone, without immediately remembering which type systems
they study explicitly. On the other hand, I didn't understand the
reasons for your doubts on those models, and the suggestion that they
may have bugs:
 > if we try to solve
 >
 >                   A = T(A,B)
 >
 > this way it may depend on the parameter B whether  T(-,B)  is contractive.
The operators that arise are contractive (or nonexpansive, as the case
may be) in each of their arguments, and of course when any of them is
fixed. Could you please point to particular incorrect or implausible
claims in those papers on metric methods?

One may perhaps object against metric methods on principle, but that's
a somewhat different matter (?).

Regards,
            Martin



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: