(long) Comments on Wadler's parametric polymorphism

Date: Tue, 24 Jan 89 15:29:14 PDT
From: John Mitchell <jcm-/RedPRdSUk12Qaki92YDXw@xxxxxxxxxxxxxxxx>
To: meyer-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx
Subject: Re:  reports to Wadler

        From 
@polya.Stanford.EDU:meyer-x+IGbNLxKNYFC4420IwThje48wsgrGvP@xxxxxxxxxxxxxxxx Thu 
Jan 19 10:44:51 1989
        Return-Path: 
<@polya.Stanford.EDU:meyer-x+IGbNLxKNYFC4420IwThje48wsgrGvP@xxxxxxxxxxxxxxxx>
        Received: from Polya.Stanford.EDU by jeeves.stanford.edu (5.59/25-eef) 
id AA01794; Thu, 19 Jan 89 10:44:49 PDT
        Received: from STORK.LCS.MIT.EDU by polya.Stanford.EDU (5.59/25-eef) id 
AA05024; Thu, 19 Jan 89 10:45:24 PDT
        Received: by stork.LCS.MIT.EDU 
                id AA02180; Thu, 19 Jan 89 13:44:09 EST
        Date: Thu, 19 Jan 89 13:44:09 EST
        From: meyer-x+IGbNLxKNYFC4420IwThje48wsgrGvP@xxxxxxxxxxxxxxxx
        Message-Id: 
<8901191844.AA02180-V7RBKq7CZw5JFtkRo5AIfbg7sE8m1Ewp@xxxxxxxxxxxxxxxx>
        To: val-qRXMwjeaoBH4ZbA3o+Y6Yje48wsgrGvP@xxxxxxxxxxxxxxxx
        Subject: reports to Wadler
        Cc: plw%cs.glasgow.ac.uk-LEftKC8aXbilgWnZye4G+Q@xxxxxxxxxxxxxxxx, 
jcm@xxxxxxxxxxxxxxxxxx
        Status: RO
        
        Phil Wadler visited the other day and explained to me a bit more about
        hexagons.  He pointed out, as an instance of the theorem (whose? Freyd 
and
        P. Scott?) that pure polymorphic lambda terms satisfy hexagons, that 
for any
        pure closed polymorphic term M: ALL s,t. (s-->t)-->(s x s)-->(t x t) we 
have
        
        |-  (M s t) = lam h:s-->t. (h x h) o (M I_s) = lam h:s-->t. (M I_t) o 
(h x h)
        
        where |- means beta-eta-convertible in polymorphic calculus and o means
        compositioon.  This seems quite interesting, and was something I hadn't
        understood before.  Is it familiar to you?
        
        Anyway, Phil wanted copies of your recent papers, eg, LINC LAB 107 and 
109.
        Hope you have some to send.
        
        Dr. Philip Wadler
        University of Glasgow
        Department of Computing Science
        Glasgow G12 8QQ
        Scotland
        
        plw%cs.glasgow.ac.uk-LEftKC8aXbilgWnZye4G+Q@xxxxxxxxxxxxxxxx
        
        Regards, A.
        
The equation looks interesting, but I don't quite see what to make
of it. What does it mean to you? When he says "the theorem," I believe
he is referring to the series of papers by subsets of Bainbridge, Freyd, 
Scedrov and Scott on "Functorial Polymorphism." I believe there was one
at LICS last year. Wadler was here visiting too, so I had a brief but
inconclusive conversation with him. I have mixed feelings about his
POPL paper. It seems like an ugly hack, at first glance , but I can't
really put my finger on what is ugly about it. MacQueen and Berry had
similar reactions.

POPL was generally OK. There were reasonable papers, but nothing 
really earthshaking, as far as I can remember. In  a seminar here,
each student is presenting his/her favorite paper from the conference.
So far, we have gone through the Higher-Order  CCS paper and are
starting Abramsky's tutorial, which was superb. I assume someone there
can give you copies of the slides. 

Meseguer's paper is interesting. The main idea is to use a
predicative type theory to give semantics to poly lambda.
One view is this. If we begin with a second-order lambda theory,
we can interpret this in a version of "Martin-Lof type theory"
(actually predicative lambda calculus with two universes)
to which we have added the universe equation U0  = U1.
By Seely's paper (Locally cc categories and M-L type theory),
there is a categorical equiv between the prodicative type
theory and locally cartesian closed categories. The equivalence
holds for the special case of theories with U0 = U1 (formalized
using maps between U0 and U1; I think a retraction suffices).
This gives us a categorical notion of model: locally cartesian
closed categories with certain extra maps meaning U0 = U1.
All of the other notions of model can be squished into this form,
and hge gets completeness this way via Pitt's completeness
theorem for presheaf models (from the Edinburgh workshop on
categories and CS). The only ugly part is that it takes so
much work (the excursion into Pitts' stuff) to show that
the predicative calculus with U0 = U1 is conservative over the
original second-order calculus. It would simplify things a great deal
to have a direct srgument. But this can only be proof-theoretic in
his context, since the whole point is to avoid defining 
second-order model directly. In other words, he cannot use a 
semantic argument unless he also defines (or uses someone elses
definition of) second-order model. But the whole point of his paper
is to argue that this roundabout construction be taken as the
definition of model. Other than this, I think it is an interesting
excursion.

John
____________________
------------------

Date: Wed, 25 Jan 89 10:27:34 EST
From: meyer
To: jcm-/RedPRdSUk12Qaki92YDXw@xxxxxxxxxxxxxxxx
In-reply-to: John Mitchell's message of Tue, 24 Jan 89 15:29:14 PDT 
<8901242329.AA12166-/RedPRdSUk12Qaki92YDXw@xxxxxxxxxxxxxxxx>
Subject:  reports to Wadler
cc: val-qRXMwjeaoBH4ZbA3o+Y6Yje48wsgrGvP@xxxxxxxxxxxxxxxx

   The equation looks interesting, but I don't quite see what to make
   of it. What does it mean to you?
-------------
It says the following intuitive, elegant fact:

There is a ``natural'' and obvious function, call it `square', of type 
                    ALL s,t. (s-->t)-->(s x s)-->(t x t),
namely, square(h) = (h x h).

Now consider other ``parametrically polymorphic'' functions (ppf's) of this
type.  Clearly one way to construct these is to perform some ppf on pairs of
type (s x s) such as reversing the order of the elements, then apply
square(h), then apply some ppf of type (t x t).  It's easy to see that every
ppf, M, obtained this way could also be obtained just by performing a ppf on
pairs BEFORE applying square(h); likewise it could be obtained by performing
a ppf on pairs only after square(h).  We can figure out which ppf to use
before applying square(h) simply by evaluating (M s s I_s); likewise eval (M
t t I_t) for afterward.

That is what the equation

(M s t) = lam h:s-->t. square(h) o (M s s I_s)
        = lam h:s-->t. (M t t I_t) o square(h)

says.

Now the amazing fact is that EVERY ppf M of type ALL s,t. (s-->t)-->(s x
s)-->(t x t) satisfies this equation (by def of ppf), and in particular,
every instance of this equation with a closed polymorphic lambda term M of this
type is provable, as a consequence of the `hexagon theorem'.

Of course, this is just one instance of many such equations about ppf's and
polymorphic lambda calculus, eg, Wadler used the same equation but with
list(s) in place of (s x s) and `map' in place of `square'.

Does this make the equation more intelligible?

After I hear from Val and Scedrov, I want to forward this to TYPES; ok?

Regards, A.


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

Return-Path: <val-qRXMwjeaoBH4ZbA3o+Y6Yje48wsgrGvP@xxxxxxxxxxxxxxxx>
Date: Sun, 26 Feb 89 11:56:19 EST
From: val-qRXMwjeaoBH4ZbA3o+Y6Yje48wsgrGvP@xxxxxxxxxxxxxxxx (Val Breazu-Tannen)
Posted-Date: Sun, 26 Feb 89 11:56:19 EST
To: meyer-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx
Cc: andre-qRXMwjeaoBH4ZbA3o+Y6Yje48wsgrGvP@xxxxxxxxxxxxxxxx, 
pjf@xxxxxxxxxxxxxxxxxx, scpsg@xxxxxxxxxxxxxx
Subject: dinaturality 


In response to your question ... [about]

   |-  (M s t) = lam h:s-->t. (h x h) o (M s s id_s)       (*)
...

I knew a little about dinaturality but these particular equations were
not familiar to me. I discussed them with Andre Scedrov and below are
some comments we drafted together. Before we get to that, I would like
to point out that (1) one can check the equations (*) directly since
there are only four closed normal forms of that type and (2) letting M
be a variable gives equations which of course are not provable but
which can be consistently added to the polymorphic lambda calculus:
since all closed substitution instances of these equations are
provable, the equations will be true in Coquand's model (constructed
>from closed types and conversion classes of closed terms via
polymorphic extensional collapse; see our paper "Extensional models
for polymorphism" TCS 59, 1988, pp.85-114).  Of course, this does not
address the interesting issue: how does one come up with such
equations?

Val

COMMENTS BY ANDRE SCEDROV AND VAL TANNEN:

The idea of interpreting polymorphic terms as dinatural
transformations between multivariate functors and universal
polymorphism as ends is a natural idea in category theory and was
first studied by Stewart Bainbridge and Phil Scott. Unfortunately this
interpretation cannot be done over arbitrary ccc's, because these
transformations do not compose in general, and because ends do not
always exist.  Nonetheless, Bainbridge, Freyd, Scedrov, and Scott have
shown that it can be done over PER's ("Functorial polymorphism", to
appear in TCS. A preliminary version will appear in "Logical
foundations of functional programming", G. Huet, ed.)  and Freyd,
Girard, Scedrov, and Scott have given a related semantic
interpretation involving coherent spaces ("Semantic parametricity in
polymorphic lambda calculus", in Proceedings LICS'88).

However, the fact that the equations (*) follow from beta-etc.
conversion, that is that they are PROVABLY true, is not a consequence
of any of these two results, which only show that the equations
(letting M be a variable) are true in the respective interpretations
and thus can be consistently added.  Since by the observation above
involving Coquand's model there is a perhaps easier proof of the
consistency of these particular equations, two questions arise:

1) Are there instances of dinaturality which, unlike the one in your
message, do not hold provably, and thus for whose consistency 
we would depend on the results of BFSS or FGSS?

Peter Freyd pointed out to us that the non-provable, closed equation
 lam f:(ALL t. t->t). f = lam f:(ALL t. t->t). (Lam t. lam x:t. x)  (#)
holds in the dinatural interpretation. But (#), while not provable, 
still holds true in Coquand's model. Indeed, (#) is a provable 
consequence of 
        f = Lam t. lam x:t. x     (##)
where f is a variable of type ALL t. t->t , and all closed substitution
instances of (##) are provable.

Here is a more complicated situation. BFSS show that in the dinatural 
interpretation over PER's, the following isomorphism holds for any type a
              ALL t.(a->t)->t
 =~ a 
The isomorphism is given by  
I= lam x:a. Lam t. lam f:a->t. fx  and
J= lam w:(ALL t.(a->t)->t). wa(id_a)
Obviously  |- J o I = id_a but NOT |- I o J = id_(ALL t.(a->t)->t).
But is it at least the case that for closed types a we have
|- I(JW) = W for any closed term W:(ALL t.(a->t)->t) ?
An observation of Christine Paulin-Mohring shows this is not the case:
take a = T->T where T = ALL s. s->s and
W = Lam t. lam f:A->t. 
       f(lam g:T. Lam s. lam x:s. g(t->s)(lam y:t. x)(f id_T)) .

However, the equation  I(Jw) = w, where w:(ALL t.(a->t)->t) is a
variable, is still a provable consequence of (##) above and therefore
holds true in Coquand's model. 

To summarize, while we do have examples of equations that hold in the
dinatural interpretation but are not provably true, nor are all their
closed substitution instances provably true, we are still looking for
an equation that holds in the dinatural interpretation but not in
Coquand's model. The last example suggests that we may need to look at
slightly more complicated types.

2) Is there a general result on provable instances of dinaturality?

Here is a partial answer, which covers the equations (*):
During his visit at Pennin the Fall of 1987, Jean-Yves Girard has remarked 
that an induction technique he had developed earlier can be used to show 
that the simply typed lambda terms can be interpreted as dinatural 
transformations over any ccc (no equalizers).
By completeness, it follows that all the instances of dinaturality
of simply typed terms are actually provable. Finally we can explain
the example in your message: a bit of detective work shows that it comes 
>from the dinaturality in s and t of any closed simply typed lambda term 
M : (p->q)->(pxp)->(qxq). Indeed this dinaturality becomes
  (f2 x f2) o M[a1/p,a2/q](g o f1) = M[b1/p,b2/q] (f2 o g) o (f1 x f1)  (**)
where f1:a1->b1, f2:a2->b2, and g:b1->a2.
One of the equations (*) is obtained by taking 
a1=b1=a2=s, b2=t, f1=id_s, f2=h, g=id_s and the other one by taking 
a1=s, b1=a2=b2=t, f1=h, f2=id_t, g=id_t. (By the way, one can also
show that the equations (*) entail (**).)

Yes, please feel free to forward this to TYPES if you wish.