[Prev][Next][Index][Thread]
Re: Recursive types in polymorphic lambda calculus
Thanks to all for the responses to my question, and sorry for the
delay in summarising the replies. The concensus seems to be that
Reynolds (83) and Bohm-Berarducci (85) understood the concept, and
that Reynolds-Plotkin (preprint in 88) spelled out the categorical
construction, with many other pieces of related work. -- P
========================================================================
The question:
========================================================================
To: types@cis.upenn.edu, categories@mta.ca
Subject: categories: Recursive types in polymorphic lambda calculus
Date: Fri, 14 May 1999 15:24:32 -0400
From: Philip Wadler <wadler@research.bell-labs.com>
There is a fairly standard encoding of recursive types
into polymorphic lambda calculus, given by
rec X.F[X] = all X.(F[X] -> X) -> X
where F[X] is a type in which the type variable X appears only
covariantly. Recall that every covariant type corresponds to a
covariant functor, so for every h:X->Y we have F[h]:F[X]->F[Y].
If we abbreviate T = rec X.F[X], then the key functions on this
type are given by the polymorphic lambda terms:
fold : all X.(F[X] -> X) -> T -> X
fold = Lam X.lam k:F[X]->X.lam t:T.t{X}(k)
in : F[T] -> T
in = lam u:F[T].Lam X.lam k:F[X]->X.k(F[fold{X}(k)](u))
out : T -> F[T]
out = fold{F[T]}(F[in])
Questions: Who first had this insight? Where is a good place to find
this spelled out in the literature? Please send results to me, and I
will summarize them for the list. Cheers, -- P
========================================================================
The answers:
========================================================================
Date: Sat, 15 May 1999 23:40:29 -0400
From: "P. Scott" <scpsg@matrix.cc.uottawa.ca>
To: wadler@research.bell-labs.com
Subject: Re: Recursive types in polymorphic lambda calculus
Cc: scpsg@matrix.cc.uottawa.ca
Dear Phil:
I can give you a bit of the history of the functorial
type approach, as far as I know it. I will start with recent
history, then mention a few ancient tidbits.
RECENT HISTORY
Syntactically, the fact that for any multisorted finitary algebraic
signature, that the elements of initial algebras can be represented by
closed normal terms of polymorphic type is well-known. It is implicit in
Girard's Phd thesis (by Curry-Howard), and explicit in Reynolds 1983
paper "Types, abstraction, and parametric polymorphism", as well as in
Bohm-Berarducci "Automatic synthesis of typed \Lambda-programs on term
algebras, TCS 39 (1985), 135-154. More recently, of course, one can
look at Girard-Lafont-Taylor, Section 11.5, and also the interesting
discussion in John Mitchell's Foundations for Programming Languages,
MIT Press, 1996, Section 9.3.
Categorically, the first place I saw the functorial approach published
in detail--and the fact that in System F, \forall p [ T(p) ==> p ==> p ]
is a weakly initial T-algebra (for definable covariant functors T) is in
Reynolds-Plotkin "On Functors Expressible in the Polymorphic Typed Lambda
Calculus (Inf. & Computation, 1993, reprinted in "Logical Foundations
of Functional Programming", edited by G. Huet, Addison-Wesley, 1990).
The second place where this is done in detail is the paper
"Functorial Polymorphism", by Bainbridge, Freyd, Scedrov, and me
(TCS 70 (1990), Subsection 4.9 of "Reynolds' Parametricity".
A closely related work to the above is by R. Hasegawa, "Categorical data
types in parametric polymorphism, MSCS 4, 1994, pp. 71-109.
A basic categorical reference for some of this is Roy Crole's book
"Categories for Types", CUP, Chapter 5. More advanced remarks on formal
category theory are also in John Mitchell's book, Section 9.3, loc. cit.
Finally, I can recommend a few papers on related material:
Abadi, Cardelli, Curien "Formal parametric polymorphism, TCS 121
(1993), pp. 9-58,
Plotkin & Abadi, "A logic for parametric polymorphism"
TLCA'93, SLNCS 664, 1993, pp. 361-375
R. Hasegawa, A logical aspect of parametric polymorphism,
CSL'95, SLNCS 1092, 1995.
PRE-HISTORY:
It's been known since Russell that in higher-order logic (using
quantification over propositional and higher-type variables) that we can
define various propositional connectives, and can even form a version of
type theory based on equality. For example, in Lambek-Scott, our
treatment of Full Impredicative Intuitionistic Type Theory (e.g. Part II,
Chap. 1, p. 129) and type theory based on Equality (Part II, Chap. 2, p.
133) were inspired not only by Prawitz's 1965 book (Natural Deduction) but
some formulas were literally taken from Russell's 1908 article.
If you then add Curry-Howard to the mixture, assigning proof terms to the
formulas involved, one essentially moves into the modern realm of data
types above.
Cheers,
Phil Scott
========================================================================
From: Daniel Leivant <leivant@cs.indiana.edu>
Subject: Re: Recursive types in polymorphic lambda calculus
To: wadler@research.bell-labs.com (Philip Wadler)
Date: Sat, 15 May 1999 10:31:06 -0500 (EST)
Certainly the basic ideas have been known (for inductive definitions
of sets) by mathematical loogicians for many years before the
second order lambda calculus was invented.
I am sure Kleene had a big role here.
I can vouch on the fly for the exact pedigree, but a good
reference for tracking things down is probably Moschovakis's
1974 monograph "elementary indcution on abstact structures"
For the lambda calculus I am not sure who was first, but I
did things independently from scratch in my paper "contracting proofs
to programs" in odifreddi volume "logic and computer science",
academic press 1990. See in particular chapter 6, but also chapters
5 and 3.
I hope this useful. let me know if I can help otherwise.
I hope you have my paper above, if not i'll email you
a source and/or hard copy.
best wishes -- Daniel
========================================================================
To: Philip Wadler <wadler@research.bell-labs.com>
Subject: Re: Recursive types in polymorphic lambda calculus
Date: Sat, 15 May 1999 17:25:37 -0400
From: Jon Riecke <riecke@research.bell-labs.com>
I'm not exactly sure to whom this is due, but my impression was
that it went back a long way. Also, isn't parametricity required
to prove that the encoding yields an initial algebra?
There's some more recent work of Plotkin's that others might not
be aware of: if one takes *linear* polymorphic lambda calculus
with term recursion, plus some modest axioms for parametricity,
one can code up recursive types whose type variable appears with
any variance (covariant, contravariant, or mixed variance). I can
dig up precise references to his talks on the subject.
-Jon
========================================================================
From: "John C Mitchell" <mitchell@cs.stanford.edu>
To: "Philip Wadler" <wadler@research.bell-labs.com>
Subject: RE: categories: Recursive types in polymorphic lambda calculus
I think this is Reynolds and Plotkin, the first incarnation of
the idea coming from Reynolds. I remember looking into this when
I was a graduate student, but I think it was their idea first.
The idea comes from category theory, or Smyth-Plotkin approach,
most specifically -- the obvious type for an initial F-algebra
is All t. (F(t) -> t) -> t.
John
========================================================================
To: Philip Wadler <wadler@research.bell-labs.com>
cc: Andrew.Pitts@cl.cam.ac.uk
Subject: Re: Recursive types in polymorphic lambda calculus
Date: Mon, 17 May 1999 09:02:39 +0100
From: Andrew Pitts <Andrew.Pitts@cl.cam.ac.uk>
I think the best place in the literature to look is
@Article{ReynoldsJC:funept,
author = {J.~C.~Reynolds and G.~D.~Plotkin},
title = {On Functors Expressible in the Polymorphic Typed
Lambda Calculus},
journal = {Information and Computation},
year = 1993,
volume = 105,
pages = {1--29}
}
There is some discussion of the origin of the encoding at the
beginning of this paper. I guess special cases of it were known to
Girard (he covers some in Proofs and Types, without history of
course). The case of algebraic signatures (ie T a sum of products) was
worked out in full generality in Bohm & Berarducci (TCS
39(1985)135--154), although the Reynolds-Plotkin paper also refers to
a paper by Leivant in 24th FOCS (1983) for this case. However, the
general case of a definable covariant functor T seems to be down to
Reynolds-Plotkin. I've taken to referring to this general case as the
"Reynolds-Plotkin" lemma when I refer to it in lectures. One important
question is what properties tyhe encoding has. Up to beta conversion,
rec X.F[X] = all X.(F[X] -> X) -> X
gives a weak initial algebra for F. In the presence of relational
parametricity properties, one can deduce that it is actually
initial. Which brings me to the final place in the literature to look
for material on this topic:
@inproceedings{PlotkinGD:logpp,
author = {G.~D.~Plotkin and M.~Abadi},
title = {A Logic for Parametric Polymorphism},
booktitle = {Typed Lambda Calculus and Applications},
editor = {M.~Bezem and J.~F.~Groote},
volume = 664,
series = {Lecture Notes in Computer Science},
year = 1993,
publisher = {Springer-Verlag, Berlin},
pages = {361--375},
}
Best wishes,
Andy
========================================================================
Date: Mon, 17 May 1999 11:03:10 +0200
From: Giuseppe Rosolini <rosolini@disi.unige.it>
To: Philip Wadler <wadler@research.bell-labs.com>
CC: Edmund Robinson <E.P.Robinson@dcs.qmw.ac.uk>
Subject: Re: categories: Recursive types in polymorphic lambda calculus
Dear Phil,
in a paper at LICS 5, Edumnd Robinson and I use an adaptation of the
usual argument you quote. We assumed that it came from the original
work of Reynolds and Plotkin on non-existence of set-theoretic models
for polymorphic lambda calculus.
Hope this is useful.
Ciao Pino
@article {MR94h:03036,
AUTHOR = {Reynolds, John C. and Plotkin, Gordon D.},
TITLE = {On functors expressible in the polymorphic typed lambda
calculus},
JOURNAL = {Inform. and Comput.},
FJOURNAL = {Information and Computation},
VOLUME = {105},
YEAR = {1993},
NUMBER = {1},
PAGES = {1--29},
ISSN = {0890-5401},
}
@incollection {MR86e:03016,
AUTHOR = {Reynolds, John C.},
TITLE = {Polymorphism is not set-theoretic},
BOOKTITLE = {Semantics of data types (Valbonne, 1984)},
PAGES = {145--156},
PUBLISHER = {Springer},
ADDRESS = {Berlin},
YEAR = {1984},
}
@incollection {MR1099156,
AUTHOR = {Robinson, Edmund and Rosolini, Giuseppe},
TITLE = {Polymorphism, set theory, and call-by-value},
BOOKTITLE = {Fifth Annual IEEE Symposium on Logic in Computer Science
(Philadelphia, PA, 1990)},
PAGES = {12--18},
PUBLISHER = {IEEE Comput. Soc. Press},
ADDRESS = {Los Alamitos, CA},
YEAR = {1990},
}
========================================================================
From: Mitchell Wand <wand@ccs.neu.edu>
Date: Mon, 17 May 1999 09:37:40 -0400 (EDT)
To: Philip Wadler <wadler@research.bell-labs.com>
Subject: Recursive types in polymorphic lambda calculus
Are you thinking of the Bohm-Berarducci coding? The Bohm-Berarducci coding
types the integers
rec X. (1 + X)
as
all X. (X->X) -> (X -> X)
which is not far from all X. ((1 + X) -> X) -> X , depending on how you want
to treat + . I usually cite Girard-Lafont-Taylor for this.
--Mitch
========================================================================
From: Nick Benton <nick@microsoft.com>
To: "'Philip Wadler'" <wadler@research.bell-labs.com>
Subject: RE: categories: Recursive types in polymorphic lambda calculus
Date: Mon, 17 May 1999 09:03:32 -0700
I'd say algebraic or inductive rather then recursive in this context.
(Though of course, there's a coalgebraic version too, but recursive seems to
imply mixed-variance) I think the usual references for the fact that one can
construct weakly initial algebras for expressible functors are:
C. Bohm and A. Berarducci. Automatic synthesis of typed \Lambda-programs on
term algebras. TCS 39 (1985)
D. Leivant. Reasoning about functional programs and complexity classes
associated with type disciplines. FOCS 24 (1983)
G. Takeuti. Proof Theory. North-Holland studies in logic and the foundations
of mathematics. (1975)
The construction is explained in Proofs and Types (Girard Lafont Taylor, CUP
1989) Chapter 11. The construction gives strongly initial algebras if the
calculus satisfies some parametricity theorems.
I think I first saw the coalgebraic version in something by Gavin Wraith,
but I seem to have misplaced the reference.
Nick
========================================================================
From: Robert Harper <Robert.Harper@cs.cmu.edu>
To: "'Philip Wadler'" <wadler@research.bell-labs.com>
Subject: RE: categories: Recursive types in polymorphic lambda calculus
Date: Mon, 17 May 1999 13:46:55 -0400
Hi Phil:
I don't know who discovered this, but certainly Reynolds exploited
it in his paper (eventually with Plotkin) "Polymorphism is not
Set-Theoretic". There he uses F[X] = (X -> 2) -> 2, where X occurs doubly
negatively, hence positively (but not strictly positively). The argument is
essentially Cantor's diagonal argument, once you get down to it. The crux
of the issue is that the syntax provides only weakly initial algebras for
definable functors (no uniqueness condition on the mediating morphism),
whereas a set model gives initial algebras, hence we'd have a set isomorphic
to its double powerset, which is impossible. The key is that Set has enough
equalizers to turn any weakly initial algebra into an initial algebra;
models like Cpo have essentially no equalizers, so they form a valid model.
Bob
========================================================================
Date: Mon, 17 May 1999 18:15:57 +0200
From: Pawel Urzyczyn <urzy@mimuw.edu.pl>
To: wadler@research.bell-labs.com
Subject: Re: Recursive types in polymorphic lambda calculus
Cc: urzy@absurd.mimuw.edu.pl, zs@pwr.wroc.pl
Dear Philip,
As far as I know, representation in \2 of inductive data types (least
fixpoints of monotonic operators) like natural numbers
or lists dates back to the paper of Bohm and Berarducci in
TCS 1985. A generic translation similar to the one you mention
in your types message was probably first given in
H.~Geuvers.
Inductive and coinductive types with iteration and recursion.
In {\em Proceedings of the Workshop on Types for Proofs and
Programs}, B{\aa}stad, Sweden, 1992, 193--217.
but to my understanding it is implicitly present in
Leivant, D., Contracting proofs to programs,
in: {\it Logic in Computer Science\/} (P.~Odifreddi, ed.),
Academic Press, 1990, pp. 279--327.
Let me point out however that there are various definitions
of inductive and recursive types and it is not the case that
all these are equivalent. In general the systems with "iterators"
can be defined within system F, while those with "recursors" can not.
A discussion of these issues is given in the PhD Thesis of Zdzislaw
Splawski:
Sp\l awski, Z., {\it Proof-Theoretic Approach to Inductive
Definitions in ML-like Programming Language versus Second-Order Lambda
Calculus\/}, PhD Thesis, Wroc\l aw University, 1993.
The following paper contains the main results about translatability
between various systems with inductive types, including the new result
that recursors cannot be implemented within system F by means of beta
reduction. It should be made available in a few weeks (we will post
an anouncements on types when it is ready).
Splawski, Z., Urzyczyn, P., Type Fixpoints: Iteration versus Recursion,
to appear in Proc. 4th ICFP, Paris, France, September 1999.
Sincerely yours,
Pawel Urzyczyn
========================================================================
Date: Mon, 17 May 1999 23:35:27 +0200
From: Bernhard Reus <reus@informatik.uni-muenchen.de>
To: Philip Wadler <wadler@research.bell-labs.com>
Subject: Re: categories: Recursive types in polymorphic lambda calculus
Dear Phil,
Well, in fact this is not quite the recursive type you "really" want
since you cannot prove uniqueness of elimination. You just have a weakly
initial solution of your domain equation F(X) = X. So you must e.g. add
an induction principle if you want to prove something. In a dependently
typed calculus (CoC) with an impredicative universe you could even
express the *initial* solution.
Categorically, this goes back to FAFT and the "solution set condition"
where the existence of a left adjoint is related to the existence of
initial objects. If the category of discourse is locally small and
internally complete, then the category has an initial object:
I = { x \in W | forall h \in Hom(W,W). h(p) = p }
where W is the weakly initial object constructed as T above and "all"
ranges over the set of objects of the category. (this is e.g. discussed
in Crole's book "Categories for Types", if I remember correctly, and
maybe there one can find more references.)
Type theoretically speaking, you can find the encoding already in Girard
et al.'s "Proofs and Types". Just with the difference that maps k :
F(X)->X are spelled out for concrete examples of F. "Fold" is called
"It" there and "in" is again given in form of several constructors
depending on the concrete form of F. "Out" is obviously a simple
application of "fold" and was not treated there.
I'm not sure that this really is what you are searching for, so if not
-- e.g. if you want to find a reference with "exactly" the formulation
you mentioned --, please accept my excuses.
Regards,
Bernhard
========================================================================
Philip Wadler wadler@research.bell-labs.com
Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler
600 Mountain Ave, room 2T-402 office: +1 908 582 4004
Murray Hill, NJ 07974-0636 fax: +1 908 582 5857
USA home: +1 908 626 9252
-----------------------------------------------------------------------
"Verbosity leads to unclear, inarticulate things." --Dan Quayle
-----------------------------------------------------------------------