Re: new course at Stanford

To: types@theory.LCS.MIT.EDU
Subject: Re: new course at Stanford
From: oravax!garrel@cu-arpa.cs.cornell.edu (Garrel Pottinger)
Date: Mon, 3 Oct 88 05:43:52 EDT
Sender: meyer@theory.LCS.MIT.EDU
Date: Sat, 1 Oct 88 10:49:00 EDT
To: jcm%ra.stanford.edu@STORK.lcs.mit.edu, types@theory.LCS.MIT.EDU
Cc: garrel@wrath.cs.cornell.edu

The course outline looks quite good, but I would like to argue for
a preamble on the type-free lambda calculus.  You need not do much
with that, but, for the following reasons, I think you should begin
by acquainting the students with the basic concepts and results.

The type-free lambda calculus is of interest because it provides
a universal model of computation which is also a functional model.
Unfortunately, the type-free calculus allows us to write down
things which are, at best, strange (e.g., WWW), and, at worst,
vicious (the voracious combinator YK, for example).

When we impose a type discipline on the type-free calculus, we are
attempting avoid such untoward features, while retaining enough power
to suit our computational purposes.

Of course, our computational purposes are various, and it is very
unlikely that a single type discipline will accomodate them all.
Hence, we must deal with a variety of type disciplines.  (I once heard
Roger Hindley remark that typing a lambda term is like describing
a person's character --- in giving such a description, the apposite
evaluative categories will vary, depending on our purpose in giving
it.  Think, for example, about how our character descriptions would
differ if we were to evaluate a given person as a police recruit,
on the one hand, and as a candidate for training as a psychotherapist,
on the other.)

Since we must deal with a variety of type disciplines and the type-free
lambda calculus calculus is the substrate of all of them, a brief
introduction to the type-free calculus is the appropriate starting
point for a study of typed lambda calculi.  (Being acquainted with
human beings in all their diversity will enhance our understanding
of any particular scheme of character description and our facility
in using it.)

Regards,

Garrel Pottinger

Odyssey Research Associates
301A Harris B. Dates Drive
Ithaca, New York 14850-1313

oravax!garrel@cu-arpa.cs.cornell.edu