[Prev][Next][Index][Thread]
The S-All-Loc variant of Fsub
[This message consists of three related notes: one from Ghelli,
a reply from Pierce, and a further note from Ghelli.
-- Phil Wadler, moderator, Types Forum.]
[Ghelli's first message]
>> E |- T1 < S1 E, X<S1 |- S2 < T2
>> --------------------------------------- (S-All-Loc)
>> E |- All(X<S1)S2 < All(X<T1)T2
>>
>> In particular, is subtyping for FSub with S-All-Loc decidable?
>Unfortunately, it is not. The problem remains essentially the same:
>the "apparent bound" of the variable X changes between the conclusion
>and the second premise. All that has changed here is that it is the
>free occurrences of X in T2 -- rather than S2 -- that get "re-bounded."
>
>Giorgio Ghelli and I checked this last summer. The proof is a
>straightforward variant of the undecidability proof for the standard
>version of Fsub (POPL '92).
>
>Cheers,
>
> Benjamin Pierce
>
I am sorry but I do not subscribe Benjamin's opinion in this case. My faulty
memory tells me that we discovered that the undecidability proof we sketched
for Fsub-S-All-Loc was not correct, and that thing are very difficult.
The point is that the S-All-Loc rule does not preserve the polarity of types,
as defined in [Ghe91] (and also in the undecidability paper of Benjamin,
I recall). Essentially, in |- A < B, A is negative and B is positive. In
T=All(x<A).B, B has the same polarity as T, while A as the opposite polarity.
A comparison G, x<A, G' |- x < B is reduced in both systems to a comparison
G, x<A, G' |- A < B. However, in Fsub the bound A was inserted into the
environment by a All rule which copied it from the negative bound of the right
hand side of the comparison. For this reason, in Fsub we can say that 'a
negative variable is substituted by a negative bound'. In Fsub-S-All-Loc,
a negative variable is substituted by a positive bound, which means that the
polarity of all the occurrences inside the bound is scrambled. In my opinion
this is the 'deep reason' which explains why our attempts of reducing the
problem of type-checking Fsub to type-checking Fsub-S-All-Loc did fail:
subtyping proofs in the two systems have a different structure.
My feeling is that Fsub-S-All-Loc is even more on the decidability borderline
than Fsub. My further feeling is that Fsub-S-All-Loc is decidable, but do not
take it too seriously. My last opinion is that, if it were decidable, it would
avoid the problem of non-conservativity of recursion ([Ghe93]) but it could
share the problem that Fsub is not a semilattice (see Benjamin's letter,
[Ghe90], [GP92]).
Rule Fsub-S-All-Loc was proposed to me by Simone Martini two years ago as a
way of avoiding divergence of Fsub type checking, and its undecidability, but
neither me or Simone never managed proving that this is true. I always read it
as just a syntactical trick. Vaughan Pratt writes:
> In (S-All-Loc) X is taken to be LOCal to the prevailing types,
> for which S1 presents itself as the obvious bound for defining this
> neighborhood.
suggesting that there may be some more serious reason to take that rule into
consideration, but I could not understand the sentence. Could somebody help me?
Giorgio
[Ghe90] G. Ghelli, Proof Theoretic Studies about a Minimal Type System
Integrating Inclusion and Parametric Polymorphism. Ph.D. thesis,
Universita di Pisa, 1990. Technical report TD--6/90, Dipartimento di
Informatica, Universita di Pisa.
[Ghe91] G. Ghelli, Divergence of F$_{\leq}$ Type-checking. Unpublished
manuscript, Really Soon Now ready to be ftp-distributed, 1991-1993...
Available from the author.
[Ghe93] G. Ghelli, Recursive types are not conservative over F$_{\leq}$.
Proc. of TLCA 1993.
[GP92] G. Ghelli and B. Pierce "Bounded Existentials and Minimal
Typing." Draft technical report, June 1992. Available from the
authors.
--
------------------------------------------------------------------------------
Prof. Giorgio Ghelli, Universita' di Pisa, Dipartimento di Informatica,
Corso Italia 40, I-56100, Pisa, ITALY
E-mail: ghelli@di.unipi.it; Phone: +39-50-510258; Fax: +39-50-510226
------------------------------------------------------------------------------
------------------------------------------------------------------------------
------------------------------------------------------------------------------
[Pierce's reply]
My apologies for my lapse of memory: Giorgio is right.
Benjamin Pierce
------------------------------------------------------------------------------
------------------------------------------------------------------------------
[A further note from Ghelli]
Dears Beppe, Benjamin, Simone, Vaughan,
I am afraid that rule S-All-Loc
>> E |- T1 < S1 E, X<S1 |- S2 < T2
>> --------------------------------------- (S-All-Loc)
>> E |- All(X<S1)S2 < All(X<T1)T2
>>
is not very interesting, since Fsub-All-Loc subtyping is not transitive.
More precisely, while 'limited transitivity':
E |- t < E(t) E |- E(t) < A => E |- t < A,
and full transitivity are equivalent in Fsub, in Fsub-All-Loc you have to
choose between:
1) Allow full transitivity: in this case Fsub-All-Loc is just the same as Fsub
2) Allow limited transitivity only: in this case Fsub-All-Loc is NOT transitive
Proof:
2) take u<Top |- All(t<Top).t < All(t<u).t
and u<Top |- All(t<u).t < All(t<u).u
All of them are immediately provable in Fsub-All-Loc, while:
u<Top |- All(t<Top).t < All(t<u).u
is not (you need hypothesis t<u, not just t<Top).
1) I want to prove that (a) E |- A' < A and (b) t<A' |- B' < B imply
(c) E |- All(t<A).B' < All(t<A').B can be proved using S-All-Loc plus full
transitivity.
(a) + (d) E, t<A |- B' < B' =>(All-Loc) (e) E |- All(t<A).B' < All(t<A').B'
E |- A'<A' + (b) =>(All-Loc) (f) E |- All(t<A').B' < All(t<A').B
(e) + (f) =>(full transitivity) E |- All(t<A).B' < All(t<A').B c.v.d.
By the way, I met exactly the same phenomenon when I studied, in [Ghe91],
a different variant of Fsub, double-context-Fsub. This is essentially
a system of judgements like:
|- E (A) < E' (B)
In this system any sice of the comparison has its context, so that the
type-checking algorithm always terminates, and the system is even more
powerful that Fsub-All-Loc. The All rule of this system is:
|- (E1) T1 < (E2) S1 |- (E1, X<S1) S2 < (E2, X<T1) T2
------------------------------------------------------ (S-All-Double)
|- (E1) All(X<S1)S2 < (E2) All(X<T1)T2
This rule shows why we need two different context. Unfortunately, this
system is not transitive, and its trasitive extension is exactly Fsub.
Quoting [Ghe91], I now begin believing that any variant of Fsub should
be designed on the basis of some kind of semantic intuition, rather then
on the basis of syntactic considerations, otherwise we run high risks of
unexpected behaviors.
Cheers,
Giorgio
[Ghe91] G. Ghelli, Divergence of F$_{\leq}$ Type-checking. Unpublished
manuscript, Really Soon Now ready to be ftp-distributed, 1991-1993...
Available from the author.
------------------------------------------------------------------------------
Prof. Giorgio Ghelli, Universita' di Pisa, Dipartimento di Informatica,
Corso Italia 40, I-56100, Pisa, ITALY
E-mail: ghelli@di.unipi.it; Phone: +39-50-510258; Fax: +39-50-510226
------------------------------------------------------------------------------