types and pedagogy

• To: types@theory.LCS.MIT.EDU
• Subject: types and pedagogy
• From: gunter@linc.cis.upenn.edu (Carl Gunter)
• Date: Thu, 6 Oct 88 23:22:17 EDT
• Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 6 Oct 88 12:18:15 EDT
Posted-Date: Thu, 6 Oct 88 12:18:15 EDT

I would like to point out another reason for beginning a course on
Programming Language Theory with an exposition of the TYPED lambda
calculus.  Although the syntax of typed systems is slightly more
difficult, this should not be a grave problem for students who are
familiar with strongly typed programming languages.  Moreover, the
SEMANTICS of typed calculi is more perspicuous than the (at first)
mysterious semantics of the untyped calculus.  When the semantics of
the typed lambda calculus has been properly exposited, the meanings of
the untyped terms can be explained clearly in that context using
recursive domain equations.  Even if I knew how it could be done, I do
not think that an attempt to explain the (denotational) semantics of
typed calculi in terms of the untyped calculus would meet with
pedagogical success.

Carl

• Prev: teach untyped lambda calculus?
• Next: Reading seminar on semantics
• Index(es):
  • Main
  • Thread