Cw le denouement

By Scott

Another ‘type’ical Friday evening concluded our 3 part treatment of Cardelli & Wegner’s paper, “On Understanding Types, Data Abstraction, and Polymorphism.”

We will skip next week to observe Easter holiday and reconvene in 2 weeks, type inferences in hand to discuss “Basic Polymorphic Typechecking” by Cardelli. This will be Friday April 10th, 6:30 pm at Bento Miso.

In other news, we have a shiny new website thanks to Dann, http://compscicabal.github.io .

This week we had to cover a lot of material, section 5 to the end (!). We took several different approaches, section 5 is about introducing universal and existential quantification and putting them to use to develop a few simple modules and data structures in the Fun language. For future reference, this section is quite important and the Stack data structure example puts the ideas into clear view. Since they compare these approaches with Ada a language none of us are familiar with, instead we tried to contrast the approach taken in Fun to the approaches in languages we are familiar with, e.g. C++, Lisp, or Java. Thanks Peter, I really liked your discussion on Java types and how the extends keyword can look a lot like bounded existential quantification, very interesting.

Section 6 looked at subtypes, bounded quantification, and how the concepts of subtypes and variant types map into the “Ideal” model of types adopted in the paper. I’m glad we discussed this in more detail as there were several deeper ideas in how types related to each other that I definitely missed when reading it on my own. Section 7 was a first look into type inference and spurred some interesting discussion as well as building anticipation for the next paper on the block.

Section 8 we didn’t have much time for, but the chart mapping out the type system ecosystem is worth spending some time looking at, as there is a lot in there. And the final sentence or two of the paper are definitely worth reading too.

See you all in 2 weeks! Scott?