Toronto-based reading group that meets weekly to read computer science books and papers.
Currently reading: The Little Typer
Hey Everyone, Smaller crowd on Friday as it seems with summer approaching many things are afoot, but that didn’t stop our intrepid group of 3 from pondering the eternal type theoretic question, “what would Philip Wadler do?” (WWWD). Next week is everyone else’s chance to ask WWWD, as we will continue reading his paper “Theorem’s for Free!” In our third and final instalment at the usual time and place Friday at 6:30pm at Bento Miso.
Bento Miso has been an incredible host for our meetings for more than a year. The community that Henry, Jennie, and Dann have created is vibrant, creative, and an important part of the Toronto art, video game, and development community. Bento Miso is a leading member of the Toronto Media Art Collective (TMAC) and I encourage you all to read about and support TMAC in their recent conflict with Urbancorp and the City of Toronto over a new nine million dollar facility. Both the city and the condo developer Urbancorp have reneged on a done deal at the eleventh hour, leaving TMAC out to dry.
WWWD? Fight til the last lambda has been applied!* TMAC is now pursuing legal and bureaucratic avenues to restore the agreement and can use our support, read more about it at http://tomediaarts.org/open-letter/ .
For the paper, we didn’t get too far, we went through 3.1 and 3.2 where he covers the proof of the first theorem he introduced at the start of the paper and the fold rearrangement theorem. We found we could follow the math, but we’re struggling to understand the full significance of the results and how they are used. Luckily Pete has already come to the rescue on slack :). Turns out it’s really important for performance optimization so hopefully he’ll be able to make it out Friday and share some of his stuff with us. We spent a lot of time working out on the white board the example in section 7 demonstrating why if you add a fixed point function to the language you can only use strict functions and almost succeeded in deriving it but got bogged down on evaluating the fixed point function composed with the identity function.
We also found ample divergence time and were talking about science fiction a bit more than usual which was highly enjoyable.
Until Friday, Scott