Why was typed lambda calculus not used?
Author Message
Why was typed lambda calculus not used?

Church's typed lambda calculus, published in 1940, seems to be at
least as interesting as his type-free lambda calculus published four
years earlier, yet the various implementations of Lisp that I find
today seem to be based exclusively on Church's type-free lambda
calculus.

Is this merely because versions of Lisp that are based on Church's
typed lambda calculus exist but I am not aware of the fact, or is it
because the first developers of Lisp debated the question and decided
to base Lisp on Church's type-free lambda calculus instead of basing
it on his typed lambda calculus?

Bill

M-x shell RET
--**-Emacs: *post-news* (News Fill)--L22--All-----------------------------
Wrong type argument:keymapp, 1

--

If you can find a better Unix than Linux, buy it.

Wed, 23 Apr 1997 16:49:12 GMT
Why was typed lambda calculus not used?

Quote:

>  Church's typed lambda calculus, published in 1940, seems to be at
>least as interesting as his type-free lambda calculus published four
>years earlier, yet the various implementations of Lisp that I find
>today seem to be based exclusively on Church's type-free lambda
>calculus.

>  Is this merely because versions of Lisp that are based on Church's
>typed lambda calculus exist but I am not aware of the fact, or is it
>because the first developers of Lisp debated the question and decided
>to base Lisp on Church's type-free lambda calculus instead of basing
>it on his typed lambda calculus?

McCarthy freely admits that he didn't really understand _any_ lambda
calculus when he invented the first Lisp.  If he _had_ understood,
then it would have had static variable scoping, and probably lazy
evaluation, as well.  I seem to recall that he briefly glanced at
Curry & Feys, but didn't understand the alpha-renaming rule (the one
that does static variable scoping).

On the other hand, Lisp had 'eval' and cons cells, which the lambda
calculus didn't have.

So it is probable that he wasn't aware of the typed lambda calculus at
the time.

Michael Levin is one of the early Lisp people who had a mathematical
logic bent, and he prepared some course notes at MIT which I found
absolutely fascinating.  I highly recommend getting MIT/LCS/TR-131,
'Mathematical Logic for Computer Scientists', Michael Levin, June
1974, approx. 175 pages.  It proves undecidability by means of Lisp
eval.

Henry Baker

Sat, 26 Apr 1997 03:15:20 GMT
Why was typed lambda calculus not used?

Quote:

>>  Is this merely because versions of Lisp that are based on Church's
>>typed lambda calculus exist but I am not aware of the fact, or is it
>>because the first developers of Lisp debated the question and decided
>>to base Lisp on Church's type-free lambda calculus instead of basing
>>it on his typed lambda calculus?
>McCarthy freely admits that he didn't really understand _any_ lambda
>calculus when he invented the first Lisp.

Quote:
>So it is probable that he wasn't aware of the typed lambda calculus at
>the time.

That sounds right to me; the similarity between Lisp and \-calculus
has probably been noticed after Lisp was created.  However, we might
still ask ourselves why Lisp is so similar to type-free \-calculus,
and not to typed \-calculus.
First of all, the original (monomorphic) \-calculus is not
Turing-complete; in other words, there are results that you can get
with a computer and that there is no typed \-calculus program to
compute.  This is not so with untyped \-calulus (by Church's thesis).
Yet, there are other, more complicated, typed \-calculi that are
Turing-complete, and in fact ML can be thought of as being based on
some sort of typed \-calculus.
But the main reason for using untyped \-calculus is that having
strong typing implies either making the programmmer type all his
expressions by hand, or having a type-inference algorithm.  This is by
no means a trivial task, and is *undecidable* for the polymorphic type
systems.  (Yes, I know, ML does type inference, but the Hindley-Milner
algorithm artificially restricts recursive definitions to be of a
monomorphic type).
With hindsight, it seems very natural that McCarthy had decided not
to type the expressions of his language.
J. Chroboczek

Sat, 26 Apr 1997 04:33:09 GMT
Why was typed lambda calculus not used?

Quote:

>  Church's typed lambda calculus, published in 1940, seems to be at
>least as interesting as his type-free lambda calculus published four
>years earlier, yet the various implementations of Lisp that I find
>today seem to be based exclusively on Church's type-free lambda
>calculus.
>  Is this merely because versions of Lisp that are based on Church's
>typed lambda calculus exist but I am not aware of the fact, or is it
>because the first developers of Lisp debated the question and decided
>to base Lisp on Church's type-free lambda calculus instead of basing
>it on his typed lambda calculus?

In a way SML is such a beast. Uses an Algol-like syntax, but otherwise
it's a lot like a strongly typed Lisp.
--
%%%%%%%%%%%%%%%}- Martin             Smile!  :-)

Sat, 26 Apr 1997 15:36:18 GMT
Why was typed lambda calculus not used?

writes:

Quote:

>>McCarthy freely admits that he didn't really understand _any_ lambda
>>calculus when he invented the first Lisp.
>>So it is probable that he wasn't aware of the typed lambda calculus at
>>the time.
>That sounds right to me; the similarity between Lisp and \-calculus has
>probably been noticed after Lisp was created.  However, we might still ask
>ourselves why Lisp is so similar to type-free \-calculus, and not to typed
>\-calculus.

From McCarthy, "Recursive Functions of Symbolic Expressions and Their
Computation by Machine, Part I" (_Communcations of the ACM_ vol. 3 number 4,
April 1960, pp. 184-195):

e. {\it Functions and Forms}. It is usual in mathematics--
outside of mathematical logic--to use the word function''
imprecisely and to apply it to forms such as $y^2 + x$.
Because we shall later compute with expressions for functions,
we need a distinction between functions and forms and a
notation for expressing this distinction.  This distinction
and a notation for describing it, from which we deviate
trivially, is given by Church [3].

Reference 3 is

A. Church, {\it The Calculi of Lambda-Conversion} (Princeton
University Press, Princeton, N. J., 1941).

Earlier in the McCarthy paper, he states that the original idea for Lisp arose
in 1958.  I don't have Stoyan's book to check, but I think LAMBDA existed even
then.

Note that JMC's statement is that he did not *understand* lambda-calculus, not
that he was unfamiliar with any particular form thereof.  And given his back-
ground in recursion theory, I'd be more surprised if he *were* unfamiliar with
it than not.

Not proof of anything, of course...
--
Rich Alderson   You know the sort of thing that you can find in any dictionary
of a strange language, and which so e{*filter*}s the amateur philo-
logists, itching to derive one tongue from another that they
know better: a word that is nearly the same in form and meaning
as the corresponding word in English, or Latin, or Hebrew, or
what not.
--J. R. R. Tolkien,

Sun, 27 Apr 1997 08:37:55 GMT
Why was typed lambda calculus not used?

>> Church's typed lambda calculus, published in 1940, seems to be at
>> least as interesting as his type-free lambda calculus published four
>> years earlier, yet the various implementations of Lisp that I find
>> today seem to be based exclusively on Church's type-free lambda
>> calculus.

>> Is this merely because versions of Lisp that are based on Church's
>> typed lambda calculus exist but I am not aware of the fact, or is it
>> because the first developers of Lisp debated the question and decided
>> to base Lisp on Church's type-free lambda calculus instead of basing
>> it on his typed lambda calculus?

MC> In a way SML is such a beast. Uses an Algol-like syntax, but otherwise
MC> it's a lot like a strongly typed Lisp.
MC> --

Well, I am somewhat aware of SML, in the sense that I am somewhat
aware of "C" -- i.e., I know what it looks like but I have never done
anything with it other than to compile programs written in it by
others -- and I suppose SML is, in some abstract sense, equivalent to
the sort of strongly-typed Lisp I have in mind, but it seems to me
there is only one Lisp in the sense that what Lisp is made of and what
Lisp is about is one and the same thing: S-expressions, like

(lambda (x y z)(cons x (cons y (cons z (quote ())))))

I suspect this is what gives programming in Lisp what for lack of a
better word might be called its distinctive "feel" and makes it such a
peculiarly _absorbing_ experience; in any case, it is not something I
would be willing to give up to get types unless it were necessary
which it does not appear to me to be.

Bill

--

If you can find a better Unix than Linux, buy it!

Mon, 28 Apr 1997 04:37:40 GMT
Why was typed lambda calculus not used?

Quote:

>>>McCarthy freely admits that he didn't really understand _any_ lambda
>>>calculus when he invented the first Lisp.

>Reference 3 [of Recusive Functions of Symbolic Expressions] is
>    A. Church, {\it The Calculi of Lambda-Conversion} (Princeton
>      University Press, Princeton, N. J., 1941).

>Earlier in the McCarthy paper, he states that the original idea for Lisp arose
>in 1958.  I don't have Stoyan's book to check, but I think LAMBDA existed even
>then.

>Note that JMC's statement is that he did not *understand* lambda-calculus, not
>that he was unfamiliar with any particular form thereof.  And given his back-
>ground in recursion theory, I'd be more surprised if he *were* unfamiliar with
>it than not.

According to McCarthy's 'History of Lisp', Sigplan Not. 13,8 (Aug
1978), James Slagle had an environment bug due to what we now call
dynamic scoping and Steve Russell invented the FUNARG (function
closure) to solve it.  McCarthy says "I must confess that I regarded
this difficulty as just a bug".  McCarthy then referenes Joel Moses's
paper 'The Function of FUNCTION in Lisp', MIT AI Memo 199, Proj. Mac Memo
428, June 1970.

Moses doesn't give much more history, but references an unpublished memo
"The FUNARG Problem Explained" by J. Weizenbaum, 1968, which I don't have
a copy of.

My statement re McCarthy may be hearsay from one or more of the following
sources: Moses, Weizenbaum, Levin, Greenblatt, Hewitt.

The last time I really tried to understand this history was in the context
of my Shallow Binding paper.

Henry Baker

Mon, 28 Apr 1997 01:11:12 GMT
Why was typed lambda calculus not used?

Thank you for your interesting response to my "history question".

I wonder if you would care to elaborate on the following:

JC> First of all, the original (monomorphic) \-calculus is not
JC> Turing-complete; in other words, there are results that you can get
JC> with a computer and that there is no typed \-calculus program to
JC> compute.

As I understand it (or misunderstand it), to say that a Turing
machine cam compute something is to say that it is possible to write
down an algorithm which when appropriately encoded and presented to
the machine will cause the machine to traverse a sequence of states
from A to B such that (the difference between A and) B represents that
which was to be computed.

If so, given that a Turing machine is a deterministic function of its
input instructions and its transition function, both of which can be
expressed (easily) in the non-typed lambda calculus, how can it be
possible to compute something on a Turing machine that cannot be
expressed in the *typed* lambda caclulus?

Can you give me an example?

Bill

--

If you can find a better Unix than Linux, buy it!

Mon, 28 Apr 1997 13:36:20 GMT
Why was typed lambda calculus not used?

Quote:

>     As I understand it (or misunderstand it), to say that a Turing
>machine cam compute something is to say that it is possible to write
>down an algorithm which when appropriately encoded and presented to
>the machine will cause the machine to traverse a sequence of states
>from A to B such that (the difference between A and) B represents that
>which was to be computed.

>    If so, given that a Turing machine is a deterministic function of its
>input instructions and its transition function, both of which can be
>expressed (easily) in the non-typed lambda calculus, how can it be
>possible to compute something on a Turing machine that cannot be
>expressed in the *typed* lambda caclulus?

Well, the lambda calculus doesn't have a concept of global state, so
there is not a direct correspondence to Turing machines (no
tape). However,  in the untyped lambda calculus, you can implement
recursion by building Y combinators, and once you have recursion you
have all the computational power you need. According to Rosser's
"Highlights of the History of the Lambda Calculus" (Annals of the
History of Computing 6(4), Oct 1984, p 337-349), Turing proved in 1937
(!) that calculable on Turing machines was equivalent to being
definable in the untyped lambda calculus.

But how do you build a Y combinator in a simply typed calculus? The
whole point of the Y combinator is that F(Y(F)) = Y(F) which means
that Y can take any function as an argument: a tall order in a simply
typed language :-).

This doesn't prove that the simply typed lambda calculus is not Turing
Complete, just that the obvious tact doesn't work.

- Marty
(proclaim '(inline skates))

Mon, 28 Apr 1997 22:21:52 GMT
Why was typed lambda calculus not used?

Quote:

>    If so, given that a Turing machine is a deterministic function of its
>input instructions and its transition function, both of which can be
>expressed (easily) in the non-typed lambda calculus, how can it be
>possible to compute something on a Turing machine that cannot be
>expressed in the *typed* lambda caclulus?

Well, it's fairly straightforward to show that programs written in
the pure, simply-typed lambda-calculus always terminate.  You have
to add a Y-combinator or recursive types or something to get non-termination.

-Greg

Tue, 29 Apr 1997 04:36:27 GMT
Why was typed lambda calculus not used?

My recollection is that someone at IU (Indiana U.) implemented
a strongly-typed scheme maybe 10 years ago.
--
Richard Billington

Wed, 30 Apr 1997 00:31:33 GMT

 Page 1 of 1 [ 11 post ]

Relevant Pages