[Prev][Next][Index][Thread]
Subtyping for Recursive Types
Date: Fri, 10 Mar 89 21:03 EST
To: types@theory.LCS.MIT.EDU
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