From Untyped to Simply Typed Lambda Calculus #10
Description
Proposal
type: long talk
audience: intermediate
category: pl theory
Summary
The Simply Typed Lambda Calculus adds function types (e.g. not:: Bool -> Bool) to the Untyped Lambda Calculus. It is the simplest example of a typed lambda calculus and can be used as a foundation for functional programming languages with simple type systems (i.e. without polymorphism, higher kinded types, dependent types...) You can also consider it as the next easy learning step into understanding more complex type systems.
Following the motto: "... there is nothing so practical as a good theory!" we'll combine theory and practice by writing an interpreter and a type checker, guided by their theoretical counterparts. These are Evaluation Rules for the interpreter and Typing Rules for the type checker.
To understand evaluation and typing rules we'll learn how to read Inference Rules in general. You can find this notation in many papers about type systems and operational semantics - so it's definitely worth learning.
Of course, we'll start with a quick recap / introduction to the Untyped Lambda Calculus.
Code examples will be in Haskell, but I promise to keep them as simple as possible - No fancy stuff... ;)
(Please note: I'm at the Haskell eXchange in London from 8th to 14th October, so I won't be able give this talk in that week...)