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,

• Why do you want to learn about type theory?
• Why is it interesting for you to study?
• What will knowing more about it let you do that you couldn’t do before?

Until next time, Scott?

Dearest Humans,

We had a perfectly lovely meeting this past Friday, full of tasty sandwiches, frothy beverages and even frothier musings as we stewed over a Greek alphabet soup of a proof. Questions were answered, confusionations were clarified (though a few were left dangling – how do we account for the lack of generics in Thm1.iv?), and we reveled in the joys of structural induction as a group for the first time. There was frantic scribbling in notebooks, hasty flipping back and forth through the paper to verify claims, deep discussion on impossibly tiny but incredibly crucial minutia, and an awful lot of pensive staring into middle distance: in short, we did math.

Thanks again to Pete for leading us from the dark and foreboding woods into the light of understanding. This week Ben has stepped up to the challenge of guiding our minds through Algorithm W and on to the proof of its soundness. We’ll forge as far into section 4 as we are able this week, finish the paper off next week, take a week off and then launch into typed meta-programming like an unstoppable force meeting a slightly-less-than-unmovable object.

As a side benefit of diving deep into the proof of the Semantic Soundness Theorem, the challenge to implement Algorithm W – or a suitable interpreter for the language it is described in – is still open, so dust off your space cadet keyboard and get ready to hit a few six key chord combos.

Love and Lambdas Dann?

Hey everyone, Thanks for what was for me at least a quite enlightening discussion on Friday, Pete continued guiding the reins of our exploration of Milner’s type theory paper. I very much appreciated the extended recap discussion of sections 3.2 and 3.3, as I had missed the previous week’s meeting, and in my own reading I definitely missed a number of important concepts, so thanks all of you!

Next Friday we will meet at Sud Forno at 6:30pm and try to get through the rest of the paper, section 3.7 and onwards. This will cover Milner’s Algorithm W which Ben has graciously challenged us all to implement, and to this end Pete has provided a text summary of the algorithm, https://github.com/pbevin/milner-type-poly/blob/master/algw.txt .

Section 3.4 and 3.5 that we discussed on Friday stepped us out of the semantic equation realm of section 3.1 and introduced the definitions for a system of types and a system of rules on how to use those types. Though all of the rules are defined quite clearly, for a neophyte some of the consequences of them are not immediately obvious. Though Milner develops many of these ideas with examples, having a group to discuss them with seemed quite valuable here. For instance, the differences between how lambdas and fix statements are typed and how let statements are typed is of profound importance, and we spent quite a bit of time discussing the implications of typing these statements on some examples that might run into problems if they were typed differently.

Throughout the discussion Friday having access to the Haskell version of the rules that Pete has developed was invaluable, https://github.com/pbevin/milner-type-poly/tree/master/src and now I notice that Pete has already started taking up Bens Algorithm W challenge, go Pete!

I feel very much like I am still trying to digest this material, I think I have taken a few bites but the chunks of knowledge are still floating around and need time to settle in. For instance, something I missed completely in my own reading was that what Milner identifies as Semantic equations over domains in section 3.1 are an entirely different concept than types and type relations, though they look similar at the surface level. This I find difficult as it is hard to even talk about the relations without calling things types or having types, but in the semantic realm we don’t have types, just domains. I still don’t quite understand what this semantic theory gives us and why we couldn’t start talking about types right away

All for now, See you all Friday! Scott?

Happy Monday, Computer Scientist!

We had a great meeting last Friday, with Pete leading the charge on unpacking Milner’s Exp language’s semantics, its types, and their semantics (Sections 3.1 and 3.4 of A Theory of Type Polymorphism in Programming). We came to an understanding of Milner’s syntax for this language and metalanguage*. We saw a roadmap for the paper, learned about lattices and complete partial orders, neatly skirted the topics of domain theory and retracts (though we may return to those later), talked about the type of wrong and the wrongness of types and how well-typed programs never go wrong, unless they fall in with a bad crowd and take up smoking and jitterbugging.

For this coming Friday we’ll be reading sections 3.5, 3.6, and 3.7. It’s not a lot of material, but it’s quite dense. 3.5 covers the connection between expression in the Exp language from 3.1 and expression in the type language of 3.4. Section 3.6 is about substitutions, which are kind of the type language equivalent of lambda calculus reductions (or not). Then 3.7 is a formal proof that Well-Typed Expressions in this language Do Not Go Wrong. We’ll dive as deep as we can in to the proof, but with an eye for coming away with an understanding of formal proofs in general and inductive proofs in particular, choosing breadth over depth if time gets short.

We’re wading in to some heady waters, but like Dante’s Virgil we have some excellent guides and guideposts along the way. Be sure to check out Pete’s study notes as you make your way through this week’s sections.

Have an amazing week!

Dann

• Perhaps a begrudging understanding, in that latter case*.
• Begrudging for me, at least*.
• Okay, fine, I still don’t understand. The syntax appears intentionally obfuscatory and makes me act completely irrationally. Sorry, I get a little verklempt just thinking of it.

Hey Everyone! Friday night we covered the first two sections of Milner’s famous paper, “A Theory of Type Polymorphism in Programming”, the conversational sections.

Next week we will continue on, I don’t think we picked a specific stopping point, as far as you can get is good. We will meet at the same time and place, Friday night at 6:30pm at Bento Miso.

Pete has taken the lead on this paper and I encourage everyone to check out his summary notes on github, https://github.com/CompSciCabal/SMRTYPRTY/wiki/Paper!-Milner-Type-Polymorphism . He does a great job at summarizing the main ideas in the paper so far. It seems like this paper formulates some of the ideas like soundness and completeness in a more clear way than we have seen before in our other readings.

Looking forward to seeing you all on Friday, Scott?

Thanks everyone for a great session on Friday!

Leo expertly wrangled us through Cardelli’s “Basic Polymorphic Typechecking” paper. Then for show-and-tell Pete showed us his type inferencer in Haskell (This was awesome Pete!) and Dann gave a super fast intro to the typed forth environment he was working on.

Next week, Friday April 17th, 6:30 pm @ Bento Miso we will be discussing the first 2 sections of Milner’s paper, “A Theory of Type Polymorphism in Programming”.

Lots of interesting conversation, for instance the sentence, “so does type have type type”, merited significant debate, and I still feel the full implications of it haven’t fully sunk in for me. Thankfully, out of context it sounds ridicululous so no will be paying attention anyway. Leo’s notes are available on the github repo to help anyone else interpret the paper, https://github.com/CompSciCabal/SMRTYPRTY/blob/master/papers/cardelli–basic-polymorphic-typechecking.md .

I really appreciated Pete taking us for a tour through his nifty Haskell implementation of the type inferencer based on the Modula 2 code from the paper (https://github.com/pbevin/cardelli), I found it really helped me understand some of the aspects of the unification and inference algorithm they discuss in the paper.

See you all next week, 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?

Friday night marked the latest installment of Cardelli and Wegner’s paper, “On Understanding Types, Data Abstraction, and Polymorphism.”

Next week will be the 4th and final chapter of Cardelli and Wegner, taking place in the usual time and place, Friday night at 6:30pm at Bento Miso.

This week covered type classification, and Universal and Existential quantification, sections 3, 4, and the start of 5. They describe their approach to types quite succinctly in the title of section 3, “Types are sets of values.” In that context, the programmer or language designer then has the task of identifying which out of the infinite sets available are interesting to use, and what subset relations to make use of. An advantage of this approach is that monomorphic, polymorphic, or untyped languages may all be described using the same type model.

Universal and existential quantification, I’m having a harder time wrapping my head around, but I am beginning to suspect that associating universal quantification with parametric polymorphism and existential quantification with abstract interfaces and information hiding is the short form description in terms I’m more comfortable with. Seeing how they are able to use type quantification to build the other more complex concepts into their system is a continuous and surprising journey. I’m finding it fascinating to see them build up their fun language, often as a programmer you are simply handed a language to use fully formed and you have to adjust to the language’s idiosyncrasies without really understanding what constraints went into the choices of designing that language. Here the language is as simple as possible and all of the additional concepts and ideas are being layered on top without additional language constructs being introduced.

Looking forward to next week where we will try to cover the rest of the paper! Scott?

Hey Everyone, Thanks for the interesting discussion of section 2 of Cardelli & Wegner’s paper, “On Understanding Types, Data Abstraction, and Polymorphism.”

Next week we will continue on to sections 3, 4, and 5 of Cardelli & Wegner, meeting 6:30 pm Friday at Bento Miso.

Section 2 of Cardelli & Wegner introduces their augmented typed lambda calculus, ‘Fun’, so named as in their words, “We christen this language Fun because fun instead of Lambda is the functional abstraction keyword and because it is a pleasure to deal with.” On first reading it seems a straightforward exposition of their language, however during the course of the evening we found numerous subtleties hidden just beneath the surface. Thanks to Dann and other’s probing questions and Ben’s knowledge of the subject matter, I think we all gained a deeper understanding of ‘Fun’, then we would have by just reading it on our own. What surprise! I always thought quiet solitary study would be the surest path to Fun.

See you all next week! Scott?

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 authors 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 Lucalli’s pizza in Brooklyn (Luca + Cardelli -> Lucalli), 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?