Why was typed lambda calculus not used?
Author 
Message 
pp000.. #1 / 11

Why was typed lambda calculus not used?
Church's typed lambda calculus, published in 1940, seems to be at least as interesting as his typefree lambda calculus published four years earlier, yet the various implementations of Lisp that I find today seem to be based exclusively on Church's typefree 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 typefree lambda calculus instead of basing it on his typed lambda calculus? Bill Mx shell RET **Emacs: *postnews* (News Fill)L22All Wrong type argument:keymapp, 1 
If you can find a better Unix than Linux, buy it.

Wed, 23 Apr 1997 16:49:12 GMT 


Henry G. Bak #2 / 11

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 typefree lambda calculus published four >years earlier, yet the various implementations of Lisp that I find >today seem to be based exclusively on Church's typefree 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 typefree 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 alpharenaming 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/TR131, 'Mathematical Logic for Computer Scientists', Michael Levin, June 1974, approx. 175 pages. It proves undecidability by means of Lisp eval. Henry Baker Read ftp.netcom.com:/pub/hbaker/README for info on ftpable papers.

Sat, 26 Apr 1997 03:15:20 GMT 


Juliusz Chrobocz #3 / 11

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 typefree 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.
[comments about \calculus and Lisp deleted] 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 typefree \calculus, and not to typed \calculus. First of all, the original (monomorphic) \calculus is not Turingcomplete; 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 Turingcomplete, 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 typeinference 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 HindleyMilner 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 


Martin Cracau #4 / 11

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 typefree lambda calculus published four >years earlier, yet the various implementations of Lisp that I find >today seem to be based exclusively on Church's typefree 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 typefree lambda calculus instead of basing >it on his typed lambda calculus?
In a way SML is such a beast. Uses an Algollike syntax, but otherwise it's a lot like a strongly typed Lisp.  %%%%%%%%%%%%%%%} Martin Smile! :)

Sat, 26 Apr 1997 15:36:18 GMT 


Richard M. Alderson I #5 / 11

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 typefree \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. 184195): e. {\it Functions and Forms}. It is usual in mathematics outside of mathematical logicto 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 LambdaConversion} (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* lambdacalculus, 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 


bho.. #6 / 11

Why was typed lambda calculus not used?
>> Church's typed lambda calculus, published in 1940, seems to be at >> least as interesting as his typefree lambda calculus published four >> years earlier, yet the various implementations of Lisp that I find >> today seem to be based exclusively on Church's typefree 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 typefree lambda calculus instead of basing >> it on his typed lambda calculus? MC> In a way SML is such a beast. Uses an Algollike 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 stronglytyped 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: Sexpressions, 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 


Henry G. Bak #7 / 11

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 LambdaConversion} (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* lambdacalculus, 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 Read ftp.netcom.com:/pub/hbaker/README for info on ftpable papers.

Mon, 28 Apr 1997 01:11:12 GMT 


bho.. #8 / 11

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> Turingcomplete; 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 nontyped 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 


Marty Ha #9 / 11

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 nontyped 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 337349), 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 


Greg Morrise #10 / 11

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 nontyped 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, simplytyped lambdacalculus always terminate. You have to add a Ycombinator or recursive types or something to get nontermination. Greg

Tue, 29 Apr 1997 04:36:27 GMT 


Richard Billingt #11 / 11

Why was typed lambda calculus not used?
My recollection is that someone at IU (Indiana U.) implemented a stronglytyped scheme maybe 10 years ago.  Richard Billington

Wed, 30 Apr 1997 00:31:33 GMT 


