Final Session of 2015

By Scott

Hey everyone! Hope you all had a great holidays and wish you a happy new year!

Back on December 18th we held our last session for the year, a festive one with oatmeal cookies, gluten free cheese filled monkey bread (thanks Leo!), brownies, some other tasty snacks and a yellow owl shaped fruit plate courtesy of the fine fruit slicers at Metro foods. We ate more than usual, reminisced on 2015, and discussed chapter 15 of PFPL, infinite types.

We will jump back in on Friday January 8th, 6:30pm at Bento Miso and bring a fresh 2016 perspective to bear on chapters 14 and 15 of PFPL. We have covered each already however the material seems to be important and worth further discussion.

Dann had the great idea to look back over our year and remember some of the things we did in 2015, hint it turns out a lot! Some favorites were the over ambitious weekly paper readings from earlier in the year, Strachey in 1 week, Array Mapped Tries, and the garbage collection paper came up. Chapter 9 of PFPL (Gödel’s system T) was also mentioned as well as a number of other things which I can’t remember at the moment but we definitely agreed were more confusing than they needed to be. Or alternatively if maximizing confusion was the author’s aim, then they achieved a stunning success.

As for the infinite types material I felt like I came away with a better grasp of how these finite types (i.e. product and sum), infinite types (I.e. inductive and coinductive ), and the languages introduced earlier in the book all fit together.

One question I came to the session with was what exactly is infinite about these types? The motivating examples are natural numbers and infinite sequences of naturals, but we had naturals earlier in the book in the E family of languages, so what is different now that we decide to class them as infinite types? The answer is that in the E languages we were piggybacking on the mathematical definition of natural numbers, but now the constructs in chapter 15 give you the power to define them without requiring recourse to an external definition of numbers. This is similar to Gödel’s T language from Chapter 9 where nats were defined in terms of the successor function.

This explains why the types in chapter 15 are called infinite but the product and sum types of chapters 10 and 11 are called finite types. The infinite refers to the infinity of natural numbers whose values can be captured by the inductive and coinductive type mechanisms. An infinite number of values cannot be expressed in terms of product or sum types since in those types the full set of possible index values must be known a priori.

All for now, looking forward to taking one more crack at these infinite types next week, see you all then, Scott