[Prev][Next][Index][Thread]

Re: teach untyped lambda calculus?



Date: Mon, 10 Oct 88 11:17:30 PDT
To: hudak-paul@yale.arpa
Cc: types@theory.LCS.MIT.EDU

I agree that untyped lambda calculus should be taught.
Last time I tried a course like this, I started with
untyped lambda calculus, but found that many of the
things I wanted to say (about semantics for example,
and "run time type errors" when constants like 0,1, +
are added) required some notion of type. So this time
I thought I'd start with typed lambda calculus, and
consider "untyped" lambda calculus a syntactic variant
of typed lambda calculus with domain equation t=t->t.
I can tell you later how well this works, as compared with
my last attempt.

John