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

an update on "Formal parametric polymorphism"




This message is an update on "Formal Parametric Polymorphism", a 
paper by Luca Cardelli, Pierre-Louis 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.