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 had 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).

We discussed pairs with their new type of T×T and then moved onto the more general concept of tuples (building on top of pairs to have more than two elements) and then records (building on top of tuples by attaching labels to each value). We noted how the specific construction of the evaluation rules actually enforce an evaluation order (e.g. in a pair, that the first term is evaluated to a value before the second and that projection forces evaluation because it is only defined on a pair of values, not terms).

We briefly touched on the notion of equivalence, e.g. is a record <alive=Bool, age=Nat> equivalent to <age=Nat, alive=Bool>? However, this requires subtyping and will be covered later in the book so we moved on.

We noted that projection in all of the above cases (e.g. t1.1 or t1.5 or t1.name) is defined as static and is not dynamic, that is the 1 in t1.1 is not some Nat term but part of the language itself.

We discussed whether we could define a function to do a sort of "dynamic projection" which led us neatly onto sums: a type that represents two different types:

Nat+Bool = a Nat or a Bool

We discussed how this necessitates the introduction of the new inl and inr operators which are used to both pattern match specific types out of a sum type with case and to introduce an instance of a sum type by populating a particular side (hence inl "in left" and inr "in right"):

inl 0 => Nat+Bool
inr false => Nat+Bool

case x of
  inl n => ...
| inr b => ...

We immediately wondered how we could infer which sum type a use of inl or inr would result in (e.g. what if your program has Nat+Bool and Bool+Bool, what type does inr zero have?) Feeling smug, we then realised this was the very next part of the chapter and that while we will revisit this later in the book, for now we can use ascription to state the type unambiguously:

inl 0 as Nat+Bool
inr false as Nat+Bool

Now armed with enough type knowledge, we wrote a project function which could dynamically give us a 0-indexed projection of a pair of type Nat×Bool:

let project = λp:Nat×Bool . λn:Nat . if iszero n then inl p.1 as Nat+Bool
                                     else inr p.2 as Nat+Bool

We were pretty pleased with the type of our project function:

Nat×Bool → Nat → Nat+Bool

With time running out, we discussed the concept of variants as an extension of sum types (not unlike how tuples generalised to records) and Tom laboured over a worked example on the whiteboard:

And with that, we were out of time with two sections left to go (General Recursion and Lists)!

Retrospective

• We were pleasantly surprised how much of the chapter we had covered given our concerns before the meeting that there was too much material to get through
• There was praise for how illuminating the meeting had been
• There was feeling that this was one of the most rewarding non-implementation meetings in the book so far with one attendee going so far as to say "it was f*cking great"
• We discussed what to do next meeting and decided to tackle the remaining two sections, mob implementations of choice types (e.g. pairs, sums, etc.) and potentially have time for another Show & Tell
• A few attendees are unavailable in two weeks so we decided to hold a poll to see whether we should postpone or arrange an interstitial meeting for next time.

Pub

In the pub, we discussed @jcoglan's Coping templating library as a good example of the value of single-field variants (e.g. simply communicating to the computer that a string is actually a URL allows us to make use of that typing information). @mudge blathered on a bit about the PHP microframework he wrote in order to write a simple wedding web site and @leocassarani regaled us with the time he received a literal treasure chest in the post from Codeship.

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.