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:

let x=t1 in t2 = (λx:? . t2) t1

(Note that we don't know what the type of t1 and therefore x is here.)

Tom explained that this is different to the other derived forms we've seen due to this issue. We wondered whether we need to do two passes in order to expand this but Tom explained that we can think of this "desugaring" as another recursing into our type_of function which may, in turn, call our desugar and so on (like co-routines), e.g.

def type_of(term, context)
  case term
  when var then ...
  when let then type_of(desugar(...), context)
  ...
  end
end

def desugar(term, context)
  case term
  when Ascription then ...
  when Let(name, term, ...) then ... type_of(term) ... 
  end
end

We also discussed the introduction of the "wildcard" _ in abstractions to avoid variable naming woes (where _ not only means "some name not already defined" but also that it will not be used in the abstraction body).

Thanks

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.