Paper! Understanding Types Cardelli and Wegner

Types!

A stackoverflow answer wherein Will Byrd talks about the differences between Prolog and Kanren (and logic/relational programming in general).

Friday March 6th Recap

The Pizza Theory of Types (?!)

Hey everyone, Friday night we kicked off polymorphic month by reading part 1 of Cardelli & Wegner's paper, "On Understanding Types, Data Abstraction, and Polymorphism".

Next Friday at 6:30pm at Bento Miso we will continue into sections 2 and beyond of the Cardelli & Wegner paper, so for those of you who missed the first part you should still be able to catch up and come join us.

The first section covers a lot of ground, providing the reasoning behind adding types to programming languages, introducing their definitions of the different types of polymorphism and spending a lot of time exploring the ideas through examples and anecdotes from other programming languages. The author's seem to have a nice sense of humour and I did wonder if maybe one of them had a teenager at the time as the motivation for adding types to the language, could be paraphrased as, "Well, if you're going to do it anyway, you may as well use protection", they even refer to types as armour which covers naked untyped representations.

During our discussion, Dann brought up the different types of pizza at Bucatoni's pizza in Brooklyn, and we decided that many of the operations normally involving pizza, e.g. Slicing, biting, or dipping are in fact polymorphic with respect to the toppings involved. However, I still thought a baked wheat crust was essential to its pizzaness. Little was I to know, that waiting at home was a sweet potatoe pizza! Showing that not only can the toppings be changed but also the main crust ingredient, boom mind blown! It turns out pizza is a purely abstract type.

Until next time Scott

---

Later...

  - Section 5 **Scott**
  - Section 6 **Dann**
  - Section 7 **Liav**
  - Section 8 **Scott**
  - Section 9 **Dann**

Friday Night Recap C&W Part 3 March 27

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