Toronto-based reading group that meets weekly to read computer science books and papers.
Currently reading: The Little Typer
Greetings fellow Cabalers! Slightly late recap, but it being the most Victorian of weekends, perhaps I can be excused. Last week Ben gave us a first rate guided tour through Algorithm W and the proof of its soundness. And on Friday 6:30 pm @ Bento Miso we will continue on to the end of Milner’s paper!
Diverging from the usual recaps, I wanted to throw a few questions out to the group that take us back to the why of type theory. Maybe it’s just me, but I find I’ve lost perspective a bit on what we are learning about. Probably best to think a precocious kid asking his teacher, “why do I have to study this useless Math?! It’s not good for anything!” :). For math, I have lots of answers to that question, but I want to be able to answer that question for type theory too. Cardelli and Wegner’s introduction made a lot of sense to me, and to paraphrase them extremely liberally, “you can do computation in an untyped universe, but to do anything useful you have to impose some type of organization, so you may as well build your types rigorously.” Good, that seems reasonable enough, but after that my sense is that things diverge into several competing aims; some practical, some theoretical, and it becomes far less clear to me.
So I open it up to all of you,
Until next time, Scott?