Thread View: comp.lang.functional
6 messages
6 total messages
Started by Richard A. O'Keefe
Sat, 28 Jul 1990 10:19
System F
Author: Richard A. O'Keefe
Date: Sat, 28 Jul 1990 10:19
Date: Sat, 28 Jul 1990 10:19
27 lines
1721 bytes
1721 bytes
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)
Re: System F
Author: Frank Silbermann
Date: Sun, 29 Jul 1990 03:21
Date: Sun, 29 Jul 1990 03:21
29 lines
1647 bytes
1647 bytes
<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
Re: System F
Author: Philip Wadler
Date: Mon, 30 Jul 1990 12:18
Date: Mon, 30 Jul 1990 12:18
20 lines
1236 bytes
1236 bytes
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
Re: System F
Author: Dipankar Gupta
Date: Tue, 31 Jul 1990 03:13
Date: Tue, 31 Jul 1990 03:13
28 lines
1407 bytes
1407 bytes
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
Re: System F
Author: Al Reich
Date: Fri, 03 Aug 1990 17:42
Date: Fri, 03 Aug 1990 17:42
16 lines
905 bytes
905 bytes
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
Re: System F
Author: Mark Leone
Date: Mon, 06 Aug 1990 15:00
Date: Mon, 06 Aug 1990 15:00
17 lines
1034 bytes
1034 bytes
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
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads