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.

That’s it!

Our mutable variant adds two new operations:

(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:

It’s a typing error if an i is a mutable pair or m is an immutable pair.

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.