crumbles.blog: FAQ: Why isn’t mutable a subtype of immutable, or vice versa?

crumbles.blog
computers are bad and you shouldn’t use them

/index.html
/docs.html
/about.html

FAQ: Why isn’t mutable a subtype of immutable, or vice versa?
17 September 2026

I remember the moment when I learned about immutability. It changed everything.

— Denis Defreyne

Periodically, in various programming language forums, the discussion comes up of why a certain language doesn’t provide the immutable and mutable variants of some data structure as subtypes or supertypes of one another. Now, it’s not impossible to do this, but it’s actually not formally correct to do so, and by doing so you’ll lose at least some of the type checking guarantees your language can usually make for you.
To understand why this doesn’t work, you have to remember the definition of a subtype. Namely, Liskov’s subsitution principle: a type S is a subtype of T if a value of type S can be used in every context where a value of type T is expected.
As usual when dealing with formal matters, this definition is strictly interpreted. Every really does mean every, not just most. (You might have learned the substitution principle as a mere recommended design pattern for OO classes, but formally speaking a true subtype has to fulfil this criterion.) A static type system which supports subtyping will have to prove this for you in order to pass your program through its type checker.
To illustrate this, let’s take the simplest compound data structure imaginable: the humble pair. Here are our operations on an immutable version.

(cons a d)

construct a new pair containing a and d and return it

(car p)

return the value of a provided when the pair p was constructed

(cdr p)

return the value of d provided when the pair p was constructed

That’s it!
Our mutable variant adds two new operations:

(set-car! p a)

change the value of a within the pair p

(set-cdr! p d)

change the value of d within the pair p

(And a new constructor, but we’ll deal with that below.)
Now, it should be obvious that an immutable pair can’t be provided where a mutable pair is expected. A place that needs a mutable pair will presumably try to use of these two operations on it, which aren’t defined on an immutable pair, so there will be a typing error.
But why couldn’t it be the other way around? All of the operations provided provided by an immutable pair are also provided by a mutable pair, so it seems like we should be able to use a mutable pair wherever an immutable pair is expected.
The reason is more subtle. The substitution principle extends beyond the set of operations (methods) a type provides to the implicit contract which comes with those operations.
When we take the car or cdr of an immutable pair, we can depend on a contract which says the result will always be the same every time we call it on that pair. This contract means that we can, for example, safely calculate the hash value of the pair based on its contents, store it away in another data structure, and know that it won’t be different when we recalculate it later to try to retrieve it. (In other words, immutability is a prerequisite for hash consing!)
Because of this, immutable and mutable pairs have to be completely different types:

(icons a d)

construct a new immutable pair containing a and d and return it

(icar i)

return the value of a provided when the immutable pair i was constructed

(icdr i)

return the value of d provided when the immutable pair i was constructed

(mcons a d)

construct a new mutable pair containing a and d and return it

(mcar m)

return the value of a provided when the mutable pair m was constructed

(mcdr m)

return the value of d provided when the mutable pair m was constructed

(set-mcar! m a)

change the value of a within the mutable pair m

(set-mcdr! m d)

change the value of d within the mutable pair m

It’s a typing error if an i is a mutable pair or m is an immutable pair.
Objection: But I’m not mutating it and I really don’t care about the contract of immutability for my use case
Because the two types of pair don’t form a subtype hierarchy, they have to be completely separate types and have separate sets of operations defined on them.
Fortunately, many languages offer one or another mechanism for ad hoc polymorphism, where the same operations can be defined on multiple types even if they don’t form a hierarchy. As a Schemer, I tend to think that this a bad idea in a dynamically typed context, because it makes the reasoning you have to do about the flow of data types vastly more complicated, and thus more difficult to get right. In practice, most languages do offer some mechanism for this, whether dynamically typed or statically typed.
Let’s consider the statically typed case first. Wadler and Blott introduced a mechanism for formally reasoning about ad hoc polymorphism and ensuring the type checker can actually prove it sound. In their terminology, mutable and immutable pairs are different types, but both can belong to a common pair type class whose operations are the original car and cdr we defined above. On mutable pairs, these refer to the underlying mcar and mcdr operations, and on immutable pairs to the icar and icdr operations.
This is still formally sound because the pair type class defines a new contract that says nothing about mutability. In a proper implementation of type classes, the type system will stop you trying to use the mutators in a method where the most you defined about the input type to your function is that they are some kind of pair, mutable or immutable. It won’t prevent you from using the car and cdr operations expecting them to be immutable when they might not be – but it does let you choose the granularity explicitly both ways, declaring the input type to your function as either a mutable pair or immutable pair or either, depending on the contract your function actually expects. A subtype relationship would only allow one way but not the other: you could declare your function as allowing immutable pairs, but potentially incorrectly implicitly including mutable pairs too; or, if it were the other way around, as allowing mutable pairs but potentially incorrectly including immutable ones; but one couldn’t consistently exclude either type (without violating the substitution principle).
Things akin to type classes are available in several statically typed languages, where they’re often called interfaces or traits or roles. However, real world type systems vary greatly in how strictly they enforce the checking.
In dynamically typed, object-oriented languages, this usually takes the form of duck typing where we simply define methods with the same name on multiple different types and let run-time type dispatch do the work. We can still get the benefits by adding explicit check for the presence or absence of the mutation operations before allowing a function to be called. In practice, it’s pretty unusual to do this – especially checking for the absence of mutators – and this is why ad hoc polymorphism in dynamically typed languages tends to invite problems.

Comments
Post your comment by replying to this post on Mastodon.

JavaScript is required to load comments.

Copyright (c) Daphne Preston-Kendal
CC BY-NC-ND, Site source code, Analytics

The fundamental question addressed is why mutable and immutable data structures cannot be considered subtypes of one another. This distinction hinges on the formal definition of a subtype, specifically Liskov’s substitution principle, which mandates that a value of type S must be usable in every context where a value of type T is expected, requiring a strict fulfillment of all implicit contracts.

The text illustrates this by examining a simple pair data structure. An immutable pair provides operations such as car and cdr, which return the contents, while a mutable pair includes operations to modify those contents, such as set-car! and set-cdr!. Because the operations provided by immutable pairs do not encompass the mutation operations of mutable pairs, an immutable pair cannot be substituted where a mutable pair is required, leading to a typing error.

The reasoning extends beyond the set of available operations to the implicit contract associated with those operations. Immutable operations imply a guarantee that the results remain constant, which enables specific properties like being useful for hash consing. This inherent contract is what necessitates that immutable and mutable pairs be defined as entirely separate types with distinct operations.

To allow for common operations across these types without establishing a subtype hierarchy, mechanisms akin to type classes, as introduced by Wadler and Blott, can be used in statically typed systems. These mechanisms define a common contract based on shared operations, such as car and cdr, without implying any relationship based on mutability. In a well-implemented type class system, the type checker can enforce that a function caller explicitly chooses the relevant set of operations (mutable or immutable) based on the function’s expectation, rather than allowing implicit inclusion of the other type, which would violate the substitution principle.

In contrast, dynamically typed object-oriented languages typically rely on duck typing for polymorphism. While this allows methods with the same names to exist across different types, ensuring correctness requires adding explicit checks for the presence or absence of mutation operations. The author suggests that this practical approach is often problematic in dynamically typed contexts because checking for the absence of mutators is unusual and introduces significant complexity regarding data flow reasoning. Therefore, the formal distinction between mutable and immutable concepts is maintained by ensuring they remain separate types, regardless of the polymorphism mechanisms employed.