Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!wuarchive!rex!fs
From: fs@rex.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.functional
Subject: Re: System F
Message-ID: <3960@rex.cs.tulane.edu>
Date: 29 Jul 90 03:21:46 GMT
References: <3477@goanna.cs.rmit.oz.au>
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 29


<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