Polymorphic lambda-calculus

Polymorphic lambda-calculus

[Elaine Gouvea Pimentel]

Hi!

I'd like to know if there is any categorical model for
polymorphic lambda-calculus.


Thanks,

Elaine.

Re: Polymorphic lambda-calculus

[R.A.G. Seely]

My 1987 JSL paper is a start - "Categorical Semantics for
Higher-Order Polymorphic Lambda Calculus", JSL 52 (1987) 4, 
pp 969 - 989.  In particular, look at section 3, where the
model of closure operators is described in categorical terms.

= rags =

On Thu, 18 Mar 1999, Elaine Gouvea Pimentel wrote:

> I'd like to know if there is any categorical model for
> polymorphic lambda-calculus.


=================================
<rags@math.mcgill.ca>
<http://www.math.mcgill.ca/~rags>

polymorphic lambda-calculus.

[Paul Taylor]

Elaine Gouvea Pimentel would "like to know if there is any categorical model
for polymorphic lambda-calculus".

Oh dear. I can see that this one is going to haunt me for the rest of
my life, besides provoking some "discussion" here.  I wrote my thesis
on this subject.

Perhaps I will be personally rid of this albatross when my book comes out.
Chapter VIII contains the definitive account of [my] notion of a "category
with a class of display maps" (or, more briefly, display category).  This
is how I deal with dependent types at the algebraic level (superseding
essentially algebraic theories encoded as categories with all finite limits).
In my view, discussion of quantifiers (whether first order or over types)
should be based on this, as is in fact done in Chapter IX.

There are several different things that you might mean by "polymorphic
lambda-calculus", and no doubt Bart Jacobs or Thomas Streicher will
contribute an overview of the "Barendregt cube".  [Robert Seely also
did some work in this area before most of the other people.]

One thing is that types are expressions involving type variables, with
a universal quantifier over types. Girard calls this System F, and there
is an introductory account in "Proofs and Types" - Girard's book that
Yves Lafont and I translated.

Numerous domain theoretic models of System F were found in the later 1980s,
using both "Scott"-like "continuous" domains and "stable" domains which
were introduced by Berry and popularised by Girard.

ALL of the domain theoretic models, so far as I am aware, had THE SAME
interpretation of type-dependency and the quantifier.  I have seen this
interpretation attributed to Girard, but I regarded it as "well known"
when I was writing my thesis - before Girard's models - and my guess is
that it is due to Gordon Plotkin, probably in the "Pisa notes".

This interpretation of the dependency of the type T[x] on x:X, where X
is in the first instance a domain (and in particular a poset, therefore
a category) is most simply described as a functor T:X->Dom^adj
where Dom^adj denotes the category whose objects are domains and whose
morphisms are [left] adjoint pairs of continuous functions. Many authors
took embeddings (monos with continuous right adjoints) instead, but
the restriction is irrelevant.  The functor T must also be continuous
in the sense of taking directed joins to filtered colimits of left adjoints,
which are also the cofiltered limits of the right adjoints.

For the stable case, replace "continuous" by "stable", where a stable
functor preserves pullbacks, and the unit and counit of the adjunctions
have pullbacks for their naturality squares.   This situation is so
over-constrained that some pretty amazing things (that I discovered but
never wrote up) happen.

The universal quantifier is most concisely described as the category of
sections of the fibration (Grothendieck construction) corresponding to
the functor T above.

That was for first order dependency over a particular domain X.  For
dependency over all domains (System F), replace X by Dom^adj.  It doesn't
matter whether this category happens to be one of your (poset) domains,
so long as you only want System F. (At the time of my thesis I considered
this to be cheating, and laboriously constructed a poset-domain that
"covered" Dom^adj in a suitable sense.  Thierry Coquand and his co-authors
did not consider this to be cheating, and thereby beat me to finding
a model of System F.)  If Dom^adj really is a domain then you get a
model of Coquand's Calculus of Constructions.

Such a model of CoC was described by Martin Hyland and Andy Pitts in the
Boulder proceedings in 1987.    If I still had the inclination to work
on such matters, I could give a simpler version of their model (replacing
the lex categories by display categories).  This was on the "to do" list
throughout the writing of my book - I wanted to include this "simplified"
version as a sequence of exercises - but it was always just over the 
horizon of what could be done with the tools available, given that the
necessary domain-theoretic techniques had been debarred from the book
from its conception.

Another model, whose types are named by countable groupoids (or by the
corresponding presheaf toposes of G-sets) is to be found in my paper
"Quantitative Domains, Groupoids and Linear Logic" in the proceedings
of the 1989 Manchester CTCS.  When I was writing this paper I tried to
get Francois Lamarche to read it, but he said he didn't know anything
about / hated permutation representations.  Nobody else, so far as I can
gather, has ever read it, and now I can no longer follow the most 
difficult calculations.  However, it is a very pretty model nevertheless.

All of this was a bit of a Holy Grail.  When you come to calculate the
interpretations of types like   Pi X. X -> (X->X) -> X,  they turn out
to be the most horrendous mess.   The "coherence space" model in "Proofs
and Types" may well be the only one in which you can give an explicit
desciption of Pi X. X -> X -> X, and even that has four elements, where
there are only two closed lambda terms.

There are of course other ways of finding models of the polymorphic
lambda calculus, such as using the "small complete category" in Hyland's
effective topos, but I'll leave someone else to write about that.

In conclusion, this particular dragon's den has already been explored,
and the corpses are still there to prove it.

Paul

You can find this stuff on my page at Hypatia,
	http://hypatia.dcs.qmw.ac.uk/author/TaylorP
and on the corresponding pages of the other people mentioned above.