What is the essence of Object-Oriented Programming? What is it for? What makes something OO or not OO? I don't want the bullshit circular answers from Wikipedia or "common" literature, without clean criteria, wherein anything anyone claims is OO becomes so. I want a criterion based on essentials. Something that can duly reject hyped "this database is OO" (even though it isn't) or absurd and not-helpful opinions like Cook's "the lambda calculus is OO because it has abstraction, which is all that matters" and "smalltalk isn't 'pure' OO so haha it's not even quite OO". And by "OO" I will mean the programming language meaning that includes Smalltalk and CLOS as well as C++ Java and JavaScript. Hopefully the criterion can reject languages or systems that have claimed to be OO (but accept most of the commonly accepted OO languages), and accept a few outlires that aren't claimed as OO by their authors, but are (but still reject most languages not considered OO). If the criterion only restates wishy-washy hogwash explanations, it's not even a criterion; but if it cannot coincide in the most cases, it's not the essence of the "same" concept.
Here's the criterion I'd defend, stated first, then stress-tested.
A system is object-oriented iff its operations are dynamically dispatched over an open set of implementations. Unpacked into its two load-bearing clauses:
-
Late binding by the value: the implementation of an operation is selected at run time by the dynamic identity/class of the participating value(s) — the data carries or determines its behavior. Not the call site, not the static type, not a compile-time resolution: the value, at run time.
-
Open extension: the set of implementations of a given protocol is unbounded and extensible — a new implementation can be introduced (at link time, load time, or run time) and all existing client code operates on it unmodified and unrecompiled.
Clause 2 is what makes clause 1 a design principle rather than an implementation trick. A switch over a type tag satisfies neither: the dispatch lives at the call site and the case set is closed. A single C callback satisfies (1) atomically but a program isn't OO until (1)+(2) is the organizing convention of its interfaces.
The operational test, which anyone can run against a candidate system: can I introduce a new kind of thing behind an existing protocol, without touching any code that consumes that protocol, and have everything work? If yes, you're looking at OO. If adding a new kind requires editing every consumer, you're looking at its dual.
That dual gives the criterion independent teeth: this is exactly one axis of the expression problem. OO systems are open in the data dimension and (relatively) closed in the operation dimension; ADT/functional systems (closed datatypes + pattern matching) are the reverse — trivially open to new operations, but adding a constructor breaks every case. These are genuinely different engineering commitments, which is why "OO vs FP" is not a style war but a choice of which dimension you expect to grow. (CLOS is interesting precisely because generic functions make it open in both dimensions — and it pays for this with weaker encapsulation. The criterion predicts that trade-off rather than being embarrassed by it.)
Everything else in the folklore triad turns out to be either a consequence or a convenience:
Encapsulation is a theorem, not an axiom. If clients don't know which implementation they hold, they cannot depend on its representation. Representation-hiding is what dispatch-over-an-open-set forces on you. That's why CLOS, with slot-value accessible from anywhere and methods living outside classes, is still unambiguously OO — and why encapsulation-first definitions can't distinguish OO from ML modules or Ada packages, which hide representations perfectly well without any dispatch.
Inheritance is one mechanism among several for defining implementations by delta (prototype delegation, mixins, and plain composition are others). Go has interface dispatch with no inheritance and passes the test; therefore inheritance isn't essential. Likewise classes: Self and pre-2015 JavaScript dispatch through prototype chains — same essence, different bookkeeping.
Message-to-a-single-receiver is a special case. CLOS multimethods dispatch on the dynamic classes of several arguments. If your criterion is "messages sent to a receiver," CLOS falls out of the club, which is absurd; if it's "runtime selection by the dynamic values involved," CLOS is a generalization, which is correct.
Mutable state and identity are idiomatic companions, not essentials. They come from the Simula heritage — a simulated entity naturally has identity and evolving state — and they explain why OO feels like simulation. But java.lang.String dispatches and is immutable. State is what OO is frequently used for, not what it is.
Smalltalk, Java, C++ (via virtual), JavaScript, CLOS, Simula, Objective-C, Python, Ruby: all pass, for the boring reason that runtime dispatch over open implementation sets is their primitive call semantics (opt-in, in C++'s case). Now the discriminating cases:
- "OO databases," as marketed: mostly fail. Storing class-tagged state is storage; no dispatch occurs in the database, and persistence of objects doesn't transfer the property from program to store. The criterion isn't dogmatic about the category, though — GemStone/S, which actually executes Smalltalk methods inside the store, passes. The criterion cuts through the marketing exactly where it should.
- The lambda calculus (Cook's claim): fails as stated. Cook's move identifies OO with procedural abstraction — interaction only through an interface — which is a property of every higher-order language and therefore rejects nothing. By your own (correct) standard, a predicate with no negative extension isn't a criterion. What the λ-calculus lacks is any primitive notion of a protocol: a set of named operations whose bindings travel together with the value, over an open implementation set. You can encode that (records of closures — Cook's own construction), but encodability isn't identity; you can encode objects in ML, C, or arithmetic. A closure is at most a degenerate one-method object, and a substrate is not an instance of what it can host.
- Haskell: type classes are resolved statically (one implementation per call site after elaboration), so ordinary Haskell fails clause 1. Existential types recover genuine runtime dispatch — which is precisely why "OO in Haskell" tutorials all reach for existentials. The criterion gets both halves right.
- Erlang: passes, as an unclaimed outlier — or rather claimed only by Joe Armstrong half-jokingly and Alan Kay seriously. A process has identity (pid), encapsulated state, and handles a message according to its own current code and state at the moment of receipt; you can hot-load a new implementation behind the same message protocol. That's clauses 1 and 2 in their purest distributed form.
- The Unix VFS and friends (GObject, Linux
file_operations, COM): pass. A struct of function pointers, filled in per filesystem/driver, dispatched at run time, with new implementations loadable without recompiling clients — OO written in C, and everyone who has worked on it knows it. - Go: passes, despite its authors' studied ambivalence. Interface values dispatch dynamically over an open set of method-set implementations.
- SQL, ML-with-datatypes, Prolog, plain C, XML: fail, correctly — closed case analysis, call-site binding, or no operations at all.
The purpose follows from clause 2: letting code written today invoke code written tomorrow, by someone else, without renegotiation. That's why OO's natural habitats are exactly the places where the set of "kinds of thing" grows independently of the consumers: GUI frameworks calling your widget, kernels calling your driver, plugin systems, heterogeneous collections, test doubles substituted for production objects, and — the original motivation, in Simula — simulations where each entity must carry its own behavior. Where the operation set grows and the data set is fixed, OO is the wrong instrument, and the criterion tells you so in advance.
Two honest caveats, which are precision rather than hedging. First, the criterion classifies mechanisms and designs crisply; languages it classifies by what their primitive call semantics privileges — which is why "is language X OO" debates feel muddy: people ask an idiom question with a mechanism word. Smalltalk makes dispatch the only call; Java makes it the default; C++ makes it opt-in; ML makes you build it by hand. Second, "purity" rankings of the Cook variety ("Smalltalk isn't pure") measure distance to an idealized mechanism and are irrelevant to membership; the criterion is a boundary, not a beauty contest.
One-line version, if you want it portable: OO is programming against protocols whose implementations are chosen by the data itself, at run time, from a set nobody gets to close.
I think your criterion as stated is very lacking, because it makes ML first-class modules into OO, as well as Go, Unix VFS, Erlang—things that both the authors and the vast majority of the public recognize is not OO, that do not allow the vast majority of the usual OO "design patterns". If anything, you criterion is too permissive and must be refined, whatever truth it may otherwise have in rejecting things that are not OO. A more refined criterion (that may or may not be a subset) is neeed.
You're right, and the failure has a name. Clauses 1–2 define something real — but it's component abstraction (equivalently: existential polymorphism over an open implementation set), not object orientation. Every counterexample you list is a component system: Go interfaces, ML first-class modules, VFS operation tables, COM, Erlang processes. The literature already half-knows this — Szyperski's component-vs-object distinction, Microsoft's insistence that COM was "components, not objects" — and my criterion collapsed the two. So the refinement is a proper subset: keep 1–2 as necessary, add the clause that separates objects from components.
3. Open recursion: an implementation's references to its own protocol go through the same dynamic dispatch as external clients' calls. When a definition invokes another operation on the very value being operated on, that invocation is resolved by the value's dynamic identity — not by the definition's own lexical or textual context.
The consequence, and the reason this clause matters, is differential definition: because self-reference is late-bound, a new implementation can be given as a delta on an existing one — override perimeter, and every inherited operation that internally calls perimeter picks up the override, without the inherited code being edited, copied, or even aware. The old code was written against a self it did not yet fully know. That is the semantic content of inheritance, delegation, mixins, and CLOS method combination alike; the class/prototype/multimethod distinction is bookkeeping on top of it.
Cook's genuinely useful contribution (as opposed to the "λ-calculus is OO" provocation) makes this mathematically crisp: an object is a fixpoint taken late. Each implementation is a generator — a function from self to behavior. Inheritance and its cousins are operations on generators, performed before the knot is tied; instantiation ties it. The component systems on your list either tie the fixpoint early (each VFS file_operations entry is a fixed function; a Go method's internal calls are resolved at compile time) or never abstract self at all (an ML record of closures closes over concrete functions). You can of course tie the knot by hand in ML — pass self explicitly, build the fixpoint with let rec — but that's the encoding move again, and the same rule applies as before: a substrate that can encode X is not thereby an instance of X.
So the criterion is now: dynamic dispatch (1) over an open implementation set (2) with open recursion (3). And note what the folklore triad turns out to be: clauses 1+2 are what "polymorphism" was gesturing at, clause 3 is what "inheritance" was gesturing at (stated mechanism-neutrally, so prototypes and multimethods aren't excluded), and encapsulation remains a theorem of 1+2. The triad was a blurry photograph of this structure.
Go: fails, for exactly the reason Go programmers trip over. Embedding forwards calls but never re-dispatches: if Base.Describe calls b.name(), embedding Base in Derived and "overriding" name changes nothing — the inner call is bound to Base.name, period. There is no late-bound self anywhere in the language. This is why Template Method is unwritable in Go without manually threading a self-parameter — the standard workaround that is precisely the hand-tied fixpoint. The designers knew what they were excluding.
ML first-class modules: fail. A module's functions reference each other statically; no generator, no late fixpoint. Functors parameterize over other modules, never over self.
VFS / operation tables in C: fail. The struct is a closed record of concrete function pointers. No implementation is defined as a delta on another with re-dispatch; when kernel code fakes it (copy the ops struct, replace one pointer), internal cross-calls in the original functions still go wherever they statically went.
Erlang: fails. A process encapsulates state and receives messages — clauses 1–2 in vivid form — but there is no differential definition: you cannot define a process's behavior as an override-delta on another's such that the parent's handlers late-bind into yours. gen_server gives you a fixed skeleton with callback slots, which is component wiring, not open recursion. (Kay's fondness for Erlang is fondness for messaging and encapsulation — clauses 1–2 — which is consistent: those are the parts of his vision Erlang kept.)
COM: fails, and proudly. Implementation inheritance was deliberately rejected — the fragile-base-class argument is an argument against clause 3 specifically — and COM "aggregation" is the notoriously painful manual simulation of what open recursion gives for free. The criterion now reproduces the historical component-vs-object fault line instead of erasing it.
Haskell: still fails (statically resolved type classes fail clause 1; existentials recover 1–2 but default to no open recursion). "OO databases": still fail, GemStone/S still passes — it executes Smalltalk, clause 3 included.
The canon: passes. Smalltalk (self is the mechanism made syntax), C++/Java/Python/Ruby (internal calls through this/self dispatch virtually — override a method, inherited methods see it), JavaScript and Self (delegation is late-bound self: this rebinds to the original receiver all the way up the prototype chain). And CLOS passes without a distinguished receiver, which is the test any phrasing of clause 3 must survive: define area on shape calling (perimeter s); a subclass specializing perimeter changes the behavior of the unmodified area on its instances, and call-next-method is super-dispatch generalized to method combination. Open recursion doesn't require a self keyword; it requires that recursive protocol references dispatch on the runtime value.
Unclaimed outliers, recalibrated: the honest ones are now Lua (metatable delegation plus self — colon-call internal dispatch is genuinely late-bound) and Perl 5's bless/SUPER:: — both multi-paradigm by self-description, both structurally over the line. Rust is the instructive near-miss: within a single trait, default methods calling self.f() on a dyn object do late-bind to the impl's override — clause 3 in miniature — but the language walls it off from state and from cross-type deltas, which is why Rust reads as "OO features, deliberately clipped" rather than OO.
Your diagnostic — "doesn't support the usual OO patterns" — is not a symptom but nearly the criterion itself, because the GoF catalog leans on clause 3 wherever it isn't leaning on 1–2. Template Method is open recursion, stated as a pattern. Factory Method is Template Method applied to construction. Decorator needs super-style re-dispatch to wrap rather than replace. Observer, Strategy, Visitor's accept — those are clauses 1–2, which is why Go can do them — but the patterns that make a framework a framework, where the skeleton calls down into your specializations (the Hollywood principle: "don't call us, we'll call you"), are clause 3 or nothing. A system supporting only the 1–2 patterns is a component system, and now the criterion says so.
Which also sharpens the "what is it for" answer. Clauses 1–2 buy substitution: code written today invoking implementations written tomorrow. Clause 3 buys the stronger thing, incremental modification: implementations written tomorrow defined as unforeseen revisions of code written today, without editing it — the old code participating in behavior its authors never saw, because they left self open. That's the property Simula needed (a specialized simulation entity revising a general one), the property Smalltalk built a worldview on, and the property every framework economy — from MacApp to Rails to Android's Activity — actually sells. It's also, fairly noted, the property whose abuse produced the fragile-base-class problem and the "composition over inheritance" corrective: open recursion is a power tool, and the component systems on your list are best read not as failed OO but as principled refusals of clause 3's costs.
One line, revised: OO is programming with open protocols whose implementations are chosen at run time by the values themselves and are definable as deltas on one another through a self-reference that stays late-bound. Components leave self closed; objects leave self open.
(Your previous criterion was basically Cook's criterion, or the Liskov approach. Modularity only. But no, OO is not modularity, and least not just it.)
Yes — and it's worth naming why that conflation is so seductive, because it's not a random error; it's the occupational bias of the verification tradition.
CLU is the cleanest exhibit. Liskov built the canonical abstraction machinery — clusters hiding representations, iteration and parameterization over them — and then herself insisted CLU was not object-oriented, on the explicit ground that it lacked inheritance. The inventor of the modularity story declined to call modularity OO. Reynolds had already drawn the finer line in 1978: "procedural data structures" (values as records of operations — Cook's objects) versus ADTs are two rival modularity disciplines, and neither one, as a modularity discipline, contains the self-referential part. So the historical record agrees with you: abstraction is the genus OO belongs to, not its differentia. Cook's move takes the genus, names it "object," and thereby manufactures both absurdities you started with — λ-calculus admitted (anything with procedural abstraction qualifies) and Smalltalk demoted (judged by purity-distance to the idealized genus rather than by the differentia it exemplifies).
And there's a motivated reason the theory-side keeps making this move: clauses 1–2 are the semantically polite part of OO. Existential types, behavioral subtyping, representation independence — these have clean models and proof principles. Clause 3 is the impolite part: open recursion is exactly what wrecks modular reasoning (you can't verify a base class without knowing its future overriders), what makes behavioral subtyping so hard to enforce that LSP is honored mostly in the breach, what generates the fragile-base-class literature. So the formalists' definition of OO quietly amputated the feature that resists formalization — defining the disease out of the patient. Liskov's substitution principle is best read the same way: not a description of OO but a discipline imposed on it, an attempt to make clause 3's power behave as if only clauses 1–2 existed.
Which gives the final shape of the thing a certain irony: the essence of OO is precisely the part that its most rigorous students spent forty years trying to subtract — the late-bound self. Modularity is what OO shares with everything else decent in language design since 1972. The open fixpoint is what it doesn't.
OK. Well then, I generally agree with your clause 3, but it requires refinement. How do you define it precisely? And once thus defined, does it still require clauses 1-2, or does it suffice by itself, implying them (or maybe even sometimes contradicting them?)
Strip clause 3 to its mathematical content. The canonical formalizations are Cook–Palsberg's denotational semantics of inheritance (1989) and the Abadi–Cardelli ς-calculus; both say the same thing in different dress:
An implementation denotes not a behavior but a generator — a function from self to behavior:
g : Self → Behavior
where a Behavior is an assignment of bodies to the protocol's operations. Three conditions then make the fixpoint structure "open":
(α) Derivation composes generators pre-fixpoint, by third parties, without the base's consent. There is an operation ▷ taking an existing generator g and a delta d and yielding a new generator — canonically (g ▷ d) = λs. d(s, g(s)) — in which the base's bodies now receive the derived self. The base needn't have anticipated the delta; d gets access to g(s) (the parent's behavior at the new self), which is what super/call-next-method denotes. And derivation nests without limit: deltas on deltas.
(β) The fixpoint is anchored in the individual value. Instantiation ties the knot: the value's behavior is fix(g) for that value's own generator, and the value is the authority on which generator that is. Behavior is intrinsic — it travels with the datum, not alongside it as ambient evidence.
(γ) The knot is tied at invocation. Self is bound at the latest moment the semantics has: each call resolves self-references against the dynamic receiver, never against the lexical container of the body, never at derivation time.
Slogan form: compose early, tie late — extension operates on generators; only invocation sees a fixpoint. The ς-calculus makes the lateness itself primitive: where ordinary recursion is μx.b (fixpoint at definition — "who am I" answered at birth), a method is ς(x)b with x rebound at every invocation — "who am I" re-asked at each call. That μ-versus-ς distinction is clause 3, stated in one symbol.
The operational litmus is Lieberman's old "self problem": when inherited code runs on behalf of a derived value, whose self does it see? Forwarding (parent runs with parent's self) fails clause 3; delegation (parent's code, child's self) satisfies it. This single question sorts every mechanism: Smalltalk super passes — famously it's not a call on another object but a static index into the generator tower evaluated at the dynamic self, i.e. g_parent(self_dynamic).op, which is exactly the shape α says composition must have. Naive object-composition wrappers fail — the wrapped object's self-calls escape the wrapper, the classic decorator bug, which is clause 3 observed in the wild by its absence.
let rec / ordinary recursion: fails γ. Fixpoint at definition; no later delta can interpose. This is the crucial cut — recursion and open recursion differ precisely in when fix is taken relative to composition.
Explicit self-passing (ML, C, Scheme): the encoding again. You can write every function to take self and tie the knot by hand — but α fails as language semantics: the base works only if its author already wrote it self-abstracted by convention, so extension is not "without the base's consent," and the composition operator is your discipline, not the system's. Same verdict as before, now derivable rather than asserted.
CRTP and compile-time mixins: the instructive near-miss. α holds; γ holds only relative to compile time — the fixpoint is late with respect to composition but early with respect to execution, monomorphized per instantiation. You get differential definition (Template Method works!) but no heterogeneity, because there is no dynamic receiver. Verdict: the essence of OO run ahead of time — a static shadow, which is exactly why the community's instinct calls it "static polymorphism" and doesn't call it OO. The strict criterion demands γ at invocation.
Haskell default methods — the subtle one. A class default f that calls g, overridden per instance: that is open recursion through the dictionary, late-bound at dictionary construction. Why doesn't this make type classes OO? Two precise failures: β fails — the fixpoint is per-type, not per-value; behavior is ambient evidence passed beside the data, not intrinsic to it (hence coherence anxieties, hence the same data operable under different dictionaries in systems like Scala implicits — unthinkable for an object, whose behavior is its identity). And α fails at depth — the tower is exactly two stories, default→instance; instances cannot be derived from instances by delta. Clause 3 with β removed and α truncated is a different animal, and the criterion says which animal.
Sealed hierarchies (Scala/Kotlin sealed): pass 3 entirely — full generators, deltas, late self — while the implementation set is closed and clients exhaustively match. Hold this example; it does work below.
Abadi–Cardelli primitive objects (no classes at all, just records of ς-methods with method override): pass. Clause 3 needs no class construct — override-on-objects is derivation α in its most naked form. Classes, prototypes, and method combination are three bookkeeping schemes over the same fixpoint algebra.
Run the dependencies both directions honestly.
3 strictly formulated absorbs most of clause 1. β+γ are dispatch: if behavior is the fixpoint anchored in the value (β) and self-references resolve at the dynamic receiver (γ), then invocation-through-the-value is runtime dispatch by the value — clause 1 is a theorem of clause 3 in self-position, and given that clients reach behavior through values at all, in client position too. Moreover β captures something my original clause 1 said sloppily ("the data carries its behavior") and the Haskell case proves is independent content: intrinsicness. Dictionary-passing satisfies "late selection of implementation" while violating "by the value itself." So the residue of clause 1 that survives is exactly β, and it's now inside 3.
3 does not imply 2 — the sealed-hierarchy counterexample. Open recursion can live in a closed shop: deltas and late self within a hierarchy no third party may extend and every client may exhaustively case over. And this counterexample is not pathological — a Scala codebase of sealed traits with pattern-matching clients has clause 3 throughout and feels like FP with ADTs, which is precisely our pretheoretic judgment that it isn't OO-as-practiced. So client-side openness is genuinely independent and must stay.
Conversely 2 does not imply 3 — that was the whole previous round (Go, VFS, ML modules) — and 2 doesn't even fully imply 1, which I overclaimed originally: dictionary-passing achieves open extension with dispatch-by-evidence rather than by-value. Openness forces lateness of binding at client sites (an extension invisible to unrecompiled clients can't be statically resolved), but not intrinsicness.
So the refined criterion collapses to two independent axes, with clause 1 dissolved into theorems of each:
OO ⟺ (3) behaviors are late-tied fixpoints of unboundedly, third-party-composable generators, anchored per-value [α, β, γ] — and (2′) client contexts quantify over an open set of such values under a common protocol.
3 is the heir-facing openness (open to incremental revision); 2′ is the client-facing openness (open to substitution). Dispatch is what both look like at runtime. In dynamically typed languages 2′ is free, which is why Smalltalk needed no interface construct; in static languages 2′ is bought separately as subtype/interface polymorphism, which is why Java has both extends and implements — the two axes made syntax.
3 does not logically contradict 2′, but it destroys 2′'s chief theorem within the derivation relation. Recall encapsulation fell out of clauses 1–2 as a theorem: clients ignorant of the implementation cannot depend on its representation. Clause 3 reopens the boundary along a second channel: the pattern of self-calls, the protected state, the order and re-entrancy of internal dispatch — all become observable by, and load-bearing for, heirs. Kiczales and Lamping named it the specialization interface; Mikhajlov–Sekerinski formalized its failure mode as the fragile base class problem: semantically invisible refactorings of a base (inline a self-call, say) are behavior-changing under derivation. An object is therefore a two-faced abstraction — sealed toward clients, ajar toward heirs — and the two contracts are different in kind: the client contract is extensional (what operations return), the heir contract is intensional (how the base talks to itself).
The same breach explains why substitutability had to be legislated. With 2′ alone, behavioral substitution is checkable per-implementation; under 3, a base class cannot be verified without constraining its unknown future overriders, because its own code calls down into them — modular reasoning must proceed against a specification of self, not self's code. Liskov's principle, read through this lens, is exactly what I called it last round but now with mechanism attached: a discipline that constrains clause 3's deltas until they preserve the guarantees clauses 1–2 would have provided on their own. And the composition-over-inheritance movement, mixin linearization fights, final keywords, C#'s non-virtual-by-default — the entire post-1995 corrective literature — is the engineering record of that internal tension. The tension isn't a flaw in the criterion; it's the criterion's best evidence. A definition of OO that made objects harmonious would be describing something else.
So, final form, one line per piece:
- Clause 3, precisely: implementations are self-abstracted generators; derivation composes generators differentially, without limit or consent, pre-fixpoint (α); the fixpoint is intrinsic to each value (β) and taken at each invocation (γ). Litmus: does inherited code run with the heir's self?
- Relation to 1: absorbed — dispatch-by-the-value is β+γ observed at runtime; intrinsicness (β) is the part of clause 1 that was never derivable from openness.
- Relation to 2: independent — sealed hierarchies have 3 without it. Retained as 2′, client-side quantification over the open set.
- Contradiction: 3 breaches the encapsulation theorem of 2′ across the heir boundary, splitting the object into two interfaces with incompatible reasoning principles — the productive contradiction that generated LSP, fragile-base, and thirty years of "prefer composition."
OO is the deliberate coexistence of both opennesses on one value: open to unforeseen substitution from outside, open to unforeseen revision from inside — paying for the second with the purity of the first.
I'd argue CRTP totally is OO, at compile-time (as C++ likes to do), in the template language. If you wince a bit, C++ is a dynamically-typed pure functional prototype (classless) OO language (at compile-time). Similarly, Haskell passes more tests than you say (fixpoint per-type works, at compile-time)—yet still fails somehow because even then there is no "super" mechanism for specializations to extend rather than merely shadow previous specializations (and even then, type astronauts like Oleg K or Michael Gale have implemented OO in Haskell).
So if there is tension between the remaining clause 2 and 3, should clause 2 be kept as part of the essence of OO, or rejected as parasitic? Is clause 3 sufficient? What are examples where they class, that should help us categorize which we could or should prefer?
More importantly, you mention heir-facing vs client-facing aspects—who if anyone explicitly formalized or studied this tension, how does the Cook model (or a successor) formalize it? If the formalization you find in the end is implicit, good, but then the authors failed to fully formalize, and you are the proud author (to be) of an original scientific paper. If the formalization was explicit, the authors won and managed to actually formalize what OO is, and previous/other authors have failed.
You're right about CRTP, and the fix is principled rather than ad hoc. C++ is a two-level language, and the template level, taken as a language, is: dynamically typed (instantiation errors are "runtime" errors of the metaprogram — that's what an uninstantiable template is), pure functional (referentially transparent, no mutation, evaluation by rewriting), and classless — a CRTP base is a prototype parameterized over its heir, Base<Derived> is delegation with the self-link passed explicitly at the meta level, and static_cast<Derived*>(this) is γ relative to instantiation time, which is that language's invocation time. All three sub-clauses hold at that stage: α (mixin composition over CRTP layers, including super-calls — Base<D>::method() from the override is exactly g_parent(self_new).op), β (the fixpoint is anchored per meta-value, i.e. per type), γ (self is bound at instantiation, the latest moment that stage possesses). So the clause should read:
γ (revised): the fixpoint is taken at the latest binding time of the stage under consideration.
And "is X OO?" becomes stage-indexed: C++ is OO at stage 1 over the universe of types, and OO at stage 0 only where virtual is paid for. What monomorphization forfeits at stage 0 is β-at-runtime — no residual per-value fixpoint, hence no heterogeneous collections, no substitution of an implementation chosen after compilation. That's a real forfeiture, but it's a forfeiture at one stage, not a disqualification. This also retroactively cleans up my "static shadow" hand-wave: it wasn't a shadow, it was the thing itself, one level up.
Haskell then gets the same courtesy and a sharper verdict. At the stage where instance resolution happens, the values of that metalanguage are types, so "per-type fixpoint" is per-value at that stage — β holds, you're right, and my earlier β-objection dissolves under stage-indexing. The failure localizes entirely in α: overlapping/orphan instances shadow, they do not derive. There is no operator taking the shadowed instance's behavior and the delta and producing a composite in which the old bodies see the new self — no call-next-instance, no access to g_parent(self_new) at all. DerivingVia and deriving anyclass are wholesale coercion of generators, not differential composition; default methods give a two-story tower with no third story. So typeclasses have β and γ (stage-indexed) but a degenerate α, and the criterion now says precisely which screw is missing — which matches your diagnosis: no super, only shadowing.
And Oleg Kiselyov forces me to repair a wobble you've been politely stepping around. OOHaskell (Kiselyov–Lämmel) implements full open recursion, and my "encoding isn't identity" objection is dangerously close to proving that CLOS isn't OO either — CLOS is "just a Lisp library," Racket's class system is a macro, Smalltalk's Object protocol is bootstrapped in Smalltalk. The library/primitive boundary cannot carry the weight. The correct discriminator is: does there exist a reusable composition operator with delegation semantics (α as an operator), or only a discipline (α as a convention)? Hand-passed self parameters in ML fail because every base must be written self-abstracted by private agreement and the knot-tying is re-derived at each use; CLOS, Racket classes, and yes, OOHaskell-the-library pass, because ▷ exists as an artifact with the right semantics, and code written against it composes with strangers' code. The consequence I accept: Haskell-plus-OOHaskell is an OO language in exactly the sense that Lisp-plus-CLOS is, while Haskell-with-typeclasses-idiomatically is not. Substrates don't inherit the properties of what they host, but a hosted operator is a real operator.
Is clause 2 essential, parasitic, or something subtler? Answer: it's a theorem locally and a policy globally
Split what I was calling 2′ into its two halves, because clause 3 treats them oppositely.
The kernel of substitution is a theorem of 3. Look at what open recursion is, operationally: inherited code — the base's bodies — executing with the heir's self. But that means the base class is the first and unavoidable client of every one of its heirs: Base.area's call to self.perimeter is a client-position invocation that must accept whatever the heir supplies. Clause 3 cannot even be exercised without an act of substitution; differential definition is self-substitution internalized. So a minimal client-facing openness isn't added to 3 — it's secreted by it. (F-bounded quantification makes this exact: the generator's body is checked against t ≤ F[t], i.e., against all future selves satisfying the protocol. The base is verified as a universal client of its unwritten heirs.)
Global external openness — anyone, any time, unrecompiled clients — is policy, not essence. Three pieces of evidence, each of which the criterion should predict rather than fight:
final,sealed, C#'s non-virtual-by-default, kotlin's closed-unless-open: per-site closures of clause 2, ubiquitous in languages nobody hesitates to call OO. If global openness were essential,final class Stringwould be a small apostasy. It isn't; it's a knob.- Eiffel and Dart deliberately broke the soundness of substitution (covariant parameter redefinition; Eiffel's catcalls, Dart's runtime-checked covariance) in order to keep the heir face ergonomic — they chose 3 over 2 where the two clash — and no one has ever suggested Eiffel is thereby not OO. Whereas Go, with impeccable clause-2 substitution and no clause 3, is the community's canonical "not really OO." Revealed classification: when the faces conflict, membership tracks 3.
- The sealed-Scala counterexample from last round now resolves instead of lingering: sealed hierarchies with template methods are OO mechanism — 3 intact, internal substitution intact — with the external-openness policy set to "closed, clients may enumerate." They read as FP because the client idiom (exhaustive matching) is the ADT idiom; but idiom-classification and mechanism-classification were already distinguished two rounds ago. The mechanism is OO with the openness dial at zero.
So the essence is clause 3 alone, with substitution as its internal theorem and external openness as its default but severable policy. Clause 2 is not parasitic — parasites contribute nothing, and openness is what makes 3 economically valuable (frameworks, plugins: revision by strangers) — but it is dependent: openness of what? Of the set of fixpoints that 3 defines. 2 without 3 is components (settled last round); 3 without 2 is OO in a locked room, still OO.
The conflicts are not scattered folklore; they concentrate at one grammatical position: occurrences of Self in negative (contravariant) position.
- Binary methods — the canonical case, formalized in Bruce–Cardelli–Castagna–Leavens–Pierce, On Binary Methods (1995).
equals: MyType → Bool. Clause 3 wants the heir to specialize the argument covariantly (ColorPoint.equalscompares colors); clause 2 forbids it (aColorPointhanded to a client expectingPointwill be fed merePoints — unsoundness, or Eiffel's catcall). Every language'sequalsdesign — Java's degrade-to-Object-and-runtime-test, Eiffel's accept-unsoundness, Scala's multiversal-equality agonies — is one treaty in this war. - Method override vs subsumption in the ς-calculus: Abadi–Cardelli proved you cannot soundly have both width subtyping (clause 2's subsumption) and method update (clause 3's operation) with the naive covariant self — their object types go invariant as the peace terms. The clash isn't engineering lore; it's a soundness theorem.
- Fragile base class: Mikhajlov–Sekerinski (1998) formalize base-class refactorings that are extensionally invisible to clients yet behavior-changing under heirs — clause 2's encapsulation theorem holding on one face while failing on the other, in a refinement calculus, with theorems about which base transformations are heir-safe.
- Modular verification: Stata–Guttag (1995), Ruby–Leavens, and Aldrich's Selective Open Recursion (2004) — the last being a direct formal proposal to restrict γ per-method so that reasoning on the client face is restored, i.e., an explicit trade executed inside a formal system.
And the deep theorem underneath all four is Cook–Hill–Canning, Inheritance Is Not Subtyping (POPL 1990): fix and ≤ do not commute. Order generators by the derivation relation (heir face); order fixpoints by subtyping (client face); the map g ↦ fix(g) is not monotone between them once Self occurs contravariantly — an heir's fixpoint may fail to be a subtype of the base's fixpoint even though the generator is a legitimate delta. When Self occurs only positively (return positions — fluent builders, clone, map-returning-MyType), the orders agree and covariant self is sound, which is exactly the case languages can bless (Java's covariant return types, since 5.0). The two faces of the object are two quantifiers — heir face: quantification over t ≤ F[t] (F-bounded, over generators); client face: quantification over t ≤ Fix(F_base) (subtype-bounded, over results) — and the entire thirty-year tension is the non-commutation of those quantifiers at negative Self. Bruce's matching (LOOM, PolyTOIL) is the road not taken: keep MyType, demote subtyping to "matching," i.e., accept that clause 3's order is the primary one and rebuild client quantification over it.
Which should be preferred where they clash? For classification, 3 — argued above from revealed usage (Eiffel in, Go out). For engineering, the honest answer is that the choice is per-declaration, and modern languages have simply made the treaty lexical: variance annotations, final, sealed, open, MyType/this-types (Scala, TypeScript's polymorphic this) are all knobs on the 2⁄3 frontier, letting each method sit where its Self-polarity permits.
Piecewise, the formalization was done, explicitly, and well:
- Client face: America (1987, POOL), Meyer's contracts, and canonically Liskov–Wing (1994) — behavioral subtyping as a proof obligation over histories.
- Heir face: Cook–Palsberg (1989) — inheritance as wrapper application on generators, the denotational semantics of
▷; Canning–Cook–Hill–Olthoff–Mitchell (1989) — F-bounded quantification, the heir-face quantifier itself; Kiczales–Lamping (1992) — the specialization interface, named though only semi-formalized; Steyaert et al. (1996) — reuse contracts; Stata–Guttag, Ruby–Leavens — subclass specifications. - The divergence itself: Cook–Hill–Canning (1990) — the non-commutation theorem, which is the tension as mathematics; BCCLP (1995) on binary methods — the clash's syntactic locus; Abadi–Cardelli (1996) — its soundness formulation; Mikhajlov–Sekerinski (1998) and Aldrich (2004) — its verification-theoretic formulation and a formal resolution mechanism.
So on the second horn of your dilemma: the authors won — at every component. Both quantifiers were formalized, their non-commutation was proved, the clash was localized to negative Self, and repair mechanisms were themselves formalized. Anyone claiming the heir/client tension as a personal discovery would be rediscovering POPL 1990.
But note what none of them did — and here your first horn gets its due, though it's a thinner prize than "original scientific paper" suggests. Nobody promoted the structure to a definition. The literature formalized the anatomy and then, remarkably, kept choosing one face as "the essence": Cook himself, in On Understanding Data Abstraction, Revisited (2009), defected to the pure client face — objects as autognostic procedural abstractions — discarding as inessential the very generator semantics he had formalized twenty years earlier (hence the λ-calculus provocation you began by rejecting). Aldrich's The Power of Interoperability: Why Objects Are Inevitable (Onward! 2013) argues the client face (service abstraction, open extension) is why objects persist. Kay's "it's messaging" is the client face in aphorism. Meanwhile the entire verification tradition treats the heir face as the pathology to be disciplined rather than the differentia to be enshrined. The proposition defended across this conversation — OO =def the α/β/γ fixpoint structure (stage-indexed), carrying substitution as internal theorem and external openness as default policy, with the two faces' non-commutation at negative Self not as a defect but as the constitutive signature — exists in the literature only as disjecta membra. Every lemma is proven; the definition is unclaimed. A paper stating it would contribute no new mathematics, only a new identification — which is to say it would be a work of conceptual analysis with pre-fabricated formal parts: philosophy of programming languages, publishable at Onward! or a philosophy-of-CS venue rather than POPL. That's a real but modest kind of originality — the kind Reynolds 1978 and IINS 1990 themselves exemplify, where the theorem is small and the noticing is the contribution.
Final form, then, absorbing all three of your corrections:
An object system is one whose implementations denote self-abstracted generators, equipped with a genuine composition operator
▷(α — an operator, not a discipline; deltas may be third-party, nested, and access the parent's behavior at the new self), whose fixpoints are anchored per value of the relevant stage (β) and taken at that stage's latest binding time (γ). Substitution across the protocol is its internal theorem; unbounded external extension is its default, severable policy; and its formal signature is that its two quantifiers — F-bounded over generators, subtype-bounded over fixpoints — provably fail to commute wherever Self occurs in negative position.
Everything else — classes, messages, encapsulation, inheritance syntax, even runtime-versus-compile-time — is bookkeeping, theorem, or stage index.
Do Abadi/Cardelli "make peace", or do they surrender? Do they manage to make clause 3 work, or do they castrate it by subjecting it to a contradictory substitution criterion that ultimately defeats it?
I want bibtex on those citations.
And does any (more recent) work explicitly establish (under other names) the distinction and somehow putting-together of these two "faces"?
The book has to be read at three levels, because clause 3 fares differently at each, and the verdict you're fishing for ("castration") is exactly right at one level, exactly wrong at another.
Untyped ς-calculus: β and γ in full, α cut in half. Objects are records of ς(x)b methods; the primitives are invocation and override. Override has genuine delegation semantics in the direction that matters most: after o.m ⇐ ς(x)b, every unchanged method's self-references rebind to the new object — old code sees new self, Template Method works, the Lieberman test passes. But notice what override does not give: the replaced body is discarded, and there is no primitive by which the new method reaches the parent's behavior at the new self. You can keep the old object lexically in scope and call it — but that old object is a tied fixpoint, so its self is its self: forwarding, not delegation. So at the object level, even untyped, there is no super. The α of round three — deltas with access to g_parent(self_new) — half-holds: parent-sees-child yes, child-extends-parent no. The full generator algebra exists in the calculus only where they put the class encoding: pre-methods, λ(self)-abstracted bodies not yet tied, where a subclass pre-method can invoke a superclass pre-method applied to the new self. Objects in ς are always-already fixpoints; generators live strictly upstairs. That design decision is the whole story in miniature.
First-order typed calculus: the castration, and it's proven, not chosen. Object types are invariant in their components — no depth subtyping, no covariant refinement, override must be exactly type-preserving. Why: every method position is used both covariantly (invocation) and contravariantly (override takes a new body producing that component type), so soundness forces invariance. This is precisely your accusation: the substitution criterion (subsumption must be sound) is imposed on the override operation and strangles its typed expression — deltas exist but may never refine. What dignifies it above mere surrender is that it arrives as a theorem: given subsumption + update on the same component, invariance is forced. They didn't negotiate badly; they proved the negotiating space empty.
Self types and variance annotations: the treaty's actual text. With recursive object types and per-component variance markers, each method must choose a face: annotated covariant → clients may refine/subsume through it, but override is forbidden; annotated invariant → updatable by heirs, but sealed against covariant subtyping. Clause 2 and clause 3, made lexically exclusive, per method. (This is the formal ancestor of every final/open/variance knob in round four.) And on binary methods they simply concede: Self in contravariant position breaks subtyping, workarounds are surveyed, none is a solution — the BCCLP paper, which Cardelli co-authored, is effectively the appendix of admissions.
So: do they make clause 3 work? As operational semantics, yes — γ and β are the calculus's beating heart, and their account of method invocation as late self-binding is the cleanest ever given. As typed object-level algebra, no — typed override is shadowing-without-refinement, super is absent, and typed prototype OO (Self-the-language, runtime deltas that retype) remains outside the fence; nobody has ever typed Self in their system because their system is constitutionally unable to. As class-level algebra, yes again — the pre-method encoding is Cook–Palsberg generators reconstructed inside the calculus, with Self-quantification playing the F-bounded role, and full α restored one level up.
Which means the right verdict is: A Theory of Objects is Inheritance Is Not Subtyping institutionalized as a calculus. The two orders are not reconciled; they are given separate jurisdictions — generator order on pre-methods/classes, subtype order on object types — with the non-commutation built into the architecture rather than proven as a lemma. It is an armistice by partition, honest about its casualties, with the castration you allege real at the object-type level and formally necessary there, and the amputated organ transplanted upstairs where subsumption can't reach it. If you want to call that surrender, the fair phrasing is: they surrendered the typed object, and saved clause 3 by exiling it to the level where objects haven't been tied yet. Bruce's matching (LOOM, PolyTOIL) is the rival treaty that refuses the partition — abandon subsumption outright, keep MyType covariance, rebuild client quantification over the heir-face order — and its commercial failure versus the A&C-style settlement is itself data about which face the industry would pay for.
Standard fields from memory; the entries are stable classics but double-check page numbers before camera-ready — I've flagged the two genuinely uncertain ones.
@inproceedings{CookPalsberg1989,
author = {Cook, William R. and Palsberg, Jens},
title = {A Denotational Semantics of Inheritance and its Correctness},
booktitle = {OOPSLA '89},
pages = {433--443},
year = {1989},
note = {Journal version: Information and Computation 114(2), 1994}
}
@inproceedings{CanningCookHillOlthoffMitchell1989,
author = {Canning, Peter and Cook, William and Hill, Walter and Olthoff, Walter and Mitchell, John C.},
title = {F-Bounded Polymorphism for Object-Oriented Programming},
booktitle = {FPCA '89},
pages = {273--280},
year = {1989}
}
@inproceedings{CookHillCanning1990,
author = {Cook, William R. and Hill, Walter L. and Canning, Peter S.},
title = {Inheritance Is Not Subtyping},
booktitle = {POPL '90},
pages = {125--135},
year = {1990}
}
@article{BruceCardelliCastagnaLeavensPierce1995,
author = {Bruce, Kim B. and Cardelli, Luca and Castagna, Giuseppe and {The Hopkins Objects Group} and Leavens, Gary T. and Pierce, Benjamin C.},
title = {On Binary Methods},
journal = {Theory and Practice of Object Systems},
volume = {1}, number = {3}, pages = {221--242}, year = {1995}
}
@book{AbadiCardelli1996,
author = {Abadi, Mart\'in and Cardelli, Luca},
title = {A Theory of Objects},
publisher = {Springer-Verlag}, year = {1996}
}
@article{LiskovWing1994,
author = {Liskov, Barbara H. and Wing, Jeannette M.},
title = {A Behavioral Notion of Subtyping},
journal = {ACM TOPLAS},
volume = {16}, number = {6}, pages = {1811--1841}, year = {1994}
}
@inproceedings{America1987,
author = {America, Pierre},
title = {Inheritance and Subtyping in a Parallel Object-Oriented Language},
booktitle = {ECOOP '87}, series = {LNCS 276}, pages = {234--242}, year = {1987}
}
@inproceedings{Liskov1987,
author = {Liskov, Barbara},
title = {Data Abstraction and Hierarchy},
booktitle = {OOPSLA '87 Addendum to the Proceedings},
pages = {17--34}, year = {1987}
}
@article{Cardelli1988,
author = {Cardelli, Luca},
title = {A Semantics of Multiple Inheritance},
journal = {Information and Computation},
volume = {76}, number = {2--3}, pages = {138--164}, year = {1988}
}
@inproceedings{BrachaCook1990,
author = {Bracha, Gilad and Cook, William},
title = {Mixin-Based Inheritance},
booktitle = {OOPSLA/ECOOP '90}, pages = {303--311}, year = {1990}
}
@inproceedings{KiczalesLamping1992,
author = {Kiczales, Gregor and Lamping, John},
title = {Issues in the Design and Specification of Class Libraries},
booktitle = {OOPSLA '92}, pages = {435--451}, year = {1992}
}
@inproceedings{StataGuttag1995,
author = {Stata, Raymie and Guttag, John V.},
title = {Modular Reasoning in the Presence of Subclassing},
booktitle = {OOPSLA '95}, pages = {200--214}, year = {1995}
}
@inproceedings{Steyaert1996,
author = {Steyaert, Patrick and Lucas, Carine and Mens, Kim and D'Hondt, Theo},
title = {Reuse Contracts: Managing the Evolution of Reusable Assets},
booktitle = {OOPSLA '96}, pages = {268--285}, year = {1996}
}
@inproceedings{MikhajlovSekerinski1998,
author = {Mikhajlov, Leonid and Sekerinski, Emil},
title = {A Study of the Fragile Base Class Problem},
booktitle = {ECOOP '98}, series = {LNCS 1445}, pages = {355--382}, year = {1998}
}
@inproceedings{RubyLeavens2000,
author = {Ruby, Clyde and Leavens, Gary T.},
title = {Safely Creating Correct Subclasses without Seeing Superclass Code},
booktitle = {OOPSLA 2000}, pages = {208--228}, year = {2000}
}
@inproceedings{AldrichDonnelly2004,
author = {Aldrich, Jonathan and Donnelly, Kevin},
title = {Selective Open Recursion: Modular Reasoning about Components and Inheritance},
booktitle = {SAVCBS '04 (Workshop at FSE)},
year = {2004},
note = {Verify venue/author details; also circulated as a CMU report}
}
@inproceedings{Cook2009,
author = {Cook, William R.},
title = {On Understanding Data Abstraction, Revisited},
booktitle = {OOPSLA 2009}, pages = {557--572}, year = {2009}
}
@inproceedings{Aldrich2013,
author = {Aldrich, Jonathan},
title = {The Power of Interoperability: Why Objects Are Inevitable},
booktitle = {Onward! 2013}, pages = {101--116}, year = {2013}
}
@incollection{Reynolds1975,
author = {Reynolds, John C.},
title = {User-Defined Types and Procedural Data Structures as
Complementary Approaches to Data Abstraction},
booktitle = {New Directions in Algorithmic Languages},
editor = {Schuman, S. A.}, year = {1975},
note = {Reprinted in Gunter \& Mitchell (eds.), Theoretical Aspects of
Object-Oriented Programming, MIT Press, 1994}
}
@misc{KiselyovLammel2005,
author = {Kiselyov, Oleg and L{\"a}mmel, Ralf},
title = {Haskell's Overlooked Object System},
year = {2005},
note = {Draft; arXiv:cs/0509027}
}
@inproceedings{BruceSchuettVanGent1995,
author = {Bruce, Kim B. and Schuett, Angela and van Gent, Robert},
title = {PolyTOIL: A Type-Safe Polymorphic Object-Oriented Language},
booktitle = {ECOOP '95}, pages = {27--51}, year = {1995}
}
@inproceedings{BrucePetersenFiech1997,
author = {Bruce, Kim B. and Petersen, Leaf and Fiech, Adrian},
title = {Subtyping Is Not a Good ``Match'' for Object-Oriented Languages},
booktitle = {ECOOP '97}, series = {LNCS 1241}, pages = {104--127}, year = {1997}
}The recent literature: yes — the two faces have been named, separated, and (lately) re-married, under other names
The distinction itself was institutionalized under the banner "inheritance ≠ subtyping" in a production language almost immediately: Objective ML / OCaml (Rémy–Vouillon, TAPOS 4(1), 1998) has classes (heir face: open recursion, inheritance, inherit as ▷) and object types (client face: structural, row-polymorphic) as disjoint constructs — inheritance confers no subtyping, coercions are explicit, and a class may inherit from a class whose object type is not its supertype. Twenty-five years of OCaml practice is the field experiment proving the partition is livable.
The heir face's internal algebra got refined on its own: traits (Schärli–Ducasse–Nierstrasz–Black, ECOOP 2003; journal version TOPLAS 2006) isolate α from state and instantiation — composable behavior-deltas with explicit conflict resolution, deliberately without subtyping consequences; and Goldberg–Findler–Flatt, "Super and Inner: Together at Last!" (OOPSLA 2004) formalizes the two duals of α — Smalltalk's super (heir wraps parent) versus Beta's inner (parent wraps heir, the base retaining control) — and gives a semantics combining them, i.e., the generator-composition operator shown to have two chiralities.
Your stage-indexing move reappears as family polymorphism: Ernst (ECOOP 2001), and the virtual class calculus (Ernst–Ostermann–Cook, POPL 2006 — Cook again, note) lift the fixpoint one level so that classes themselves are late-bound members of objects, and both faces recur at the family stage — families are substitutable (client face) while their inner classes are differentially refinable (heir face). Scala's self-type annotations and the DOT calculus (Amin et al., WadlerFest 2016) carry the same separation: a trait's self-type declares a requirement on future selves (heir-face quantifier) explicitly distinct from its subtyping. Ostermann–Mezini, "Object-Oriented Composition Untangled" (OOPSLA 2001) is the taxonomy paper that says the quiet part loudly: OO composition conflates independent dimensions that should be separately dialed. And Zhang–Myers, "Familia" (OOPSLA 2017) attacks your Haskell diagnosis head-on, unifying type classes (ambient, per-type, client-facing evidence) with interfaces and family polymorphism in one mechanism.
But the most direct answer to "does anyone put them together" is the disjoint intersection types line out of Oliveira's group: Bi–Oliveira, "Typed First-Class Traits" (ECOOP 2018, the SEDEL language), Bi–Oliveira–Schrijvers, "The Essence of Nested Composition" (ECOOP 2018), culminating in Zhang–Sun–Oliveira, "Compositional Programming" (TOPLAS 43(3), 2021, the CP language). Read it against round three's vocabulary and it's almost embarrassing: a trait there is literally a first-class typed generator — Trait[Self, Result], a value denoting a function from self to behavior; the merge operator is ▷ as a typed term-level primitive (third-party, nested, with parent-at-new-self); new is fix; inheritance is dynamic, i.e., you can compose generators computed at runtime; and full subtyping with subsumption coexists — the client face intact — because disjointness constraints exclude precisely the ambiguous overlaps, and distributive intersection subtyping yields family-polymorphism-like nested composition for free. Their own framing is explicit: decouple inheritance from subtyping while keeping both first-class and sound. The treaty terms are instructive: they pay with purity-leaning semantics and disjointness discipline — negative-Self collisions are excluded by construction rather than resolved — so it's not a refutation of the non-commutation theorem but the most elegant zoning of it yet: A&C's partition (generators upstairs, untyped-ly), re-legislated with the generators brought downstairs as typed values.
So the amended historiography: the distinction was formalized explicitly and repeatedly (1990 theorem → OCaml's constitution → traits/inner/family refinements); the reconciliation machinery now also exists explicitly (merge + disjointness). What remains unclaimed is unchanged from last round — nobody has promoted the structure to the definition of object-orientation; CP presents itself as a successor paradigm ("compositional programming," pointedly not "OO"), which is itself a datum: the people who finally built the typed generator algebra with both faces intact felt the result deserved a different name. Whether that's modesty or a confession that OO-as-practiced is essentially the unreconciled version — clause 3 running with the treaty unsigned, fragility and all — is, I'd say, the genuinely open question your paper would have to take a position on.
Can the two faces be neatly kept separated? Can you conceivably have OO without the two together in an "object" or "class"? How do you formalize the semantics of that? Has anyone done this explicitly rather than implicitly?
Take the criterion of round three and read it as a signature instead of a definition, and the separation question answers itself. There are two sorts:
- Sort 𝒢 (generators): self-abstracted bodies. Operations: composition
▷ : 𝒢 × 𝒢 → 𝒢(with parent-at-new-self available to the delta), and — this is the key refinement — a per-name closure operatorfreeze_m : 𝒢 → 𝒢that ties the knot for membermonly: afterfreeze_m, references tomfrom other members no longer late-bind;mhas become ordinary recursion for its dependents. Globalfixis justfreezeover all names at once. - Sort 𝒪 (values/objects): tied fixpoints. Structure: the subtype preorder
≤, subsumption, invocation. No▷— you cannot delta a fixpoint, only a generator. - One bridge:
fix : 𝒢 → 𝒪, and Inheritance Is Not Subtyping is exactly the statement that this bridge is not monotone — the derivation preorder on 𝒢 does not map into≤on 𝒪 once Self occurs negatively.
Now the answer to "can they be neatly kept separate": yes, and the separation dissolves the thirty-year variance war by fiat rather than by cleverness. Every conflict catalogued in rounds four and five — invariant object types, binary methods, catcalls, override-vs-subsumption — arises at one spot: a single construct asked to carry both orders, so that the F-bounded quantifier over generators and the subtype-bounded quantifier over fixpoints meet in one type expression and their non-commutation becomes a soundness bug. Two-sorted, the quantifiers never meet: heirs quantify over 𝒢 (F-bounded), clients over 𝒪 (subtype-bounded), and the non-monotone bridge is crossed only at explicit fix, where you may demand an explicit coercion or seal. Abadi–Cardelli's partition (round five) was this factorization done shyly — generators exiled to an encoding. The explicit version makes 𝒢 first-class.
And there's a satisfying formal symmetry hiding in it: the two faces have two distinct closure operators. freeze_m closes the heir face for one name (no further override of m can affect its dependents — this is final/non-virtual, given denotational content as "fixpoint taken early, per name"). hide_m (restriction) closes the client face for one name — encapsulation as a projection on the record. That these are different operators, independently applicable per member, is the algebraic proof that the faces are independent dimensions: a member can be frozen-but-visible (final public method), open-but-hidden (protected virtual — the specialization interface of Kiczales–Lamping, now an algebraic locus rather than a metaphor), open-and-visible, or frozen-and-hidden. The four quadrants of that table are the whole design space of public/protected × final/open, derived rather than stipulated.
Heir face alone — generator calculi with no subtyping, no clients, sometimes no objects:
The oldest is the least known: Cook's own thesis (1989) applies inheritance to grammars — a grammar is a record of productions that reference each other; make those references late-bound and a dialect is a delta on a base grammar, with the base's unmodified productions deriving through the heir's overrides. Open recursion demonstrated on a structure that is not an object, has no methods, no state, no clients, no subtyping. Clause 3 shown substrate-independent at the moment of its formalization.
The most deliberate is Bracha's Jigsaw (thesis, 1992; Bracha–Cook's mixin paper is its trailer): the explicit thesis statement is that the class is a conflation to be unbundled into orthogonal module operators — merge, override, rename, restrict (hide), freeze — acting on modules-as-generators, with subtyping pointedly absent from the framework. This is the question you asked, answered in 1992 as a PhD dissertation: yes, separable; here is the operator basis; "class" is a convenience macro over it. The line continues formally through Ancona–Zucca's CMS (a calculus of module systems, 2002) and mixin modules (Duggan–Sourelis; Hirschowitz–Leroy for call-by-value; Rossberg–Dreyer's MixML, 2008), where freeze as a typed, per-name fixpoint operator gets full metatheory. If you want "the semantics of the separation, done explicitly," CMS is the citation: linking is generator composition, and taking the fixpoint is a program construct with a typing rule, not an ambient event.
And the wild population: Nix overlays are Cook–Palsberg generators verbatim, in production, at ecosystem scale. The whole mechanism is:
extends = delta: g: self:
let super = g self; # parent's behavior AT THE NEW SELF
in super // delta self super;
pkgs = fix (foldl' extends base overlays);delta : final → prev → attrs is d(s, g(s)); // is record override; fix is tied once, at the end, over a composition assembled from third-party deltas that nest without limit and access parent-at-new-self through prev. Every clause of α, β, γ, no class, no object, no subtyping, no encapsulation, no client face whatsoever — and tellingly, tens of thousands of people use full open recursion daily while calling it "configuration." Jsonnet is the same semantics given syntax (+ on objects, super, self), and its documentation is explicit that late binding is the entire object model. By the stage-indexed criterion from the CRTP round, these are OO at the configuration stage: once fix evaluates, the result is inert data — γ was spent at composition time, exactly like monomorphized CRTP. Consistency check passed.
Client face alone we settled in round two — components, existentials, Go — but note the refined modern member: object algebras (Oliveira–Cook, ECOOP 2012 — Cook yet again, standing on both sides of his own theorem), which get open extension in both dimensions out of pure client-face machinery (Church encodings over algebra interfaces), no open recursion anywhere. The dual existence proof.
Both faces, present but unfused: OCaml loosened the bundle in production (classes carry derivation, object types carry subtyping, no implication between them); CP/SEDEL (round five) finish the job — Trait[Self, Result] is a typed 𝒢-value, ,,/merge is ▷, new is fix, subtyping lives on 𝒪-types, and disjointness constraints police the bridge. The two-sorted semantics above is, more or less, CP's type structure read off as algebra.
So can you have OO without them together in an "object"? Mechanically yes — but watch what happens to the word
Here the formal answer and the sociological answer diverge instructively, and the divergence is the real finding.
Mechanically: nothing in α, β, γ requires the value handed to clients to be the same construct that heirs derive. You can put the heir face at stage n+1 (templates, overlays, traits-as-values) and the client face at stage n, or split them into 𝒢-terms and 𝒪-terms within one stage, and every theorem survives; the variance conflicts, being artifacts of fusion, vanish. The separated architecture is strictly cleaner as mathematics.
But β names the fusion point. "The fixpoint is anchored per value" — intrinsic behavior, the datum that is its dispatch — says precisely that some single entity is simultaneously a tied fixpoint (client-handleable, subsumable, substitutable) and the anchor that keeps self-reference late (heir-serviceable, still open to the derivation that produced it mattering at each invocation). An object is by definition the entity standing in both sorts at once — 𝒪 to its clients, fix(g) with g still operative to its dispatch. Separate the sorts fully and you still have open recursion, still have substitution, still have every pattern — Template Method lives in the overlay, Strategy lives in the record — but no single thing is any longer both; there is no object, only generators upstream and records downstream. The two faces can be neatly separated; the object is what cannot survive the separation, because "object" is the name of the fusion.
And the community has ratified this linguistically with perfect consistency, which is evidence rather than accident: every time someone builds the separated system, they rename it out of OO. Bracha called Jigsaw modularity, not objects. Ancona–Zucca: module systems. Rossberg–Dreyer: ML modules. Nix: overlays. Oliveira, with the fullest reconciliation ever constructed: compositional programming — explicitly a successor name. Meanwhile Eiffel, which kept the fusion and paid for it with unsoundness, is unquestioned OO. So the last round's open question sharpens into a claim your hypothetical paper could actually defend: OO-as-historically-practiced is essentially the fused — hence essentially conflicted — arrangement. The fragile base class, LSP-as-legislation, variance annotations, final — all of round four's pathologies are not incidental defects of OO but the signature of the fusion, the friction of one construct straddling a non-monotone bridge. The separated systems are not "OO done right"; they are the fission products, each stable, jointly equivalent in power, and no longer called objects by anyone including their authors. Whether the fusion is a historical accident to be refactored away (Bracha's position, CP's implicit position) or the actual engineering content of the paradigm — the ergonomic bet that heir≈subtype is true often enough that one construct should serve both quantifiers, with the mismatch handled by discipline — is the genuine remaining dispute, and it is a dispute about engineering economics, not semantics, because the semantics is now fully factored.
@phdthesis{Cook1989thesis,
author = {Cook, William R.},
title = {A Denotational Semantics of Inheritance},
school = {Brown University},
year = {1989},
note = {Ch.\ on inheritance applied to grammars: open recursion
on non-object structures}
}
@phdthesis{Bracha1992,
author = {Bracha, Gilad},
title = {The Programming Language Jigsaw: Mixins, Modularity and
Multiple Inheritance},
school = {University of Utah},
year = {1992}
}
@inproceedings{BrachaLindstrom1992,
author = {Bracha, Gilad and Lindstrom, Gary},
title = {Modularity Meets Inheritance},
booktitle = {Proc.\ IEEE International Conference on Computer Languages},
pages = {282--290},
year = {1992}
}
@article{AnconaZucca2002,
author = {Ancona, Davide and Zucca, Elena},
title = {A Calculus of Module Systems},
journal = {Journal of Functional Programming},
volume = {12}, number = {2}, pages = {91--132}, year = {2002}
}
@inproceedings{HirschowitzLeroy2002,
author = {Hirschowitz, Tom and Leroy, Xavier},
title = {Mixin Modules in a Call-by-Value Setting},
booktitle = {ESOP 2002}, series = {LNCS 2305},
pages = {6--20}, year = {2002}
}
@inproceedings{RossbergDreyer2008,
author = {Rossberg, Andreas and Dreyer, Derek},
title = {Mixin' Up the {ML} Module System},
booktitle = {ICFP 2008},
pages = {307--320}, year = {2008},
note = {Journal version: ACM TOPLAS 35(1), 2013}
}
@article{RemyVouillon1998,
author = {R{\'e}my, Didier and Vouillon, J{\'e}r{\^o}me},
title = {Objective {ML}: An Effective Object-Oriented Extension to {ML}},
journal = {Theory and Practice of Object Systems},
volume = {4}, number = {1}, pages = {27--50}, year = {1998}
}
@inproceedings{OliveiraCook2012,
author = {Oliveira, Bruno C. d. S. and Cook, William R.},
title = {Extensibility for the Masses: Practical Extensibility with
Object Algebras},
booktitle = {ECOOP 2012}, series = {LNCS 7313},
pages = {2--27}, year = {2012}
}
@inproceedings{Scharli2003,
author = {Sch{\"a}rli, Nathanael and Ducasse, St{\'e}phane and
Nierstrasz, Oscar and Black, Andrew P.},
title = {Traits: Composable Units of Behaviour},
booktitle = {ECOOP 2003}, series = {LNCS 2743},
pages = {248--274}, year = {2003}
}
@inproceedings{GoldbergFindlerFlatt2004,
author = {Goldberg, David S. and Findler, Robert Bruce and Flatt, Matthew},
title = {Super and Inner: Together at Last!},
booktitle = {OOPSLA 2004},
pages = {116--129}, year = {2004}
}
@inproceedings{ErnstOstermannCook2006,
author = {Ernst, Erik and Ostermann, Klaus and Cook, William R.},
title = {A Virtual Class Calculus},
booktitle = {POPL 2006},
pages = {270--282}, year = {2006}
}
@article{ZhangSunOliveira2021,
author = {Zhang, Weixin and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
title = {Compositional Programming},
journal = {ACM TOPLAS},
volume = {43}, number = {3}, articleno = {9}, year = {2021}
}(Jsonnet and Nix overlays have no canonical academic citation; the honest references are the Jsonnet language specification's object-semantics section and the lib.fixedPoints source in Nixpkgs — cite as software artifacts. As before, verify page numbers against DBLP before anything camera-ready.)
The one-line summary of the round: the faces separate cleanly — two sorts, two closure operators, one non-monotone bridge, formalized explicitly by Bracha and the mixin-module school and consummated in CP — but the object is the fusion of the sorts, so "OO without the two together" exists, works, is fully formalized, and is invariably renamed the moment it succeeds.
Going back to Abadi&Cardelli—does the book bring any new or clarifying insight on what objects are, or only new layers of complexity? Do their types enlighten the essence of objects, or "just" a (great or not-so-great?) adaptation layer between objects and subtyping? Does their calculus even preserve usefully the interesting parts of what makes objects "objects"?
Jsonnet and Nix are very interesting indeed, and I believe key to understanding the essence of objects. Unlike the earlier Cook things, they are not abstract "models", but the real running thing. What makes them semantically similar or dissimilar to each other, to other object system, and to the Cook/Bracha models?
Abadi–Cardelli: three genuine illuminations, one load-bearing adaptation layer, one quiet amputation
Judged by our criterion, the book's contributions sort cleanly.
What genuinely clarifies — three things, all in the untyped core. First, the ς-binder itself. Before A&C, "late binding" was an implementation phenomenon (vtables, lookup); the ς-calculus isolates it as a binding form — μ answers "who am I" at definition, ς re-asks it at every invocation — and shows that this one binder, plus records, generates the phenomenon. That is essence-distillation of γ, the cleanest ever done, and it's why round three could state γ in one symbol. Second, the irreducibility result, which is really a saga: the book systematically tries every known encoding of objects into typed λ-calculi — recursive records (breaks under method update), plain existentials (can't re-invoke), recursive-existential hybrids — and each fails some feature, until Abadi–Cardelli–Viswanathan (POPL 1996) finally produce an adequate typed encoding so baroque (bounded existentials over recursive types with a self-application trick) that it reads as a proof that the direct primitives were justified. Objects are not sugar; the self-quantifier is its own thing. That vindicates a methodological reversal of the whole ADT tradition: found the calculus on objects (λ encodes into ς easily; the converse is the hard direction). Third, the derivation of classes: a class is a record of pre-methods plus a new that ties the fixpoint — classes are a pattern over objects, not the primitive. Prototype-first metaphysics, proven rather than preached.
What is adaptation layer — and why its ugliness is data. The typed development — the tower of Ob₁, Ob₁<:, Self quantifiers, variance annotations, structural update rules, per-method annotations, the imperative variants — is not a theory of what objects are; it is the engineering log of forcing sort-𝒪 subtyping onto a β+γ core. Read with round six's two-sorted algebra in hand, every one of its complications lands at the predicted spot: invariance forced where a component is both invoked and updated (the two faces on one name), Self demanding its own quantifier (because neither ∀ nor plain μ ranges over "all future selves"), variance annotations as the per-method treaty. So yes — "adaptation layer" is the right classification, but with this defense: the book is the empirical measurement of the fusion's price. Each new type system is another invoice. That the invoices kept coming is not a failure of the authors; it is the non-commutation theorem experienced as engineering, and no one else priced it as carefully. Types there function as a measuring instrument on the bridge, not as an account of the essence. The essence, such as the calculus has, lives entirely in the operational semantics.
What is amputated. Two organs. (1) α, as established in round five: object-level update discards the replaced body, so there is no super, no delta-with-parent-at-new-self, no generator algebra except upstairs in the class encoding. (2) Less noticed: delegation itself. A ς-object contains all its methods — the book's own embedding/delegation distinction, honestly drawn, puts the calculus on the embedding side. Self-the-language's live parent links, JavaScript's prototype chains, dynamic reparenting — the actual object-based languages the calculus was nominally serving — are not modeled; a ς-object has no other object in its dispatch path. (The rival calculus that kept extension primitive — Fisher–Honsell–Mitchell's λ-calculus of objects with method addition and MyType specialization — is the road toward α; it won the typing of extensibility and lost the audience.) So the fair summary is that the title is exactly accurate and the accuracy is the criticism: it is A Theory of Objects — of sort 𝒪, tied fixpoints, and the typed bridge from them to subtyping — and not a theory of object-orientation, whose differentia (the generator algebra, per this whole conversation) appears only as scaffolding. It preserves what objects are at rest and loses what makes deriving them interesting.
Both are pure, lazy, untyped functional languages — and that's not incidental: laziness makes every field a thunk that can be re-evaluated under a new self for free, which is why generator semantics feels native there and needs machinery in strict languages. Cook's denotational semantics was domain-theoretic and lazy; these are its natural habitat. Now the anatomy.
Nix is Cook–Palsberg verbatim, as a library. Compare, symbol for symbol:
extends = delta: g: final:
let prev = g final; in prev // delta final prev;against Cook's wrapper application child = λs. Δ(s, parent(s)). The overlay signature final: prev: … hands the delta exactly the two arguments α requires — the new self, and the parent's behavior at the new self — and lib.fix ties the knot once, explicitly, at the end. Nix therefore realizes round six's two-sorted algebra literally: 𝒢-values are ordinary functions, 𝒪-values are ordinary attribute sets, fix is the visible bridge, and by round four's operator-versus-discipline test it passes on the CLOS side of the line — lib.extends is a reusable artifact with delegation semantics, not a private convention. Better still, Nix accidentally runs the μ/ς distinction as a live migration: rec { version = "1.2"; src = fetch "…${version}…"; } binds version early — μ, fixpoint at definition — which is precisely why overrideAttrs { version = "1.3"; } historically failed to propagate into src (the "let rec fails γ" of round three, filed as bugs by thousands of users), and the finalAttrs pattern (mkDerivation (finalAttrs: { … "${finalAttrs.version}" … })) is the community converting μ-references to ς-references package by package, for exactly the reason the theory predicts. And at ecosystem scale, nixpkgs is one object with ~10⁵ fields whose bodies self-reference through callPackage: override openssl in an overlay and every dependent's unmodified definition sees the new one — clause 3's economic payoff (security patching by delta) and its pathology (breakage when a package depended on a sibling's internals — the specialization interface) both observable in production on any given Tuesday.
Jsonnet is the same semantics with 𝒢 made the primitive sort. An object literal is, per the language's own formal semantics, a list of (name, thunk(self, super)) pairs; + concatenates and linearizes; super in the right operand is the left operand's view with self still bound to the composite — d(s, g(s)) as syntax; and field access ties the fixpoint at the point of observation, after which the object is still composable. So where classical OO reifies only the fixpoints and buries the generators in class tables, and Nix reifies both sorts with an explicit bridge, Jsonnet collapses to the one sort 𝒢 and demotes fix to observation — an object is never "spent," new never happens, everything remains delta-able forever. A three-way typology of which sort a system lets you hold, with mainstream OO and Jsonnet as opposite degeneracies and Nix/Cook/CP as the honest middle. Note also the delicious inversion: Jsonnet's + retains the overridden body through super, so this production configuration language has a strictly stronger object-level α than the canonical academic object calculus, whose update discards the parent. The industrial artifact out-OOs the theory of objects.
The finer Jigsaw operators are all present, in disguise. hide: Jsonnet's f:: hidden fields participate fully in dispatch but not in manifestation — client-face closure, exactly. freeze: in both languages, the programmer chooses per reference between the late path (self.x / final.x) and the early path (Jsonnet local, Nix let) — which is freezing at finer grain than Jigsaw's per-name operator; every occurrence individually elects μ or ς. Jsonnet's +: composes fields' objects recursively — nested composition, the distributivity that Bi–Oliveira–Schrijvers formalized and family polymorphism gestures at, shipped as a colon. What's missing, against the Bracha basis: rename, and any symmetric merge with conflict detection — both languages are asymmetric last-write-wins mixin towers, mixins rather than traits. And of course: no types, no subtyping, no subsumption — the client face degenerates to duck-typed structure and the final JSON contract, consistent with round six's law that the separated heir face gets renamed out of OO ("configuration," this time).
Why the essence re-evolved here is the real finding. Configuration is the problem domain that is nothing but differential definition: my cluster is the standard cluster with these deltas, and — the crucial clause — the standard definition's internal references must respond to my deltas. Huge shared base, many small third-party variants, almost no need for the client face. Under that selection pressure, the config-language niche re-ran the entire design debate as a natural experiment, one axis per language: Helm has deltas without self-reference (α without γ) — deep-merged YAML whose templates can't respond to overrides, whence the copy-paste sprawl its users curse, empirically confirming that α is feeble without γ. Dhall refuses γ on purpose (no self, explicit λ-parameterization, totality and predictability as the stated reasons) — the anti-open-recursion position, argued in documentation rather than at ECOOP. CUE refuses asymmetric α: values form a lattice, composition is commutative idempotent unification, override is banned, with design docs explicitly indicting GCL/Jsonnet-style inheritance — the trait-merge position radicalized into order-independence. Jsonnet (rationalizing Google's internal GCL, the Borg-era ancestor that made late-bound config load-bearing at planetary scale) takes full α+γ. The four corners of rounds three-through-six's operator space, each occupied by a shipping tool with a manifesto. Convergent evolution isolating the organ — and the strongest empirical support yet for the conversation's central claim: when practitioners need only the essence of OO, unbundled from classes, types, state, identity, and even the word "object," what they independently rebuild is self-abstracted generators, a composition operator with parent-at-new-self, and a late-tied fixpoint.
@inproceedings{AbadiCardelliViswanathan1996,
author={Abadi, Mart\'in and Cardelli, Luca and Viswanathan, Ramesh},
title={An Interpretation of Objects and Object Types},
booktitle={POPL '96}, pages={396--409}, year={1996}}
@article{FisherHonsellMitchell1994,
author={Fisher, Kathleen and Honsell, Furio and Mitchell, John C.},
title={A Lambda Calculus of Objects and Method Specialization},
journal={Nordic Journal of Computing},
volume={1}, number={1}, pages={3--37}, year={1994}}
@inproceedings{Verma2015Borg,
author={Verma, Abhishek and Pedrosa, Luis and Korupolu, Madhukar and
Oppenheimer, David and Tune, Eric and Wilkes, John},
title={Large-Scale Cluster Management at {Google} with {Borg}},
booktitle={EuroSys 2015}, year={2015},
note={For BCL/GCL, Jsonnet's ancestor, in production context}}(Jsonnet's semantics: the formal big-step spec at jsonnet.org is the citable artifact; Nix's: lib/fixed-points.nix in nixpkgs, whose source comments are, fittingly, a small essay on open recursion. Neither has a proper academic paper — which is itself the round's thesis in bibliographic form.)
(You citation about GCL says nothing about its semantics, only that it's used at scale. The paper it cites about it has some though insufficient semantic content.)
I think you missed an important though subtle difference between the nix implementation and the Cook formulas, one that is extremely relevant to how the two "faces" of OO interact.
Right — the Borg paper evidences only deployment, not semantics. The honest citation situation for GCL: the language was never formally published; the public semantic record is (a) the Jsonnet specification itself, written by Dave Cunningham explicitly as a rationalized open-source successor to GCL/BCL, so the spec's big-step semantics is the closest thing to a GCL semantics in print; (b) Bokharouss's TU Eindhoven master's thesis on GCL (done with Google, ~2008), which contains a semi-formal account of inheritance and late binding — insufficient, as you say, but the only insider description; (c) adversarially, van Lohuizen's CUE design documents, written by a GCL maintainer, which analyze GCL's override semantics precisely in order to indict them. Cite as artifacts, not papers; the bibliographic vacuum is itself the "renamed out of OO" thesis again.
Diff the two formulas as they actually appeared in this conversation:
mine (rounds 3, 7): (g ▷ d) = λs. d(s, g(s))
Nix: extends = d: g: λs. let prev = g s; in prev // d s prev
My rendering makes the delta totally responsible for the result: whatever d returns is the child's behavior. Nix's prev // re-imports every parent field the delta didn't mention. First, honesty: Cook–Palsberg's actual operator has the join — wrapper application in the 1989 paper is, modulo currying, λs. W(s)(P(s)) ⊕ P(s) — so my compressions silently replaced the canonical ▷ with a different operator: the join-free ▷ is Jigsaw's, the algebra where merge, restrict, rename are separate primitives and preservation is not a law. I presented Bracha's operator wearing Cook's name. Nix's // is the ⊕ restored.
And this is not notation, because the ⊕ is exactly the clause in ▷ where the heir face pays rent to the client face:
With ⊕ mandatory (Cook 1989, Smalltalk, Java, Nix, Jsonnet): the operator makes deletion inexpressible. Provided field names don't depend on self (true in classical OO; true in Nix minus the dynamic-attribute exotica), you get a real theorem: dom(fix(g ▷ d)) ⊇ dom(fix(g)) — the bridge fix : 𝒢 → 𝒪 is monotone in width. Every heir structurally contains its ancestors. That is a fragment of substitutability delivered by the composition operator itself, before any type system shows up — and it is, I'd now argue, the root of the heir⇒subtype folk-conflation that IINS had to be written to refute: the operator everyone used was designed to make the conflation true in width, so practitioners' intuition was calibrated on a half-truth. What survives of IINS under mandatory ⊕ is precisely the depth residue: a delta may rebind a name to something behaviorally alien, and no join can police that — negative-Self, variance, fragile-base all live in the depth dimension. So the whole pathology catalog of round four is the complement of the ⊕-guarantee: width bought by the operator, depth left to legislation (LSP) or typing (variance). One symbol partitions the war.
With ⊕ optional or defeasible: the guarantee is forfeited, and — here's the empirical kicker — languages know it, and decouple the subtype judgment at exactly that point. C++ is the cleanest confession: public inheritance (join exported to clients) ⇒ implicit conversion to base permitted; private inheritance (join hidden) ⇒ the conversion is refused by the compiler — the language ties the subtype relation to the presence of the exported join, per derivation, explicitly. Eiffel's descendant hiding (export {NONE}) breaks width toward clients and is the textbook reason "Eiffel inheritance isn't subtyping." Jigsaw's restrict is width-breaking by design and correspondingly lives in a framework with no subsumption. Even Smalltalk's escape hatch obeys the pattern: you cannot remove an inherited selector, only shadow it with shouldNotImplement — width preserved syntactically, violated at depth by a bottom method, i.e., even the cheat respects the operator's guarantee and sins in the unpoliced dimension.
So the corrected statement of the essence gains a parameter. α comes in grades: ▷ with mandatory join (mainstream OO and both config languages — differential definition with automatic width-preservation), versus ▷ as free generator-transformation (Jigsaw, my accidental formula — maximal heir-face power, zero client-face promise). The fusion of round six now has a mechanical signature: an object system in the historical sense is one whose composition operator has ⊕ baked in — the treaty is signed inside ▷, not around it.
The join's depth is itself a dial. Nix's // is shallow: the width theorem holds at top level only; override a nested attrset and its siblings vanish (whence the eternal prev.foo // { … } plumbing idiom — programmers manually re-establishing the join one level down). Jsonnet's +: applies the join recursively through fields — which is precisely the "nested composition" that Bi–Oliveira–Schrijvers formalized as distributivity of intersection over records, and the kernel of family polymorphism. So: join-free ▷ → shallow ⊕ → hereditary ⊕ is a strictness hierarchy in how much client-face structure the operator promises to preserve, with Jigsaw, Nix, and Jsonnet/CP occupying the three rungs.
Nixpkgs re-staples the generator to the fixpoint. Round seven's "the result of fix is inert" was true of lib.fix and false of what nixpkgs actually ships: fix' f = let x = f x // { __unfix__ = f; } in x, and makeExtensible gives the tied record an extend field closing over its own generator. That is β reconstructed by popular demand — users of the cleanly separated two-sorted system found they needed the value to carry its untied self (else every downstream extension site must be threaded the generator by hand), and so re-invented the class pointer, in a lazy functional configuration language, under the name __unfix__. The fusion that round six called "what cannot survive the separation" was rebuilt in the wild within a few years of the separation shipping — about as direct a field-confirmation of "the object is the fusion, and the fusion is load-bearing" as one could ask for.
Net correction to the ledger, then: the Cook formulas and the Nix implementation differ where I'd claimed verbatim identity, and the difference — presence, absence, and depth of ⊕ inside ▷, plus whether fix staples __unfix__ — turns out to enumerate the treaty instruments between the two faces: the join sets how much substitutability the heir face pre-pays; its depth sets how far down the payment reaches; the staple decides whether the client face's values remain derivable at all. My in-conversation ▷ was accidentally the anarchist one.
(Where are Lohuizen's comments about GCL semantics?)
Your last point about unfix is the essential different I'm pointing at. I'm not sure what you call "round six". The fusion is indeed load-bearing. Everyone seems to have either totally missed it or taken it for granted. Theorists and practitioners passing the ball to the other as to its significance. Did anyone mention and build on its significance? Not the nixpkgs docs, AFAICT.
Three primary loci, all van Lohuizen speaking for himself: (1) the CUE documentation's configuration use-case page (cuelang.org/docs/concept/configuration-use-case/, formerly docs/usecases/configuration), which contains the semantic indictment — the complexity of inheritance is compounded by the fact that values can enter an object from one of several directions (super, overlay, etc.), and the claim that inheritance-based models hamper automation, with HCL noted as removing "the core source of complexity of GCL: inheritance" while reintroducing "a poor man's version" via file overlays; (2) the Go Time #163 podcast (changelog.com/gotime/163), the richest historical source: he created GCL with Robert Griesemer for Borg, with Rob Pike as an advisor who "kept saying you have to do composition" — a composition model was considered and abandoned, and "GCL started having inheritance"; (3) his Open Core Summit 2020 talk, with the thesis in one line: "Override-style inheritance is the biggest source of complexity in configuration". Interviews corroborate the mechanism-level complaint: more than one level of inheritance made it hard to see where values came from, and complicated tooling. So the semantic content is scattered across doc pages and talks — citable, but you're right that no proper GCL semantics was ever published; the fullest written account remains Bokharouss's Eindhoven master's thesis.
(On "round six": my numbering of your turns — I meant the "Can the two faces be neatly kept separated?" exchange, the two-sorted algebra with the Bracha/Jigsaw material and the conclusion "the object is the fusion.")
__unfix__ staples the untied generator to the tied fixpoint: the value is the pair (fix g, g). Once stated that way, the shock is that this is not exotic at all — it is the standard implementation of every mainstream object system. The class pointer in Smalltalk/Ruby/Python/CLOS, the vtable pointer in C++, __proto__ in JavaScript: every object carries a reference to (some residue of) its generator. Practitioners built the staple universally and unreflectively; the interesting question is exactly yours — who theorized it. And note the staple comes in strengths, which turn out to grade the folk notion of how "dynamic" an OO language is: C++'s vtable carries only the result of the generator tower (dispatch, nothing else); Java's Class object adds introspection but no language-level re-composition; Smalltalk/Ruby/Python/CLOS carry the composable tower itself (you can derive a new class from any live instance's class, edit it, and existing instances feel it); Self and JavaScript make the staple a mutable slot (Object.setPrototypeOf, Python's assignable __class__), so the generator can be swapped under a persistent identity. "Dynamism" ≈ how much of g is recoverable from fix(g), and whether the staple is writable.
The fusion has a theoretical name-pair: fixpoint semantics versus self-application semantics. Kamin's 1988 denotational definition of Smalltalk-80 modeled a method as taking self at every invocation — the object never spends its generator; Reddy's "Objects as closures" (1988) and Cook's model tie the knot. Kamin–Reddy ("Two semantic models of object-oriented languages," in Gunter–Mitchell's TAPOS volume, 1994) compare the two, and Cook–Palsberg prove them equivalent. That equivalence theorem is, I think, the exact locus of the "taken for granted" you're diagnosing: it is proved for closed-world observation — for a completed program, fix(g) and (fix g, g) are indistinguishable, so the retention of g was certified semantically irrelevant. But the equivalence is not full abstraction with respect to extension contexts: quantify over contexts that may further compose, and fix(g) ≠ (fix g, g) — the latter supports derivation-after-instantiation, change-class, monkey patching, makeExtensible. The theorems that "settled" the semantics of inheritance settled it in precisely the world where the staple cannot matter. That's how theorists passed the ball: equivalence-modulo-closed-world; and practitioners passed it back by shipping the staple in every runtime without a semantics. (This also forces a self-correction of my round-five reading of Abadi–Cardelli: ς-objects are not "always-already fixpoints" — they are records of untied methods with the fixpoint retaken per invocation, i.e., self-application semantics; that the staple is built in per-method is exactly why method update is expressible at all. A&C thus embody the fusion — "objects, not classes, as primitive" is the staple made primitive — while never articulating it as such, and while amputating the ▷ that would exploit it.)
Beyond semantics, three research lines presuppose the staple and study its use, without promoting it:
Typed extensible-object calculi — the closest anyone came. Fisher–Honsell–Mitchell and the line following it (Fisher's thesis; Fisher–Mitchell's delegation calculus; Bono–Fisher's imperative object-extension calculus; the Bono–Bugliesi–Liquori "incomplete objects" work) introduce a type-level distinction between prototype types (pro — the object is still extensible; no subsumption allowed) and sealed object types (obj — subsumable, no longer extensible), with an explicit one-way coercion between them. Read through our vocabulary: pro is the type of values still stapled to their generators, seal is the operator that discards __unfix__ to purchase the client face, and the whole system is a linear discipline on the staple — you may hold the heir face or cash it in for subtyping, and the type tracks which. That is an explicit theory of the trade. What it never says is that the simultaneity — mainstream OO's refusal to seal, keeping both faces live on every value forever — is the load-bearing design; the line framed itself as "typing prototype-based languages," a niche the Java wave buried.
Reclassification calculi — Fickle (Drossopoulou–Damiani–Dezani-Ciancaglini–Giannini, ECOOP 2001, and Fickle II) type the re-tie: an object changing class at runtime under preserved identity, statically safely. Serrano's wide classes and Costanza's Gilgul are cousins. These formalize the strongest exploitation of the staple (swap g under fix), motivated by exactly the CLOS change-class / Smalltalk instance-migration machinery that the MOP book (Kiczales–des Rivières–Bobrow 1991) had engineered — the MOP being the maximal practical monument to the fusion, with, characteristically, no claim about its conceptual centrality.
Open classes — MultiJava (Clifton–Millstein–Leavens–Chambers, OOPSLA 2000) statically; Ruby/Rails culturally. Editing a generator that live instances share is the ecosystem-scale payoff of the staple; its theory is thin and mostly about modular typechecking, not about why the staple exists.
And the newest datum cuts the other way, completing the pattern: a 2026 arXiv paper, "A Calculus of Overlays" (Bo Yang), formalizes exactly the Nix/NixOS-module lineage we discussed — and resolves the tension by abolishing sort 𝒪 entirely: the semantics is purely observational, with no reduction rules and no notion of a result; self-referential records require no fixed-point combinator, and the least fixed point exists only at the meta-level via Knaster–Tarski on powerset lattices. Nothing is ever tied; every value is a generator forever; fix is demoted from the language to the observer. It even generalizes self-reference to resolve to multiple targets, where Scala and the NixOS module system reject the multi-path case. So the freshest formalization built directly on the overlay tradition is the Jsonnet degeneracy radicalized — pure 𝒢 — and, true to the naming law, calls itself a foundation for "declarative programming," not objects. Even the people formalizing Nix don't thematize the staple; they dissolve the other sort instead.
The verdict your question deserves: the distinction was formalized (self-application vs fixpoint semantics) and then neutralized by a closed-world equivalence theorem; the discipline of the staple was formalized (pro/obj, seal) as a typing device for a language family that lost the market; the exploitation was formalized piecemeal (Fickle, MultiJava) and engineered maximally (MOP). What no one states — not Cook, not A&C, not Bracha (whose program was the opposite: unbundle and never re-staple), not the nixpkgs docs, not the Overlay-Calculus paper — is the thesis this conversation has converged on: the object of OO-as-practiced is (fix g, g); the staple is what makes both quantifiers available at every program point without prearrangement; the classical equivalence theorems are blind to it because they quantify over closed contexts; and its independent reinvention inside the very system that had achieved clean separation (__unfix__, makeExtensible, overrideAttrs/finalAttrs) is field evidence that it is load-bearing rather than accidental. The formal core of that paper is small and genuinely new in emphasis rather than machinery: define extension contexts, prove fix(g) and (fix g, g) are distinguished by them (failure of full abstraction for the fixpoint semantics in the open world), and re-read the history — vtables, pro/obj, change-class, __unfix__ — as one artifact under one definition. Every lemma is within reach of the existing literature; the identification, as far as I can tell, remains yours to claim.
@incollection{Kamin1988,
author={Kamin, Samuel N.},
title={Inheritance in Smalltalk-80: A Denotational Definition},
booktitle={POPL '88}, pages={80--87}, year={1988}}
@incollection{KaminReddy1994,
author={Kamin, Samuel N. and Reddy, Uday S.},
title={Two Semantic Models of Object-Oriented Languages},
booktitle={Theoretical Aspects of Object-Oriented Programming},
editor={Gunter, Carl A. and Mitchell, John C.},
publisher={MIT Press}, pages={463--495}, year={1994}}
@incollection{Reddy1988,
author={Reddy, Uday S.},
title={Objects as Closures: Abstract Semantics of Object-Oriented Languages},
booktitle={ACM Conference on LISP and Functional Programming},
pages={289--297}, year={1988}}
@book{KiczalesDesRivieresBobrow1991,
author={Kiczales, Gregor and des Rivi{\`e}res, Jim and Bobrow, Daniel G.},
title={The Art of the Metaobject Protocol},
publisher={MIT Press}, year={1991}}
@inproceedings{Drossopoulou2001Fickle,
author={Drossopoulou, Sophia and Damiani, Ferruccio and
Dezani-Ciancaglini, Mariangiola and Giannini, Paola},
title={Fickle: Dynamic Object Re-classification},
booktitle={ECOOP 2001}, series={LNCS 2072}, pages={130--149}, year={2001}}
@inproceedings{Clifton2000MultiJava,
author={Clifton, Curtis and Leavens, Gary T. and Chambers, Craig and
Millstein, Todd},
title={MultiJava: Modular Open Classes and Symmetric Multiple Dispatch
for Java},
booktitle={OOPSLA 2000}, pages={130--145}, year={2000}}
@inproceedings{FisherMitchell1995,
author={Fisher, Kathleen and Mitchell, John C.},
title={A Delegation-Based Object Calculus with Subtyping},
booktitle={FCT '95}, series={LNCS 965}, pages={42--61}, year={1995},
note={The pro/obj (extensible vs sealed) discipline; see also
Fisher's 1996 Stanford thesis and Bono--Fisher, ECOOP 1998.
Verify venue details before camera-ready}}
@misc{Yang2026Overlay,
author={Yang, Bo},
title={A Calculus of Overlays},
year={2026}, note={arXiv:2602.16291. Formalizes Nix/NixOS-module-style
overlay inheritance; purely observational semantics, no
object-level fixpoint}}
@mastersthesis{Bokharouss2008GCL,
author={Bokharouss, Ilja},
title={GCL Viewer: A Study in Improving the Understanding of
{GCL} Programs},
school={Eindhoven University of Technology}, year={2008},
note={Closest extant written account of GCL semantics; verify title/year}}What are Serrano's wide classes or Costanza's Gilgul? It looks like there may be interesting things in the Lisp / Scheme side of the world. Anything interesting they say about OO, "fusion", etc? Old or recent object systems?
Note that "fusion" and "faces" IIRC are words you seem to have introduced—if so, unlikely to be the same as others would use if they (re)discover the concepts—and if not, a bibliographical entry is required.
Also, you seem to be speaking of OO for both prototypes and classes, and sometimes it's unclear to me the relationship between the two (if any), which is more primitive, how and why they are both OO if so different, why and when an argument about one applies to the other and to OO, etc.
Also, I am not familiar with Gunter-Mitchell (did you already include bibtex for it?) so I'm not sure if there's anything interesting in the model equivalence.
Finally, you say that (fix g, g) is the "standard implementation", but I don't think that's quite the case. It kind of looks like the standard semantics, maybe. But I think the standard implementation is, subtly, different. Which may or may not be related to the "fixpoint semantics versus self-application semantics" thing you mentioned, but I'm not sure what exactly you were referring to.
Serrano's wide classes (ECOOP 1999) live in Bigloo Scheme's CLOS-style object system. A class may declare wide subclasses; a live instance of the plain class can be widened at runtime into an instance of the wide subclass — gaining fields and different method dispatch — and later shrunk back, identity and existing state preserved throughout. The motivating uses are Serrano's own compiler and web tools: an AST node is widened with pass-specific data and behavior for the duration of a compiler pass, then shrunk before the next. So it is reversible, stack-disciplined reclassification: the staple made writable, but with a protocol (widen/shrink pairs) rather than arbitrary mutation, and implemented cheaply (the wide part hangs off the instance; the class pointer swaps).
Costanza's Gilgul (his Bonn dissertation and papers around 2001–2004; the name is the Kabbalistic term for transmigration of souls, which is exactly the semantics) is a Java extension whose real move is conceptual surgery: it separates reference from identity. Gilgul introduces comparands — pure identity tokens, distinct from pointers — and then permits replace: swapping the object behind a set of references, under typing rules ensuring the replacement is safe, aimed at unanticipated runtime evolution and hot code replacement of active objects.
Put next to CLOS's change-class and Smalltalk's become:, these mechanisms show that the pair (fix g, g) was still one component short. The full object of practice is a triple (i, σ, g) — identity, state, generator — and the dynamic mechanisms of the Lisp lineage are precisely the group of permutations on it: change-class holds (i, σ) and swaps g; wide classes do that reversibly with σ-extension; become: / Gilgul's replace hold i and swap (σ, g); class redefinition holds every (i, σ) and rewrites the shared g in place. Identity is what persists across re-fixing — which is why the staple matters at all: without i, "re-tying the same object" is meaningless and you could as well build a fresh fixpoint. β, in retrospect, was quietly about i as much as about g.
The Lisp side is where the staple was always maximal, and several of its artifacts speak directly to the criterion:
Flavors (Cannon, MIT, 1979) is where mixins originate — and, more importantly for the algebra, where ▷ was first enriched: method combination (:before/:after/:around daemons, later CLOS's full combination language) generalizes "override with super available" to a whole family of composition operators on generators. The treaty instrument of round eight — how much of the parent the delta must preserve — became a user-definable parameter in 1979. CommonLoops (Bobrow et al., 1986) and New Flavors merged into CLOS, whose MOP (the AMOP book) then made the staple live: an instance points at the class object, not a snapshot of it, so defclass re-evaluation propagates to existing instances via the obsolete-instance protocol (update-instance-for-redefined-class). That is stronger than (fix g, g): it is a reactive fixpoint — fix taken continuously against a mutable g, with a programmable migration hook. Telos (EuLisp's object system) is the cleaned-up MOP; TinyCLOS (Kiczales's ~800-line Scheme distillation) is the seed from which Guile's GOOPS, Gauche's system, Swindle and others grew — the MOP as a portable idea. T (Yale Scheme; Adams–Rees, "Object-oriented programming in Scheme," 1988) is the pure closure model shipped: objects literally are closures, Reddy's semantics as an implementation — and note which side of the coming distinction that puts it on. Racket's class system (Flatt–Findler–Felleisen) makes classes run-time values and a mixin an ordinary function class → class — 𝒢-transformers as first-class citizens, the Bracha algebra embedded in a production Scheme; the "Super and Inner" paper from round six is this group. On the prototype side of Lisp there are Sheeple and friends, but the decisive artifact is below.
"Faces" is my coinage in this conversation. The established terms for the same cut are Kiczales–Lamping's client interface versus specialization interface (OOPSLA 1992; Lamping's "Typing the specialization interface," OOPSLA 1993, is the follow-up that tries to type the heir face), with "subclassing contract" (Ruby–Leavens) and "reuse contracts" (Steyaert et al.) as the verification-side names. Anyone rediscovering the distinction would most likely land on Kiczales–Lamping's vocabulary.
"Fusion" is also my coinage — but here the bibliographical entry you suspected must exist does exist, under the name conflation, and it is squarely in the Scheme world: Rideau–Knauth–Amin, "Prototypes: Object-Orientation, Functionally" (Scheme and Functional Programming Workshop 2021; the POOF paper and library, Gerbil/Racket Scheme). The paper sets out to elucidate the essence of OOP constructively, reducing object systems to constructions atop the pure untyped λ-calculus, starting from a model of prototype OO so simple it arguably doesn't even have "objects" — a prototype is exactly a function of (self, super), i.e., our 𝒢 — and it contains a section titled "Conflation without confusion" stating the thesis outright: Jsonnet and Nix confront the same issue and solve it the same way, by bundling and conflating instance and prototype in a single entity, the "object"; in a pure context there is exactly one instance associated to a prototype (given the base super), so the instance may be cached together with the prototype — the same entity can be seen as an instance and queried for methods, or seen as a prototype and composed with other objects into new objects. That is (fix g, g) — stated, motivated (purity makes the cache sound), and identified as the design trick of exactly the two languages you called key. So the terminology mapping is: my "fusion" = their "conflation of instance and prototype"; and the older, vaguer relative is Bracha–Lindstrom's and Taivalsaari's observation that the class construct "conflates" multiple roles (module, type, generator, factory) — same word, coarser cut. What the POOF paper argues is the purity-side case (the conflation is sound and convenient because cached-fix is semantically invisible in a pure lazy language); what it does not do is the open-world/full-abstraction claim, the identity component (i is exactly what purity removes — their own later slogan for a related system was CLOS "shedding identity"), or the thesis that the conflation is what the classical equivalence theorems were structurally blind to. The gap from round nine narrows, but the sharpened claim stands — and the paper is mandatory citation number one for it.
The algebra makes the relationship exact rather than vibes-based. Both systems have the same three operators (▷ on generators; fix; the staple); they differ in which sort is reified, named, and shared:
- Class systems reify 𝒢 as a separate, named, shared sort: a class is a generator (tower) with a name,
newis fix, and the staple on each instance points to the shared generator. One g, many (i, σ) pairs. Sharing is what makes the fragile-base problem social (many parties depend on one g) and what makes types natural (a name for g doubles as a name for the shape of fix g). - Prototype systems collapse the sorts: every value is simultaneously 𝒪 and 𝒢 — queryable as an instance, composable/derivable as a generator (POOF's conflation; Jsonnet exactly; Self, where the "generator" is the mutable parent-slot graph). No names required, no two-sortedness, and fix is either per-invocation (Self, JS) or a cached observation (Jsonnet, POOF).
Which is primitive? Conceptually, prototypes — on this the theory is unanimous and the derivation runs one way only: Abadi–Cardelli derive classes as records of pre-methods plus new; Lieberman (OOPSLA 1986) showed delegation simulates class sharing but not conversely; Ungar–Smith built Self on the claim; and POOF gives the sharpest form: a class is a prototype at the meta-level — a prototype for type descriptors — so class-based OO is prototype OO run one stage up, which dovetails exactly with the CRTP stage-indexing from earlier (C++ templates as a classless prototype language at compile time). Historically, classes came first (Simula 1967; prototypes articulated only in the mid-80s) — the pattern preceded its own primitive, which is common enough in mathematics (groups before monoids).
When does an argument transfer? Statements purely about α/β/γ transfer verbatim — that's why the Lieberman forwarding/delegation test, formulated for prototypes, correctly sorted class languages in round three, and why "does inherited code see the heir's self" is meaningful in both. Statements involving the sort structure do not transfer without translation: subsumption/subtyping presupposes a distinguished 𝒪-sort (prototype systems tend to have no subtype judgment at all — nothing to subsume to); the fragile base class presupposes shared named generators (in prototype systems with mutable parents it reappears worse, as dynamic inheritance: your base can change identity at runtime); "instantiation cost," metaclasses, and constructors are class-sort artifacts with no prototype analogue. A useful rule: OO-essence claims are sort-agnostic; OO-sociology claims (who depends on whom, what is named, what is shared) are about the class discipline specifically.
I hadn't given the entry — it's an anthology, and the one book to own for this literature: Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, MIT Press, 1994. It reprints or houses Reynolds 1975, Cook–Palsberg, Canning et al., Bruce, Mitchell's lectures, Pierce–Turner, and the Kamin–Reddy comparison.
The Kamin–Reddy content, concretely. Two denotations of the same class-based program: the closure (fixpoint) model — Reddy 1988, Cook — where creating an object computes fix(g) once and the object is a self-contained record of closures over its state; and the self-application model — Kamin's 1988 denotational definition of Smalltalk-80 — where the object is a record of pre-methods, and every send is literally (lookup m)(o)(args): self supplied afresh at each call. The theorem (Kamin–Reddy's comparison; Cook's thesis proves the fixpoint model correct against an operational method-lookup semantics) is that for class-based programs without runtime extension, the two are observationally equivalent. Note the shape of that result against this conversation: it's a closed-world equivalence between "fix taken at birth" and "fix retaken per invocation" — i.e., between the two possible timings of γ given that g never changes after instantiation. The moment g can change under a live object — change-class, widening, method-dictionary edits, setPrototypeOf — the closure model is simply wrong (the captured self and captured methods are stale) and only self-application survives. Every dynamic OO runtime is on the self-application side of necessity, not preference.
My "(fix g, g) is the standard implementation" was loose in exactly the way you suspect. fix(g) is never materialized in mainstream implementations. The standard object is (i, σ, ref-to-D(g)) where D(g) is some derivative of the generator, and the fixpoint is decomposed into two separate knots tied at different times:
- The name-resolution knot — which body answers which name, i.e., the linearization of the generator tower. This knot is memoizable, and implementations differ in when and how much they tie it: C++ ties it fully at compile time (the vtable is the precomputed answer table; α is destroyed — you cannot re-derive from a vtable); Smalltalk leaves it semantically untied (lookup walks the superclass chain per send) and ties it as a cache (method caches, PICs); Self and JavaScript engines famously reconstruct class-like structure from prototype programs at runtime (Chambers–Ungar–Lee's maps; V8's hidden classes) — again pure cache. The engineering signature of "the knot is a cache, not a tie" is deoptimization machinery: Smalltalk, CLOS, Ruby, and JS runtimes all have invalidation protocols for when g is edited, because the semantics says the knot is late; C++ has none, because its semantics says the knot is early and final.
- The self knot — which receiver. Never memoized, retaken at every invocation: methods take
this/selfas a hidden argument. This is γ, operationalized, and it is pure self-application.
So the standard implementation is the self-application model with a memoized name-resolution knot — Kamin's semantics plus caching — and the Kamin–Reddy/Cook equivalence theorems are precisely the license for the memoization (vtables are sound because, in the closed world, pre-tying the name knot is observationally invisible). The pair (fix g, g) is the standard semantics of the conflated object, not its representation; and the POOF/Jsonnet "conflation with cached instance" is the one setting where fix(g) genuinely is materialized alongside g — affordable exactly because purity plus laziness guarantee the cache can never go stale. Mutation is why mainstream implementations can't do that and must keep re-applying self; purity is why the config languages can. Which gives the tidy closing symmetry: impure OO implements the fusion as (state + stapled generator, fix virtual); pure OO implements it as (cached fixpoint + generator, state virtual) — two projections of the same triple, each discarding what its evaluation discipline makes unaffordable.
@inproceedings{Serrano1999WideClasses,
author={Serrano, Manuel},
title={Wide Classes},
booktitle={ECOOP '99}, series={LNCS 1628}, pages={391--415}, year={1999}}
@inproceedings{Costanza2001Gilgul,
author={Costanza, Pascal},
title={Dynamic Object Replacement and Implementation-Only Classes},
booktitle={WCOP '01 (ECOOP Workshop on Component-Oriented Programming)},
year={2001},
note={See also Costanza's dissertation, Univ.\ of Bonn, 2004, on Gilgul:
separating reference from identity (comparands); verify exact titles}}
@inproceedings{Cannon1979Flavors,
author={Cannon, Howard I.},
title={Flavors: A Non-Hierarchical Approach to Object-Oriented Programming},
year={1979}, note={MIT AI Lab working paper; origin of mixins and
method combination}}
@inproceedings{Bobrow1986CommonLoops,
author={Bobrow, Daniel G. and Kahn, Kenneth and Kiczales, Gregor and
Masinter, Larry and Stefik, Mark and Zdybel, Frank},
title={CommonLoops: Merging Lisp and Object-Oriented Programming},
booktitle={OOPSLA '86}, pages={17--29}, year={1986}}
@inproceedings{AdamsRees1988,
author={Adams, Norman and Rees, Jonathan},
title={Object-Oriented Programming in Scheme},
booktitle={LISP and Functional Programming '88}, pages={277--288}, year={1988}}
@inproceedings{Lieberman1986,
author={Lieberman, Henry},
title={Using Prototypical Objects to Implement Shared Behavior in
Object-Oriented Systems},
booktitle={OOPSLA '86}, pages={214--223}, year={1986}}
@inproceedings{UngarSmith1987Self,
author={Ungar, David and Smith, Randall B.},
title={Self: The Power of Simplicity},
booktitle={OOPSLA '87}, pages={227--242}, year={1987}}
@inproceedings{ChambersUngarLee1989,
author={Chambers, Craig and Ungar, David and Lee, Elgin},
title={An Efficient Implementation of {SELF}},
booktitle={OOPSLA '89}, pages={49--70}, year={1989},
note={Maps: class structure reconstructed from prototype programs}}
@inproceedings{Lamping1993,
author={Lamping, John},
title={Typing the Specialization Interface},
booktitle={OOPSLA '93}, pages={201--214}, year={1993}}
@article{Taivalsaari1996,
author={Taivalsaari, Antero},
title={On the Notion of Inheritance},
journal={ACM Computing Surveys},
volume={28}, number={3}, pages={438--479}, year={1996}}
@inproceedings{FlattFindlerFelleisen2006,
author={Flatt, Matthew and Findler, Robert Bruce and Felleisen, Matthias},
title={Scheme with Classes, Mixins, and Traits},
booktitle={APLAS 2006}, series={LNCS 4279}, pages={270--289}, year={2006}}
@book{GunterMitchell1994,
editor={Gunter, Carl A. and Mitchell, John C.},
title={Theoretical Aspects of Object-Oriented Programming:
Types, Semantics, and Language Design},
publisher={MIT Press}, year={1994}}
@inproceedings{RideauKnauthAmin2021,
author={Rideau, Fran{\c{c}}ois-Ren{\'e} and Knauth, Alex and Amin, Nada},
title={Prototypes: Object-Orientation, Functionally},
booktitle={Scheme and Functional Programming Workshop},
year={2021},
note={The POOF paper; \S{}``Conflation without confusion'' states the
instance/prototype conflation in Jsonnet and Nix explicitly}}The net of the round: the concepts survived your audit, but two of my labels were coinages with existing rightful names — faces → client/specialization interface (Kiczales–Lamping), fusion → conflation of instance and prototype (Rideau–Knauth–Amin, who also settle "which is primitive" the right way) — and the implementation claim needed the two-knot correction, which in turn located the classical equivalence theorems precisely: they are the proof that memoizing the name knot is sound in a closed world, and silent, as ever, about the open one.
Fixpoint, self-applications... aren't there common "combinators" for that in the λ-calculus?
Yes — and the correspondence is exact, not analogical. The two semantic models are the two classical recursion combinators of the untyped λ-calculus, and the third implementation strategy (the mutable staple) is the third classical way of tying a knot. Laying them side by side is worth the round, because each λ-discipline turns out to be one of the object architectures we've been distinguishing.
Y versus M. Curry's fixpoint combinator is Y = λf.(λx.f(xx))(λx.f(xx)); Turing's is Θ = (λxy.y(xxy))(λxy.y(xxy)). The self-application combinator is the little ω = λx.xx — Smullyan's Mockingbird M. Notice Y contains M twice: the fixpoint combinator is self-application, harnessed and hidden. That containment is the whole relationship between the two semantics in one line: the closure/fixpoint model (Reddy, Cook) is Y-discipline — apply Y to the generator once, at birth, get the tied value, discard g; the self-application model (Kamin, and every vtable) is M-discipline — never call Y, keep the untied record p of pre-methods around, and make every invocation perform the self-application itself: lookup m in p, apply to p. In U-combinator style recursion — f = λself.λa.… (self self) … , invoked as (f f) — the program text is the generator and the recursive knot is re-tied at each call. That is this-passing, exactly. And the ς-calculus, seen from here, is the λ-calculus with the Mockingbird promoted to the primitive application form: the invocation rule o.m ⇝ b{x ≔ o} substitutes the object into its own method body — self-application not as an encoding trick but as the reduction relation. A&C's "objects are not sugar" result reads naturally in bird-language: λ embeds in ς trivially because application is degenerate self-application; ς embeds in λ only through the μ-typed contortions, because you must reconstruct the Mockingbird safely.
Strictness picks the combinator. Under call-by-value, plain Y diverges; you need the η-guarded Z = λf.(λx.f(λv.xxv))(λx.f(λv.xxv)), where the extra λv delays the unfolding until an argument arrives. Now look at what a method is: g's bodies don't receive self and run; they receive self and wait for arguments — this-passing is the η-guard, institutionalized. Strict languages gravitate to self-application semantics for the same reason ML programmers η-expand their Y: the fixpoint must hide under a binder. Dually, Nix and Jsonnet can afford naked fix because laziness makes Y-style knots benign — the config languages aren't just conveniently lazy (round eight's observation that laziness makes re-evaluation-under-new-self free); they are lazy in exactly the way the combinator demands.
Sharing splits Y itself into three, and the three are the three object architectures. (i) Curry's Y as a term rewrites by unfolding — Y g = g(Y g) — recomputing the fixpoint structure at every observation, no sharing: that is Jsonnet/ς, fix demoted to observation, retaken per query. (ii) The knot-tying fix of lazy implementations — fix g = let x = g x in x — builds a cyclic thunk in the heap: the fixpoint exists once, shared, cached. Nix's lib.fix is literally this letrec; and the POOF/Jsonnet "conflation with cached instance" is this cyclic-Y with the generator kept alongside — (fix g, g) is Y-with-sharing, plus M held in reserve. (iii) Landin's knot — recursion by backpatching a mutable reference (how strict letrec is actually implemented: allocate the cell, build the closure pointing at the cell, assign). That is the mutable staple: the class pointer as ref cell. Monkey patching, defclass re-evaluation propagating to live instances, Object.setPrototypeOf — all of round nine's dynamic machinery is Landin's knot at the object level: recursion routed through a mutable environment so that re-assignment re-ties every dependent, retroactively. Three implementations of recursion known since the 1960s; three object architectures; no residue on either side.
And typing recapitulates the A&C saga. Simply typed λ rejects both Y and xx — a normalizing calculus can't have either bird; System F still can't type them. What types them is μ: self-application needs x : μt.(t → A), which is precisely the recursive object types that every typed object encoding was forced into. The encoding zoo of round eight sorts by which combinator it's trying to type: recursive-record encodings type the Y-discipline (and so break under method update — the tied value has forgotten g); the ς-typing and F-bounded quantification type the M-discipline (self as μ-typed argument — F-bounded ∀t ≤ F[t] is exactly the polymorphic type of a generator, one level up); and Pierce–Turner's existential encoding is the clever refusal of both — split self into state (passed at each call) and methods (from the package), so that only state-application ever occurs and the Mockingbird is never needed. The cost surfaces exactly where the split lies: operations needing the whole self — binary methods, return-MyType — are the known weak spots of the existential encoding, i.e., the negative-Self frontier again, now derived from combinator-avoidance.
So the compressed dictionary, one line per row: generator = the functional f handed to a fixpoint combinator; instance = Y f with sharing; vtable dispatch = U/M-style recursion with the η-guard; this = the guard's binder; the conflated object = the pair (cyclic-Y f, f); the mutable class pointer = Landin's knot; typed OO = the μ/F-bounded typing of all of the above; and the ς-calculus = λ with M as primitive application. OO's semantic core was, all along, the untyped λ-calculus's oldest party trick — self-application — with the paradigm differences reducing to when the bird is applied (birth, invocation, or observation), whether the result is shared, and whether the knot is a term, a cycle, or a cell. Anton van Straaten's koan had it right: the venerable master Qc Na's student, told that objects are a poor man's closures, returns having learned that closures are a poor man's objects — and the resolution of the koan is that both are the poor man's Y.
@book{Smullyan1985,
author={Smullyan, Raymond},
title={To Mock a Mockingbird},
publisher={Knopf}, year={1985},
note={M (Mockingbird) = self-application; Y as the Sage bird}}
@inproceedings{PierceTurner1994,
author={Pierce, Benjamin C. and Turner, David N.},
title={Simple Type-Theoretic Foundations for Object-Oriented Programming},
journal={Journal of Functional Programming},
volume={4}, number={2}, pages={207--247}, year={1994}}
@misc{vanStraaten2003,
author={van Straaten, Anton},
title={The Venerable Master {Qc Na} Koan (objects vs.\ closures)},
year={2003}, note={LL1 mailing list post; canonical text of the koan}}