Subtyping for Recursive Types

Date: Fri, 10 Mar 89 21:03 EST

To: types-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx


On Thursday, here at LCS, Val Breazu-Tannen presented a translation of
inheritance (subtyping) by means of coercion functions.

Two issues raised by Val's talk piqued my interest:

    (1) During his presentation, Val mentioned some results that the
        simply-typed \-calculus, with ``strong variants'' and recursive
        types has an inconsistent equational logic.

Can anyone tell me what this means?  What are strong variants, for
example?

--------------

    (2) What should be the subtyping rule for recursive types?

One possible rule is         C,a<Top |- s < t
                        --------------------------
                        C |- (rec a s) < (rec a t)

Val conjectured that this rule is sound, so long as `a' does not appear
`negatively' within s (or t).

This condition on the appearances of the recursively-bound type variable
is important.  The FX-87 typechecker required a means to test
type-inclusion of recursive types.  Pierre Jouvelot implemented this by
maintaining a stack of assumptions about type variable inclusions, and
comparing recursive types by:

(Testing (rec a s) <? (rec b t))
        1. Push a<b to the assumption stack.
        2. answer := Test s <? t
        3. Pop a<b from the assumption stack.

This method effectively assumes the following subtyping rule,

              C,a<b |- s < t
(RL)    --------------------------
        C |- (rec a s) < (rec b t)

The FX-87 Reference manual does not state this rule; it states type
inclusion rules for other types, and provides a conversion rule that

        (rec a s) == s[(rec a s)/a]   (I.e., unroll the recursion once.)

I suppose that a precise definition of the FX-87 type inclusion relation
would be as the maximal fixed point of the conditions described in the
manual.


The rule (RL) expresses the condition that `a' (resp. b) not appear
negatively in `s' (resp. t), because if it did, then the required
derivation that C,a<b |- s < t would fail.  This derivation would
require b<a, which C,a<b does not provide.

We can observe that this condition is important for type safety by
considering this example:

        s = (rec a {u:a -> int, v:real})

        t = (rec b {u:b -> int})

The type variable `a' appears negatively in the body, and we have

        H = (lambda (x : t)
              (x.u {u = (lambda (w : t) 4)}))

It is not safe to apply H to a value of type `s', because the u field of
that value will be applied to a value of type t not containing a field
v:real.


The translation rule for the inclusion rule (RL) could be:

          C*,f:a -> b   |-   (G f) : s -> t
        -------------------------------------
        C* |-  (Y G) : (rec a s) -> (rec b t)

[Proposed by Rishiyur Nikhil and myself.]

This translation makes sense; we should expect a coercion function on
recursive types to be defined recursively in terms of the body coercion
function.

  --Jim