[Prev][Next][Index][Thread]
an update on "Formal parametric polymorphism"

To: types@dcs.gla.ac.uk

Subject: an update on "Formal parametric polymorphism"

From: ma@src.dec.com

Date: Sat, 06 Feb 93 18:21:17 0800

Approved: types@dcs.gla.ac.uk
This message is an update on "Formal Parametric Polymorphism", a
paper by Luca Cardelli, PierreLouis Curien, and myself, presented
at the recent POPL conference. I will assume some familiarity with
the paper.
In the version of the paper in the POPL proceedings, a rule is presented
that equates quantification over types and quantification over relations,
(Rel Eq Forall XW). As the paper says, this rule is a source of
semantic difficulties. I mentioned in my talk at POPL that Ryu Hasegawa
had very recently found an ingenious proof of inconsistency for our
system with the rule (Rel Eq Forall XW).
Since POPL, we have replaced the problematic rule with a weaker one,
then checked that this weaker rule suffices for our results. This
variant equates quantification over types and over relations only
in type expressions, and not in arbitrary relation expressions as
(Rel Eq Forall XW). We have sketched a proof of consistency for
the modified system, with a semantics based on the parametric PER
model of Bainbridge, Freyd, Scedrov, and Scott. We hope to write
the semantics properly in the course of this year; a very brief summary
follows.
We would be happy to send a full, updated version of our paper to
interested parties. This version includes the modified system with
many results that could not fit in the POPL abstract, as well as
an appendix with Hasegawa's clever example. (We intend to offer
this paper for general ftp in a couple of months.)

A brief summary of the semantics, for the brave:
In the standard per model, universal quantification over types is
interpreted with an intersection over pers; in contrast, in the per
model of Bainbridge et al., universal quantification over types is
interpreted with an intersection over (saturated) relations. Both
interpretations of universal quantifiers come into play in our semantics.
We interpret quantifiers in the top and bottom rows of our judgments
with an intersection over relations. In the middle row, type quantification
corresponds to intersection over pers, and relation quantification
to intersection over relations.
A slight miracle guarantees that the two different interpretations
of forall coexist happily. Essentially, we prove that if A is a
type then the meaning of A as (A's identity) relation does not depend
on the interpretation of its quantifiers. The argument is reminiscent
of some of Bainbridge et al..
For instance, let A = (forall X)B; write /\_{pers P} [B]_{P/X} for
the intersection when P ranges over pers of the meaning of B with
X mapped to P, and /\_{rels R} [B]_{R/X} for the corresponding intersection
with R ranging over relations. Obviously, /\_{rels R} [B]_{R/X}
is included in /\_{pers P} [B]_{P/X}. Conversely, let x, y be in
type A, that is, x(/\_{rels R} [B]_{R/X})x and y(/\_{rels R} [B]_{R/X})y,
and let x(/\_{rels P} [B]_{P/X})y; then x(/\_{rels R} [B]_{R/X})y
follows by saturation, as desired.