The First Practical Friday

By Scott

Hello fellow Cabalers and welcome to all new Recruits! Last Friday we kicked off the Cabal year with a bang and started Chapter 1 of The Practical Foundations of Programming! So exciting!

For those who couldn’t make it, this Friday, September 18th, 6:30pm at Bento Miso is still a great time to start, as we will blatantly ignore the advice of the bearers of the Holy Handgrenade and proceed directly unto Chapter 4. The reading for the week is sections 4.1 and 4.2 and and Pete has already started some notes to help us because he is awesome, here: Static and Dynamic and here: Type Judgements.

After a round of introductions, we started on the preface which in typical Harper style, is short but incredibly dense, and I suspect that other groups without as judicious wranglers as ours would never have escaped the preface. He asks some pretty fundamental questions about programming, e.g. what is a program made of? What structure does a program have? And though he wasn’t able to answer those questions, I think it will be good to keep those questions in the back of our minds even when wading through murkier waters.

In Chapter 1 of PFPL, Harper starts laying some mathematical ground work for what will follow, so we defined Abstract Syntax Trees, Sorts (Not to be confused with types!), and introduced a variety of notation for manipulating variables and trees. Pete’s and Ben’s explanations surrounding Sorts I found particularly helpful for my understanding, as while reading I had thought of them like types, but they are serving a different purpose here. I liked Pete’s analogy with English language, where the types of a typed programming language like Haskell correspond to the meanings of words, whereas Sorts correspond to the grammatical structure provided by a word. As example, “The dog chased Sally” works as a sentence, but not “The dog swam Sally”, as the verb swam requires a preposition “to” to have a full English sentence. A type error concerns meaning, so a sentence could be grammatically correct but make no sense, e.g. “The dog quoted Sally”, which makes sense if the dog happens to be Mister Peabody but otherwise is impossible.

Thanks to Dann and Bento Miso as always for doing a wonderful job, and see you all again soon, Scott