Lecture on Thursday 12:10 in SU1.
- We have prepared some lecture notes, mostly for the Hindley-Milner type system.
- Introduction to the lambda calculus
- Notes on ipmlementing lambda calculus
- An easy to read blog post about reduction strategies
- A concise way of performing substitution and beta-reduction in de Bruijn representation of lambda terms
- Article on combinatory logic containing the abstraction elimination technique discussed on the lecture (Combinatory calculi -> Completeness of the S-K basis)
- Haskell Platform
- ...
To complete the course, students need to pass the exam or write a program.
Exam will cover topics discussed during the semester, form of the exam (written or oral) will be determined at a later date.
The programming task involves creating a simple evaluator and a type inference engine for one of the lambda calculus variations discussed in lectures, further specifications will be given in the form of assignments during the semester.
-
Choose your favorite lambda term representation and define the appropriate data type for the representation. You can choose either:
- straightforward lambda terms representation
- lambda terms representation using De Bruijn indices
-
Implement substitution and beta-reduction. You have two options here:
- Implement substitution and beta-reduction directly for your representation of lambda terms.
- Or you can choose alternative (or bonus) approach: Avoid problems dealing with bound variables by using abstraction elimination to transform lambda terms to simpler combinator terms. See wikipedia article on combinatory logic containing description of the abstraction elimination technique discussed on the lecture (section Combinatory calculi -> Completeness of the S-K basis).
-
Implement the normal reduction strategy.
- Implement Hindley-Milner algorithm W (see the lecture notes for more information).