18
$\begingroup$

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 was associated with the Simply 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. This is by his own admission when he published "Recursive functions of symbolic expressions and their computation by machine, Part I". You can read it here.

McCarthy appears not to have addressed the Simply Typed Lambda Calculus. This seems to be dominated by Robyn Milner with ML.

There is some discussion of the relationship between Lisp and Lambda Calculus here, 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)

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Probably has something to do with the Typed Lambda Calculus not being Turing-complete. $\endgroup$
    – Jan Johannsen
    Commented Jun 24, 2014 at 8:06
  • $\begingroup$ Thanks @JanJohannsen - could you expand on that? $\endgroup$
    – hawkeye
    Commented Jun 24, 2014 at 11:00

1 Answer 1

Reset to default
19
$\begingroup$

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.

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.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ 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). $\endgroup$
    – hawkeye
    Commented Jun 25, 2014 at 22:05
  • 4
    $\begingroup$ I'm really very far from the most qualified person in the world on this topic. $\endgroup$
    – Sam Tobin-Hochstadt
    Commented Jun 27, 2014 at 14:31
  • $\begingroup$ The link appears to be broken. I believe this is the same paper: hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf $\endgroup$
    – bmaddy
    Commented Jun 23, 2016 at 21:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.