We had an interesting meeting! We got through all the lecture slides, but didn’t get into the draft book material. We figured out a lot of things, but were left with some questions, which perhaps would be answered in the book.
Some things we couldn’t quite understand just from reading the slides:
- How exactly does the lambda calculus implementation of the Ackermann-Péter function work?
- We aren’t quite clear how the concepts of “introduction” and “elimination” apply with the typing rules for recursion and corecursion.
One additional thing I pointed out was that the functions ‘in’ and ‘out’ in recursion and corecursion do nothing - they are just there to make the typing rules work out. This is an example of isorecursive typing, as opposed to equirecursive, which wouldn’t have the ‘in’ and ‘out’ keywords. But isorecursive types are easier to implement in practice. Here’s a lecture about recursive types from Cornell: https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture27.pdf
I also explained the Haskell code that I wrote for last time, to implement Ed’s pairing operation for simply typed lambda calculus.
We decided to start working on the exercises for next time, but also go over the book material to see if we can answer some of our questions. Look for an announcement about the next meeting, on Dec. 11th.