Types and Programming Languages Chapter 18 Case Study Imperative Objects
In this meeting, we discussed Chapter 18 of Types and Programming Languages: "Case Study: Imperative Objects".
Before the meeting, @tomstuart sent the following update to the club mailing list:
Until now we’ve been working with toy functional languages based on the lambda calculus, but now TAPL wants to show us how to build something that looks more like a real-world object-oriented programming language. Chapters 18 and 19 each approach that task separately, from different directions:
- Chapter 18: How can we use familiar language syntax & semantics to simulate the features of an OO language?
- Chapter 19: How can we use familiar ideas to design the syntax & semantics of an OO language from scratch?
So chapter 18 is about cobbling together OO features from more basic pieces we already have laying around: the simply typed lambda calculus plus records, references and subtyping. To do this we need to work out what “OO features” we want to cobble together, and then work out how to encode those features by using the simpler ones at our disposal. (Object Oriented Programming with Nothing???!‽) This is necessarily a bit clumsier than designing a more suitable language from scratch, but it has the significant benefit of not requiring any new formal work (e.g. no new typing or subtyping rules, no new safety proof) because we’re just reusing old parts rather than conjuring up new ones.
Pages 226 & 227 are pretty clear about what “OO features” we should care about:
- Multiple representations — different objects can implement the same method differently
- Encapsulation — an object’s internal representation can only be seen & used by its own methods
- Subtyping — we have some way of substituting one type of object for another when that’s safe
- Inheritance — we have some way of sharing behaviour between objects
- Open recursion — one method can call another method on the same object (i.e. self/this)
The basic encoding suggested by the chapter is an intuitive one: we can represent “objects” as records, where each label is a method name and each value is a function that implements that method. This dovetails nicely with our existing subtyping rules, because we’ve already built up a sensible system for when one record or function (or record of functions) is substitutable for another, so everything should just work as expected. The chapter also shows us how to use records of references for state, lexical scoping for encapsulation, and object-generating functions for inheritance (classes and subclasses).
Some of this is a bit fiddly, but it’s all “just programming” using the language features we’ve seen already — everything up to and including section 18.8 should be explicable given enough luck & concentration.
BEGIN TOTALLY IGNORABLE STUFF ABOUT OPEN RECURSION
The chapter does become what I would call Extremely Fiddly when dealing with open recursion in section 18.9 and onwards. This is bad news for us because it depends upon fix, which was covered in chapter 11 (section 11.11, “General Recursion”) but didn’t get much attention from us at the time.
To understand this chapter, all we really need to know about fix is its evaluation rule:
fix (λx.t) → [x ↦ fix (λx.t)] t
In English, that means that fix foo evaluates to the body of the function foo with all the occurrences of foo’s parameter replaced with fix foo.
For example, if you evaluate…
fix λfactorial. λn. if iszero n then 1 else n * factorial (pred n)
…then you get:
λn. if iszero n then 1 else n * (fix λfactorial. λn. if iszero n then 1 else n * factorial (pred n)) (pred n)
which is a function that does the “first step” of a factorial. When called with an argument, if the iszero n part evaluates to false then you end up evaluating the nested fix and the same expansion happens again, and so on until iszero n becomes true. The ultimate purpose of fix here is to allow the factorial function to refer to itself.
We need this incredible expanding behaviour in section 18.9 to allow an object to refer to itself so that it can call its own methods. If all the talk of fix and evaluation order becomes a little too mind-bending, peek into section 18.12 to see how we can achieve the same effect with mutable references instead. This is an idea that our conversations have touched on before (see page 516), but in a new setting.
We needn’t get too bogged down in open recursion if it’s too confusing — the other OO features are much simpler and are interesting enough in themselves. Maybe open recursion is only worth discussing during the meeting if we feel confident we understand the rest of the material?
END TOTALLY IGNORABLE STUFF ABOUT OPEN RECURSION
Happy reading. Looking forward to next week!
Thanks to @leocassarani and Geckoboard for hosting and providing refreshments, @tomstuart for shepherding the meeting, [@charlieegan3] for organising the meeting, @zetter for providing bread and @jcoglan for volunteering to host the next meeting.