<p>First, your friend is wrong about the history of the $\lambda$-calculus. Church created the untyped calculus first, which he intended as a foundation for mathematics. Fairly quickly, it was discovered that the logic derived from this calculus was inconsistent (because non-terminating programs existed).  Eventually Church developed the simple theory of types as well, and many other things besides, but that wasn't the original point of the system.</p>

<p>An excellent overview of the history is found <a href="http://hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf">in this paper</a>.</p>

<p>Second, the simply-typed lambda calculus is a quite restrictive language. You need some form of recursive type to write any interesting kind of program in it. Certainly, it would be impossible to write the kinds of programs in McCarthy's original paper with the $\lambda$-calculi based type systems understood in 1958. Cutting-edge programming type systems at that point were the ones found in Fortran and COBOL.</p>

CC BY-SA 3.0
2014-06-25T22:05:14.167Z
Wow - answered by the most qualified person in the world on this topic. Thanks @Sam. Perhaps I'll get a Phd application in to you by the end of the year. (It sounds like Ambrose BS is looking forward to working with you guys).
hawkeye
CC BY-SA 3.0
2014-06-27T14:31:48.767Z
I'm really very far from the most qualified person in the world on this topic.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2016-06-23T21:47:52.250Z
The link appears to be broken. I believe this is the same paper: http://hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf
bmaddy
CC BY-SA 3.0
2014-06-25T13:25:35.420Z
2016-07-04T15:46:39.150Z
2016-07-04T15:46:39.150Z
Sam Tobin-Hochstadt
<p>I was having a discussion with a friend recently (who is an advocate of strongly typed languages). He made the comment:</p>

<blockquote>
  <p>The inventors of Lambda Calculus always intended it to be typed. </p>
</blockquote>

<p>Now we can see that <a href="http://en.wikipedia.org/wiki/Alonzo_Church">Church</a> <a href="http://en.wikipedia.org/wiki/Lambda_calculus#Typed_lambda_calculi">was associated with</a> the <a href="http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus">Simply</a> Typed <a href="http://en.wikipedia.org/wiki/Typed_lambda_calculus">Lambda Calculus</a>. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus. </p>

<p>Now when John McCarthy created Lisp - he <a href="http://en.wikipedia.org/wiki/John_McCarthy_%28computer_scientist%29#Career_in_computer_science">based it on the Lambda Calculus</a>. This is by his own admission when he published <a href="http://dl.acm.org/citation.cfm?id=367199">"Recursive functions of symbolic expressions and their computation by machine, Part I"</a>. You can <a href="http://dspace.mit.edu/bitstream/handle/1721.1/6096/AIM-008.pdf?sequence=2">read it here</a>. </p>

<p>McCarthy appears not to have addressed the Simply Typed Lambda Calculus. This seems to be dominated by <a href="http://en.wikipedia.org/wiki/Robin_Milner">Robyn Milner</a> with <a href="http://en.wikipedia.org/wiki/ML_%28programming_language%29">ML</a>. </p>

<p>There is some discussion of the relationship between Lisp and Lambda Calculus <a href="https://groups.google.com/forum/#!topic/comp.lang.lisp/VeMa1B3ZF6Y">here</a>, but they don't really get to the bottom of why McCarthy chose to leave it untyped. </p>

<p>My question is - <strong>If McCarthy admits he knew about Lambda Calculus - why did he ignore the Typed Lambda calculus?</strong> (ie - is it truly obvious that Lambda Calculus was intended to be typed? It doesn't seem that way)</p>

CC BY-SA 3.0
2014-06-24T08:06:34.637Z
Probably has something to do with the Typed Lambda Calculus not being Turing-complete.
Jan Johannsen
CC BY-SA 3.0
2014-06-24T11:00:53.013Z
Thanks @JanJohannsen - could you expand on that?
hawkeye
<lambda-calculus><church-turing-thesis><lisp><typed-lambda-calculus>
Historic Relationship between Typed Lambda Calculus and Lisp?
hawkeye
# Historic Relationship between Typed Lambda Calculus and Lisp?

(Asked by: username_0 on 2014-06-23)

I was having a discussion with a friend recently (who is an advocate of strongly typed languages). He made the comment:

> The inventors of Lambda Calculus always intended it to be typed.

Now we can see that [Church](http://en.wikipedia.org/wiki/Alonzo_Church) [was associated with](http://en.wikipedia.org/wiki/Lambda_calculus#Typed_lambda_calculi) the [Simply](http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) Typed [Lambda Calculus](http://en.wikipedia.org/wiki/Typed_lambda_calculus). Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus.

Now when John McCarthy created Lisp - he [based it on the Lambda Calculus](http://en.wikipedia.org/wiki/John_McCarthy_%28computer_scientist%29#Career_in_computer_science). This is by his own admission when he published ["Recursive functions of symbolic expressions and their computation by machine, Part I"](http://dl.acm.org/citation.cfm?id=367199). You can [read it here](http://dspace.mit.edu/bitstream/handle/1721.1/6096/AIM-008.pdf?sequence=2).

McCarthy appears not to have addressed the Simply Typed Lambda Calculus. This seems to be dominated by [Robyn Milner](http://en.wikipedia.org/wiki/Robin_Milner) with [ML](http://en.wikipedia.org/wiki/ML_%28programming_language%29).

There is some discussion of the relationship between Lisp and Lambda Calculus [here](https://groups.google.com/forum/#!topic/comp.lang.lisp/VeMa1B3ZF6Y), but they don't really get to the bottom of why McCarthy chose to leave it untyped.

My question is - **If McCarthy admits he knew about Lambda Calculus - why did he ignore the Typed Lambda calculus?** (ie - is it truly obvious that Lambda Calculus was intended to be typed? It doesn't seem that way)

**Tags:** lambda-calculus, church-turing-thesis, lisp, typed-lambda-calculus

> **Comments:**
> **username_1**: Probably has something to do with the Typed Lambda Calculus not being Turing-complete.  
> **username_0**: Thanks @JanJohannsen - could you expand on that?  

---

## 1 answers

### Answer by username_2 on 2014-06-25. Score: 19 | Accepted answer

First, your friend is wrong about the history of the $\lambda$-calculus. Church created the untyped calculus first, which he intended as a foundation for mathematics. Fairly quickly, it was discovered that the logic derived from this calculus was inconsistent (because non-terminating programs existed). Eventually Church developed the simple theory of types as well, and many other things besides, but that wasn't the original point of the system.

An excellent overview of the history is found [in this paper](http://hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf).

Second, the simply-typed lambda calculus is a quite restrictive language. You need some form of recursive type to write any interesting kind of program in it. Certainly, it would be impossible to write the kinds of programs in McCarthy's original paper with the $\lambda$-calculi based type systems understood in 1958. Cutting-edge programming type systems at that point were the ones found in Fortran and COBOL.

> **Comments:**
> **username_0**: Wow - answered by the most qualified person in the world on this topic. Thanks @Sam. Perhaps I'll get a Phd application in to you by the end of the year. (It sounds like Ambrose BS is looking forward to working with you guys).  
> **username_2**: I'm really very far from the most qualified person in the world on this topic.  
> **username_3**: The link appears to be broken. I believe this is the same paper: http://hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf  

---

