Bob in the Red Room

By Scott

Hi everyone! Lots of cabal activity this week, Tuesday night we had the pleasure of meeting the author of PFPL, Bob Harper himself as he kindly agreed to join us for dinner and drinks at the Red Room and on Friday we discussed chapter 28 of PFPL, our first foray into control flow and the analysis of control stacks.

On Friday we will meet as usual to discuss chapter 29 “Exceptions” at 6:30pm at Bento Miso. Also any and all self projects are welcome, so if you have some interesting things you would like to share, bring them! :)

Bob Harper was in Toronto this week for the Homotopy Type Theory Worksop at the Fields Institute which Ben and Dann also attended and so was available to meet with our small collective of CS enthusiasts as well as a some other workshop attendees. Apologies to those who couldn’t make it out, you were missed, but hopefully we asked some of the questions you would have. It was a pleasure to meet Bob, he was quite relaxed and friendly and didn’t see to mind that we asked the same question a few times :).

It was really interesting to hear some more perspective on some of the topics from PFPL. For instance he went over his thoughts on the “Boolean blindness” problem from PFPL 25, and explained how languages shouldn’t have this concept of a proposition testing for the class of something followed by different clauses, rather the better way to approach it is to think of them as sum types from the outset and your class selection as a case analysis. He said that when teaching, he has even tried having students use languages where there are no “if” statements at all, only case selection.

Another topic he brought up was the second order polymorphic lambda calculus and a result of Reynolds that “Polymorphism is not set-theoretic” which he considered one of the most beautiful results in CS. We’ve actually danced around some of the consequences of this result in chapter 17 when discussing representational independence. I found the Reynolds paper and you can take a look, https://hal.inria.fr/inria-00076261/document .

All for now, thanks Bob for coming to hang out with us, and thanks Dann for orchestrating things! Scott