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".

Table of contents

• Tom's update
• The chapter
• Retrospective
• Thanks

Tom's update

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!

The chapter

We began by going through Pierce's five defining features of object-oriented programming:

1. Multiple representations: effectively, polymorphism or the ability to call the same method on multiple values and get potentially different behaviour;
2. Encapsulation;
3. Subtyping: not necessarily sub-classing but more akin to Go's interfaces where objects of one class can be used where another might be expected;
4. Inheritance;
5. Open recursion: both the ability to refer to self (or this) and the late binding behaviour of that.

The chapter then proceeded to show us a case study of an implementation of the above features using only the functionality we've already seen in the book, such as records, references, abstractions and applications.

At their most basic, the chapter showed how we could model a Counter object as a record with methods as fields and a single piece of state encapsulated by lexical scope using let:

let x = ref 1 in
  {get = λ_:Unit. !x,
   inc = λ_:Unit. x := succ(!x)}

One quirk here is that our lambda abstractions always take a single argument so we have to use _ and Unit even though we ignore the argument in our methods. This means that calling methods also have to take an argument so we use unit:

c.inc unit

We briefly discussed having some syntactic sugar (e.g. empty parentheses, c.inc()) to hide this.

From there, we then saw an "object generator" which is effectively a factory/constructor for such objects:

newCounter =
  λ_:Unit. let x = ref 1 in
    {get = λ_:Unit. !x,
     inc = λ_:Unit. x := succ(!x)}

By using records as our representation of objects, we get quite a lot of functionality for free such as subtyping. Due to our existing record width subtyping rules, we can create a new object which has the same methods as our Counter as well as some new ones and use it wherever a Counter is expected:

newResetCounter =
  λ_:Unit. let x = ref 1 in
    {get = λ_:Unit. !x,
     inc = λ_:Unit. x := succ(!x),
     reset = λ_:Unit. x := 1}

Until now our objects have only had one piece of state (an internal number), what if we want to keep track of more than that? Why not use nifty records once more? Instead of having a single reference in lexical scope for use in our methods, we can have a record of references.

let r = {x=ref 1} in
  {get = λ_:Unit. !r.x,
   inc = λ_:Unit. r.x := succ(!r.x)}

We discussed whether we could use a reference to a record instead of a record of references but, as we have no way of updating a single field of a record, this would mean that subtypes of objects would need to know all fields in order to update any state.

While this is all well and good, we've really been copy and pasting methods between objects and subtypes: is there a way for us to introduce the concept of a class where objects re-use the same method definitions?

In order to do that, we need to separate the concept of methods from the internal object's state as until now we've been relying on lexical scope to encapsulate references. We can do this by taking the record of references we just introduced and making classes a function of this record (its "representation"):

CounterRep = {x: Ref Nat}

counterClass =
  λr:CounterRep.
    {get = λ_:Unit. !r.x,
     inc = λ_:Unit. r.x := succ(!r.x)}

We can update our object generator accordingly:

newCounter =
  λ_:Unit. let r = {x=ref 1} in
    counterClass r

This allows us to define subclasses without writing out each method definition again:

resetCounterClass =
  λr:CounterRep.
    let super = counterClass r in
      {get = super.get,
       inc = super.inc,
       reset = λ_:Unit. r.x := 1}

newResetCounter =
  λ_:Unit. let r = {x=ref 1} in
    resetCounterClass r

Note that we effectively create an object of the superclass with the same representation which we can refer to using super.

So we can inherit from a class and add methods but what about adding more state? Again, we benefit from using records for our "representations" so we can introduce a new representation with more fields and happily use that in existing object generator functions thanks to subtyping:

BackupCounterRep = {x: Ref Nat, b: Ref Nat}

backupCounterClass =
  λr:BackupCounterRep.
    let super = resetCounterClass r in
      {get = super.get,
       inc = super.inc,
       reset = λ_:Unit. r.x := !r.b,
       backup = λ_:Unit. r.b := !r.x}

Note that we're passing a BackupCounterRep to resetCounterClass which is expecting a CounterRep but our trusty record width subtyping rule makes this safe.

Our progress implementing OOP is looking pretty good: we've got multiple representations (multiple objects of different types can be used in place of one another), encapsulation (the state of an object is not accessible from the outside), subtyping (we can use a ResetCounter where we expect a Counter), inheritance (ResetCounter inherits from Counter) but no open recursion yet.

In order to do that, we must revisit something we'd conveniently skipped in earlier chapters: the fix operator.

@tomstuart led an explanation of what the fix operator does using the example of calculating factorials. In short, it allows us to define recursive functions in the lambda calculus: it is passed a generator and returns its fixed point. See also Tom's update for an explanation of this in more detail.

Some of us taking this somewhat on faith, we proceeded to see how we could use fix to introduce self in our objects:

setCounterClass =
  λr:CounterRep.
    fix
      (λself: SetCounter.
        {get = λ_:Unit. !(r.x),
         set = λi:Nat. r.x:=i,
         inc = λ_:Unit. self.set (succ (self.get unit))})

Retrospective

• There was some concern that we didn't spend enough time on the trickier latter section of the chapter (re open recursion) but also opinions that we did the right thing by focussing on the first sections and ensuring everyone understood the material;
• There was general consensus that everything from fix onwards was much more difficult and varying opinions about how important that was;
• We were reminded that this, unlike other chapters, is something of a "dead end" as it is a standalone case study: it isn't built upon in further material but is a single exploration;
• We decided that the next meeting will be about the second case study, "Featherweight Java", in chapter 19.

Thanks

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 organise the next meeting.