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

inheritance, coercions and polymorphism

Return-Path: <val@linc.cis.upenn.edu>
Date: Thu, 22 Sep 88 10:58:34 EDT
Posted-Date: Thu, 22 Sep 88 10:58:34 EDT
Cc: gunter@linc.cis.upenn.edu, andre@cis.upenn.edu



>FROM   Val Breazu-Tannen, Carl Gunter and Andre Scedrov
               University of Pennsylvania

This is a short announcement about our progress on providing a model
for FUN (see Cardelli & Wegner, Computing Surveys, 17 (1985), pp.
471--522) extended with full recursive types. (Recently, Bruce &
Longo, as well as Martini, have provided models for FUN, but without
recursive types.) We have not yet written out full details for
variants and existential quantifiers, but we hope to get to these in
due course; the rest of the language (and, of course, recursive types)
seems to work out satisfactorily with our approach.

Say FUNREC is FUN (C. & W. pp. 519--520) without existentials and
variants, but with full recursive types.

Our technique is based on the idea that expressions from FUNREC can be
translated into expressions in the polymorphic lambda calculus with
records and recursive types (which we'll call "enriched F2" below).
More precisely, a derivation of an inheritance judgement or typing
judgement in FUNREC is translated into a derivation of a typing
judgement in enriched F2. In particular, bounded universal
quantification is translated as follows:

      T[ForAll a<r. s] = ForAll a. (a -> T[r]) -> T[s]

where T[t] is the translation of type expression t.  One can think of
it this way: a bounded quantification

      ForAll a<r. s

is the type of an expression with a generic variable  a  which is
"expecting" a coercion from that variable into the type  r .  Contexts
of inclusion constraints are translated by enriched F2 typing contexts
with new "coercion" variables.  Some examples:

1)      a<t |- a<t  (axiom VAR)

translates as

      x : a->T[t] |- x : a->T[t]

2) The derivation of   a<t |- t->a < a->t
>from two occurrences of the axiom VAR, by the rule ARROW,
translates as the derivation of the polymorphic typing judgement

x: a->T[t] |- \y: T[t]->a. \z:a. x(y(xz)) : (T[t]->a) -> (a->T[t])

NOTE: One can think of the translations of inheritance judgements as
the explicit coercions that "implement" the inheritance relation.

3) If the last rule in a derivation is (GEN), i.e. bounded universal
introduction

        C. a<s , A |- e : t             
   -------------------------------  (a not free in C, A)
   C,A |- /\a<s. e : ForAll a<s. t

then the last part of the derivation obtained by the translation will
be

             T[C], x: a->T[s], T[A] |- T[e] : T[t]
       ---------------------------------------------------
       T[C] , T[A] |- \x: a->T[s]. T[e] : (a->T[s]) -> T[t]
-------------------------------------------------------------------
T[C] , T[A] |- /\a. \x: a->T[s]. T[e] : ForAll a. (a->T[s]) -> T[t]


4) If the last rule in a derivation is (SPEC), i.e. bounded universal
elimination

   C,A |- e : ForAll a<s. t      C |- s' < s
   -----------------------------------------
             C,A |- e{s'} : t{s'/a}             
   

then the last part of the derivation obtained by the translation will
be

    T[C],T[A] |- T[e] : ForAll a. (a->T[s])->T[t] 
------------------------------------------------------
T[C],T[A] |- T[e]{T[s']} : (T[s']->T[s])->T[t]{T[s']/a}
                                    
                                               T[C] |- c: T[s']->T[s]
---------------------------------------------------------------------
           T[C],T[A] |- T[e]{T[s']} c : T[t]{T[s']/a}


NOTE: The rules of FUNREC prevent  a  from occurring free in  s .


Since the derivation of a judgement (inheritance or typing) is not
uniquely determined by the judgement, our translation does not give a
unique enriched F2 term for each derivable judgement of FUNREC.
However, we show that any two derivations of the same judgement are
translated as provably equal terms, thereby establishing the coherence
of the translation.

Thus any model of enriched F2 (for example, Scott domains, qualitative
domains, dI domains, etc.) can also be viewed as a model of FUNREC.

We expect that these ideas will extend to much (if not all) of Quest.

NOTE:   FUN does not completely capture the various features of
inheritance as practiced in object-oriented languages.  Extensions to
FUN (in different directions than Quest) are currently being studied
in the community, but no crystalized proposal has yet emerged.