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

Re: intellectual history of types

Many thanks to everyone that responded to my query.  Here is a complete
summary of what I got...

        B

----------------------------------------------------------------------
Philip Wadler <wadler@nslocum.cs.bell-labs.com>

Jean van Heijenoort, From Frege to Godel,
A sourcebook in Mathematical Logic, 1879-1931
Harvard University Press, 1967

  Includes material by Frege and Russell.  But there is no specific
  focus on types, and indeed one might argue that types are
  underrepresented.

Twan Laan
The evolution of type theory in logic and mathematics

  Explains Russell's ramified theory of types from a computing
  perspective.  Goes back through the history (Russell, Curry, etc.)
  and puts together a modern synthesis of the historical ideas.
  By far the best introduction I've seen to Russell's type theory for
  computer scientists.

Philip Wadler

Philip Wadler, Proofs are Programs: 19th Century Logic and 21st
Century Computing. This is a variant of another article, New
Languages, Old Logic, that appeared in Dr Dobbs Journal, special
supplement on Software in the 21st century, December 2000.
http://www.cs.bell-labs.com/who/wadler/topics/history.html

  As the 19th century drew to a close, logicians formalized an ideal
  notion of proof. They were driven by nothing other than an abiding
  interest in truth, and their proofs were as ethereal as the mind of
  God. Yet within decades these mathematical abstractions were realized
  by the hand of man, in the digital stored-program computer. How it
  came to be recognized that proofs and programs are the same thing is a
  story that spans a century, a chase with as many twists and turns as a
  thriller. At the end of the story is a new principle for designing
  programming languages that will guide computers into the 21st century.

  [I hope some day to write a longer and better version.  Any comments
  gratefully received.]

----------------------------------------------------------------------
Daniel Leivant <leivant@cs.indiana.edu>

a good overview of type-theoretic approach to the foundations of
set theory is chapter 3 of "Foundations of Set Theory" by Fraenkel, 
Bar-Hillel and Levy.  It's an older and source which is too often
overlooked, so i mention it in particular.

You might also find something useful in my chapter on higher order logic 
in D.M. Gabbay, C.J. Hogger, J.A. Robinson and J. Siekmann (editors),
Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2:
Deduction Methodologies,
Oxford University Press, Oxford, 1994, pp.~230--321.
If you do look there and have any comments, I would be most interested:
a second edition is in preparation, and I need to revise my chapter.

----------------------------------------------------------------------
Hans-Joerg Tiede <htiede@titan.iwu.edu>

I saw your recent posting to the types mailing list asking about a
survey of the history/philosophy of types. The first article that I
thought of, which you probably know, is Robert Constable's survey of
types in computer science, philosophy, and logic in the "Handbook of
Proof Theory" (ed. Samuel Buss). It has a very extensive bibliography.
As a matter of fact, a number of articles in that collection are
probably of interest to type theorists. Also, Quine's book "Set Theory
and it's Logic" has a chapter on type theory that discusses some of the
philosophical origins of Russell's theory of types as a foundation for
set theory.

----------------------------------------------------------------------
Gerard Huet <Gerard.Huet@inria.fr>

I am not sure such an ambitious survey exists at this point. 
Among my modest attempt at a historical perspective, you may be interested
to have a look at my short introduction to part 3 of "Logical Foundations
of Functional Programming", ed G Huet Addison Wesley 1990. In the same
volume I also give a uniform presentation of type theory, pp 337 to 397, a
condensed presentation of my course at CMU; the article by Thierry Coquand
on the analogy between propositions and types is also relevant I believe. I
do not know if this book is easy to get, nowadays, but Andre Scedrov must
have a copy, since he contributed.

PS Seldin has a very extensive bibliography on types. You should also lok
up the Curry volume.
You may be interested to know that I stumbled on the topic back in 1970
when I read Curry&Feys vol I, which was such an intriguing material that I
could not make up my mind if it was philosophy or maths !

----------------------------------------------------------------------
Pierre Lescanne <Pierre.Lescanne@ens-lyon.fr>

I do not know whether this is really relevant, but you may be
interested by what Gerhard.Heinzmann@clsh.univ-nancy2.fr collected.
He wrote an interesting monography (edited by an obscure French
publisher) where he collected papers by Peano, Russell, Zermelo,
Poincare etc, about the debate on the foundation of mathematics.  This
is very interesting in the sense that Gerhard Heinzmann put together
papers that are scattered.


    Heinzmann, Gerhard (éd), Poincaré, Russell, Zermelo et Peano,
Textes de la discussion (1906-1912) sur les fondements des
mathématiques : des antinomies à la prédicativité, Paris : Blanchard,
1986.

----------------------------------------------------------------------
Judith Underwood <judith@qss.co.uk>

I can't lay my hands on it at the minute so I can't check
exactly what it says about types, but I remember 
_Philosophy of Mathematics: Selected Readings_ (Paul
Benacerraf and Hilary Putnam, eds) as being interesting
and useful. 

----------------------------------------------------------------------
Sandeep Kumar Shukla <skshukla@mipos2.intel.com>

I guess you have to start with Bertrand Russel's famous book
(Principia Mathematica 3 volumes ?), and Russell's paradox and other
issues in Foundations of Mathematics that extensively dealt with
notion of types in the early 20th century.  However, I guess
Mathematical set theoriticians also are quite extensively responsible
for the development of the notion of types and type hierarchy. I
remember, the notions from the work of Cantor, and the diagonalization
arguments of various kinds gave rise to ideas similar to types (I am not sure,
 just my interpretation of history!)