ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) (07/28/90)
I recently bough a copy of Logical Foundations of Functional Programming ed. Gerard Huet Addison-Wesley 1990 ISBN 0-201-17234-8 which is one of the Austin "Year of Programming" series. There's a paper in the "The system F of variable types, 15 years later" by Jean-Yves Girard, and J.C.Reynolds' introduction to that section says that it's essentially the same second-order typed lambda calculus that he came up with. In Reynolds' introduction, he says that - every expression describes a termination computation - every function from natural numbers to natural numbers which can be proved total using second-order arithmetic is expressible in it This is all very interesting. The trouble is that while I would like to know more about it, Girard's article requires rather more category theory than I can remember in order to read it. Is there are much simpler explanation of this stuff anywhere? Huet, in the preface, speaks of "toning down category theory, at least in the title, in order not to discourage practically minded computer scientists with too much abstract intellectual terrorism". I wish he _hadn't_ toned down the title; then I might have known what I was in for. -- Science is all about asking the right questions. | ok@goanna.cs.rmit.oz.au I'm afraid you just asked one of the wrong ones. | (quote from Playfair)
fs@rex.cs.tulane.edu (Frank Silbermann) (07/29/90)
<3477@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au Richard A. O'Keefe: > There's a paper in the "The system F of variable types, 15 years later" > by Jean-Yves Girard, and J.C.Reynolds' introduction to that section says > that it's essentially the same second-order typed lambda calculus that > he came up with. >... > This is all very interesting. The trouble is that while > I would like to know more about it, Girard's article requires > rather more category theory than I can remember in order to read it. > Is there are much simpler explanation of this stuff anywhere? Probably not, unfortunately. In a normal (non-polymorphic) language, every function is defined over a known domain of values, whether given implicitly or explicitly. A polymorphic definition, however, deliberately does _not_ restrict the definition to any one domain, but serves as a schema for defining functions over many domains, all of which share some common properties. The ability to abstract out these common properties of domains and the functions over them -- well was one of the motivations for category theory's development. I just wish I could understand the stuff. Frank Silbermann fs@rex.cs.tulane.edu Tulane University New Orleans, Louisianna USA
wadler@cs.glasgow.ac.uk (Philip Wadler) (07/30/90)
In article <3477@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) writes: >There's a paper "The system F of variable types, 15 years later" >by Jean-Yves Girard ... Is there are much >simpler explanation of this stuff anywhere? Two handy references: J.-Y.\ Girard, Y. Lafont, and P. Taylor, {\em Proofs and Types}. Cambridge University Press, 1989. J. C. Reynolds, Three approaches to type structure. In {\em Mathematical Foundations of Software Development}, LNCS 185, Springer-Verlag, 1985. The Reynold's paper is perhaps the best introduction to type theory for computer scientists in existence. Girard's book provides a more thorough introduction to System F and related systems, including strong normalisation and coherrence semantics. - Phil
dg@otter.hpl.hp.com (Dipankar Gupta) (07/31/90)
In article <3960@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes: > ><3477@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au >Richard A. O'Keefe: > [...deleted ...] >> I would like to know more about it, Girard's article requires >> rather more category theory than I can remember in order to read it. >> Is there are much simpler explanation of this stuff anywhere? > [...deleted...] >The ability to abstract out these common properties of domains >and the functions over them -- well was one of the motivations >for category theory's development. > >I just wish I could understand the stuff. > > Frank Silbermann fs@rex.cs.tulane.edu > Tulane University New Orleans, Louisianna USA Have a look at the book "Computational Category Theory" by Rod Burstall and Rydeheard (I think) which is a "computationally-oriented" (whatever that may mean!) intro to Cat theory and uses ML to introduce cat theoretical concepts. //Dipankar dg@hpl.hplb.hp.com -- Internet Dipankar Gupta/HP9801/00 -- HPDesk
reich@AUSTIN.LOCKHEED.COM (Al Reich) (08/04/90)
I don't know if there's a simpler explanation of second order typed lambda calculus, but I do know of one for category theory: "A Taste of Category Theory for Computer Scientists" by Benjamin C. Pierce CMU-CS-88-203 Computer Science Dept., Carnegie Mellon Univ., Pittsburgh, PA 15213 It includes a tutorial, case studies, a literature survey, and some typographical errors (which aren't hard to find if you read carefully). Al Reich Lockheed - Austin Division
mleone@f.gp.cs.cmu.edu (Mark Leone) (08/06/90)
In article <349@titmouse.AUSTIN.LOCKHEED.COM> reich@AUSTIN.LOCKHEED.COM (Al Reich) writes: >I don't know if there's a simpler explanation of second order >typed lambda calculus, but I do know of one for category theory: > > "A Taste of Category Theory for Computer Scientists" > by Benjamin C. Pierce > CMU-CS-88-203 > Computer Science Dept., Carnegie Mellon Univ., > Pittsburgh, PA 15213 This paper has recently been revised and expanded (March 1990). The new version is available as CMU-CS-90-113 -- Mark R. Leone <mleone@cs.cmu.edu> Computer Science, Carnegie Mellon University Pittsburgh, PA 15213