Types and Programming Languages Chapter 11 Simple Extensions
We began the meeting as per tradition by admiring the variety of bread and dips provided by @urbanautomaton and @tomstuart and helping ourselves to beverages provided by @leocassarani.
We began by listing the various sections of the chapter as a lot of us has struggled to get through it all beforehand and discussed our plan of attack for the meeting:
- Should we steam ahead, attempting to tackle as much as possible?
- Should we pick a predefined endpoint (e.g. cover up to "Pairs") and aim only for that?
- Should we pick specific sections of interest?
We decided that, as each section built atop the last and each section introduced a valuable new concept, we should steam ahead but with the full expectation that we wouldn't finish the material in a single meeting and that we may need to carry over into a second one.
We began by breezing past "base types" and onto a discussion of the new Unit type and its use in the sequencing derived form t1; t2.
We discussed the expanded version of sequencing:
t1; t2 = (λx:Unit . t2) t1
And pondered why x had to be type Unit, e.g. what if t1 returned a Bool or Nat. We assured ourselves that this would count as a type error in this language as calculating a value and not using it is pointless (particularly as we don't yet have side-effects).
We then tackled type ascription and expressed it in terms of abstraction and application:
t1 as T = (λx:T . x) t1
Which we all thought was rather nifty.
We then moved onto let and explained what it does (e.g. similar to Clojure's let) and Leo derived some typing rules for it:
We then attempted to express let as a derived form and immediately ran into an issue:
Thanks to Leo and Geckoboard for hosting and buying drinks, to Simon and Tom for buying snacks, Chris for organising the meeting and Tom for leading the discussion.