Types and Programming Languages Chapter 19 Case Study Featherweight Java
So what was the point of this then?
Well, last time we built a tiny imperative objects system in the same typing system we already had, encoding what we wanted in the primitives already available to us.
Here, we're looking at an abridged Piercey-pierce paper doing much the same thing, but a bit differently.
Chris Z: plus some interesting discussion of the different tradeoffs in language design [notes: I missed the end of this]
Tom: it's interesting because of the contrast - all through the book we've had our heads up one particular [pause] I wanna say... butt? But this is the first chance we've had to look at a different approach.
Some of the things it highlights is that what we've been working with up to now isn't the only way of doing things. Although the operational semantics is still treated as a set of term rewriting but a bit more complicated.
Mudge: so last time, where we had problems with the [static late binding?] with the imperative objects, is that easier in this case because we've got more control?
Tom: Yes, cos we can write that directly into the evaluation rules, which we get to decide.
James: There's also some engineering practicality here, e.g. the ease of doing nominal subtyping, where at typecheck time you don't have to evaluate any complex rules, you just check a graph of names that fully defines your subtype relation.
What is FJ? Main takeaway is that it doesn't have assignment, so it's a functional subset of java. This provides a platform for experiments, e.g. adding generics - you can play around with them in this formal context and learn/prove things in a less complex setting (and indeed that happened! GJ is FJ + Generics, which ended up turning into the actual Java generics implementation. Pretty cool.)
It's still Turing complete though - you can encode the lambda calc in it. So there.
Constructors are completely constrained - you can only set the named fields, and the existence of them in FJ serves only to make it a subset of actual Java.
James C: Why is it important that this be a genuine subset of Java?
Tom: The book points out, there's no ML implementation - you can actually run these examples with Java. Maybe that's good?
Another consequence of a purely functional subset is that we can write the evaluation rules just with term rewriting; no complex modelling of heaps, say.
What does an FJ program look like, and how do we evaluate it? Well, it's:
- A list of class definitions
- A single expression, optionally referencing the above (well, presumably at least some of them)
Bit of discussion about:
new Pair(new A(), new B()).snd → new B()Aren't new A() and new B() evaluated? Well, here they kinda have been - this is the only way we have to represent "an instance of A". So while in Java this would be evaluable and result in some sort of IL representation of an A object, here we're just manipulating the text of the program. So we've kinda got to say "in Java, evaluating the LHS would result in a value that looks like the result of evaluating the RHS".
[we look at the next example for E-InvkNew, I am lost]
[we look at E-CastNew]
(Pair) new Pair(new A(), new B()) → new Pair(new A(), new B())So this is illustrating that if the RHS of a cast is a new instance, you can directly check that it's a subtype of the cast type - in this case it's equal, so we can just throw the cast away.
Here subtyping isn't a property of the class structure, it's explicitly declared in the code. Checking the subtype relation is just a lookup in a graph. There does need to be a mechanism to enforce that a declared subtype is a valid structural subtype, too, but you don't need to keep checking this - your compiler can check things like function type signatures and wotnot.
A purported advantage of nominal subtyping is that it prevents "Spurious Subsumption". Hmm.
Imagine in your program somewhere you come up with, say, a Money representation that looks like:
{ currency:String, amount:Integer }
And some other bit of modelling ends up with a structurally identical type representing a different sort of value - structural subtyping would allow one to be substituted for another, when maybe that's wrong. Nominal subtyping would give these different names, and they wouldn't be substitutable.
[INTERLUDE WHILE LEO REMOVES A CHILD'S SOCKS FROM THE LIGHT SENSORS]
Why is this "contentious", per Piercey-pierce? We don't know. Does anyone truly know the mind of Piercey-pierce? He refers to page 138, is this number reachable in a human lifespan?
[TOM TESTS THIS THEORY WITH SOME SCROLLING]
Okay, so we previously talked about variants, and he gave an example about single-variant types which basically lets you give a name to an otherwise structurally identical type.
Another advantage of nominal types is that it makes recursive types trivial, e.g. we can say things like
List ::= [] | Pair(H, List)
So yeah, the next chapter that we will NEVER READ is about introducing a new bit of type syntax that allows us to do this for structural types, c.f. the fix operator we had with recursive functions.
[Piercey-pierce grumbles about the purported engineering advantage of nominal subtypes - "well-engineered typecheckers" for structural systems reduce "most" subtype checks to a single comparison. Well then, that's us told.
Discussion is made of the handwavy bar syntax, which we think of as vector notation, so f[bar] = f1,...,fn and so forth. I don't know how to type an f with a bar on top of it.
Tom: there's no sequencing, notably. Functions are just returns (and per James C, the word return is redundant as a result, only there for Java compatibility).
In the subtyping relation, "CT" is just like a lookup table that lets you get the class definition of the argument.
A program is a pair
(CT, t)of a class table and a term.
So basically, a bunch of class definitions and a single expression. Like we said. Sheesh.
The class table has some properties:
- If you look up C, you get its definition (c'mon)
- Object is not in there, it's a magically-defined thing
- [I missed this bit]
- The relation has no cycles, i.e. is antisymmetric
We look at the definitions for:
- getting the fields of a class
- getting the type of a method
- getting the body of a method
- checking if overriding a method is permissible
We are, I think, collectively and unanimously disgusted.
e.g. why is fields(Object) = ·? Why not {}? Who knows. Disgusting.
Paul: Why are there multiple bees?
Us: Why indeed.
[Narrator: I'm not even going to attempt to transcribe this, I give up. I'm going back to my early career of football.]
James C: (capturing it perfectly) It's confusing because the same letter refers to different things. It's confusing because it implies those bees have to be the same but they don't.
[PAUL DOES SOME HEROIC WHITEBOARDING]
Rich: Clearly Bee Bar and Bee are two COMPLETELY different things
Tom: So in English, "To find out what the type of a method is within a class, you look at the definition of a class, and take [the types of all the args] → [the return type]"
Then there's another step that says "if your method isn't defined in the current class, look in the supertype".
Straightforward, and no-one got covered in bees.
[we skip over method body lookup]
[we look at the method overriding]
The rule seems to say we have to exactly match the method signature of the supertype.
Tuzz: Is that where casting comes in? Can we get that covariant / contravariant property back with explicit casts?
[some discussion of actual Java properties that I missed]
We gaze upon the evaluation rule schemas (schemæ?)
Tom: Does anyone care about these things?
The first three rules are all computation rules, i.e. are applied to values, in this case "new" instances. new is the only value in this system.
Notably the cast rule is just a check - you don't change the type of the thing, you just check that it's okay to treat it as the cast type, i.e. that your value is a subtype of the cast type.
All the other rules are congruence rules.
Apparently not a great many people care about these things.
Oh god.
T-Var - just like in the lambda calc. A Γ turns up unannounced, or barely so.
T-Field - meh
T-Invk - James C gives a majestic summation along the lines of, "if the receiver has some class type, you look up the method definition in that, find the parameter types, check that all your arguments are subtypes of the parameter types, and IF SO, the resulting type is the return type of the method"
Tom: Basically all of these rules are doing exactly what you'd expect, just hidden in a bunch of symbology
James C: Casting is the only thing that seems different here - everything else is largely what we've seen before
Tom: Pedantically, it's interesting to note: the syntax of types doesn't contain → here. We only have classes, and the → is just some notation that describes what our mtype helper returns, but that could just be a pair ([args], return). Every type here is an object.
There's also some different, uh, types of checking going on here. The above rules all describe whether some term t has type T in Γ. Other rules describe class typing, which determine if some class definition is "OK" in the sense that it's allowable, or that some method definition is "OK" (does it return the correct type? Is it an allowable override if it's overriding a superclass method?)
James C: What purpose does it serve here to have to state what you think the method returns, and then have that checked?
Tuzz: Is it a nominal vs structural thing?
Tom: The pragmatic answer is "cos that's how Java works", and Java doesn't have return type inference. You have to say what you think you're returning, and if you mess that up, it'll whinge at you.
James: Does it let you hide information? You can declare a less specific return type than you're actually returning, to prevent people relying on e.g. you returning a HashMap object instead of a Map
Tom: A way of thinking about it is that there's a mandatory cast at the end of every function
Object encodings: understand how encapsulation / reuse works under the hood, if you like.
Treating objects as primitives: lets us play around with their operational semantics directly, and experiment more easily with features on top of them, which is better for language design.
Yes. Inside TAPL there was a small book struggling to get out. And we have done it.
Whats-next then eh, not much chat. We need some reckons. Should we have a whats-next meeting? We've done that before.
Charlie's idea: rather than suggest books specifically, suggest areas of interest. You don't know what you don't know, so that's a way of maybe getting a broader pool of ideas.
Leo: Next meeting normally would be 21st of November - keep that in the calendar for the whats-next step?
Chris Z: Shall we start after Christmas?
General assent that interstitials until Jan is a good idea
Leo warns us that he has a recurring meeting some tuesdays these days. Tut tut etc.
[WE DECIDE TO DO A WHATS NEXT, um, NEXT]
Paul: Do we want to do like a mega-retro on TAPL? We did one after NTO.
[a minor TAPL retro ensues]
- Leo: we've done really well, tackled something waaay harder than before
- Paul: it's been great, but also has felt most like work at times, which has led to some low points and odd division of labour
- Tom: it's definitely the least "fun" book we've tackled this far
- Paul: the early implementation stuff was great fun and spawned some great tangential learning
- James / Tuzz: yeah, but the implementation stuff rather dried up
- Tom: I'd like to prioritise building stuff next, and will personally be evaluating ideas on that basis - how likely is it to generate messing-around implementations?
A few of us went to the nearby Singer Tavern after the meeting and found ourselves a quiet room to celebrate the end of TAPL. Among other things, we discussed:
- Whether Blade Runner 2049 is mince or not;
- Swatch Internet Time, Metric time and "we need to take back the Greenwich Means of production";
- Whether The Legend of Zelda: Breath of the Wild is a good video game for someone not comfortable with 3D platforming;
- What actually is the blockchain, Merkle trees and the horrifying details of Ethereum;
- AWS Lambda.
Thanks to @leocassarani and Geckoboard for hosting and providing refreshments, @tomstuart for shepherding the meeting, @jcoglan for organising the meeting, @jcoglan and @urbanautomaton for providing bread, @urbanautomaton for taking notes and doing this write-up and @tuzz for volunteering to organise the next meeting.