teach untyped lambda calculus?

To: types@theory.LCS.MIT.EDU
Subject: teach untyped lambda calculus?
From: Matthias Felleisen <matthias@rice.edu>
Date: Thu, 6 Oct 88 23:09:55 EDT
Sender: meyer@theory.LCS.MIT.EDU
Date: Thu, 6 Oct 88 10:15:08 CDT
To: types@theory.LCS.MIT.EDU, jcm%ra.stanford.edu@STORK.lcs.mit.edu
In-Reply-To: John Mitchell's message of Wed, 5 Oct 88 21:41:11 EDT <8810060141.AA00849@stork.LCS.MIT.EDU>

I would like to offer another reason for teaching UNTYPED \-calculus. 

In summary, the reasoning goes as follows: 

(1) The typing of variables in programms contributes as much to the
understanding of programming languages as the unit system of physical
equations to the understanding of physics. (2) Moreover, the current
type structures and type systems of programming languages are more of
a hinderance in my work than of help.

The first sentence is not meant to be an offense but rather a request
for a good answer. I have asked this question often and I have never
received a satisfactory answer. 

For a support of (2) I need to explain what kind of programs I write.
I have recently developed a THEORY OF PROGRAMMING LANGUAGE
EXPRESSIVENESS, which differentiates the EXPRESSIVE POWER of
"Turing-equivalent" programming languages (*). For example, I can show
that a lambda-(value)-calculus language with assignment statements is
MORE EXPRESSIVE than a pure lambda-(value)-calculus. In my course on
programming language theory, I teach this theory and to that end I
need to show a lot of expressiveness relationships.

If I take a weakly typed language as the basis, I can cover a lot of
material on the basis of my expressiveness theory. That is, I can
provide an understanding of how many "voguish" programming facilities
can be understood as EXPRESSED IN a simple base language, and why certain
other facilities are ubiquitous of most existing programming languages
(so to speak the PRINCIPLES OF PROGRAMMING LANGUAGES). On the other
hand, if I take a strongly typed language as my staring point, I get
bogged down by the typing system with trivial little problems: recall
that after all in ML
		LET x BE <exp> in <exp> =/= ((\x.B)M).

Of course, the very point that typed programming languages can express
fewer facilities than untyped languages makes it important that we
study types. But, the important point is that we recognize the TYPE
STRUCTURE of programming languages as ONE OUT OF MANY facets that we
need to understand and THAT WE DON'T OVEREMPHASIZE IT at the cost of
others, in particular, in a course on the INTRODUCTION TO PL THEORY.

 
-- Matthias

(*) I have written an EXTENDED ABSTRACT on the theory of
expressiveness and are willing to distribute it (if somebody is
interested).