I feel like the explanation is overcomplicated. Types are properties of values, not variables. Mutability is a property of variable, not of a value.

So it's kind of a categorical error. (I want to joke here that all categorical errors are just type errors in category theory.) When we speak of "type of a variable", we mean this variable can only be assigned (bound to) values of certain type. This has nothing to do with whether it can be reassigned (i.e. mutability).

So you don't even need the notion of subtyping to explain this.

Also, one could probably define variable as a monad over its type.

So really there are 2 orthogonal axes:

- A: can I change the value

- B: can something else change the value (can I depend on a predictable stable value)

Because the axes are orthogonal, hierarchical based subtyping (inheritance) breaks, but type classes (interfaces), ad hoc polymorphism, would work.

In C, const answers A

In rust, due to pointer aliasing restrictions (either one mut pointer xor any amount of read only pointers), (lack of) mut answers both A and B

If you pair mutability with exclusive access then you have handled the objection raised by the (some may say overly) strict definition of subtyping here and also the attempt to argue over the objection. No code which asks for an immutable instance will ever observe the mutability because the ask for an immutable reference is exclusive. Therefore, you could pass the mutable reference but so long as something holds onto that reference the mutability is no longer available to other code.

So mutability xor aliasing provides this strict subtyping relation. Of course, you also then need ways of loosening this by providing objects without such a contract and you enter the land of interior mutability, where again the mutable methods can be understood as a part of a subtype because a holder of the reference without mutable methods was explicitly told that there was no the guarantee that the object wouldn't change.

In other words, immutable != read only.

In C# ReadOnlyCollection<T> and ImmutableArray<T> are two completely different things for this exact reason.

I would phrase it in terms of subsets. All cats are mammals, therefore "cat" is a subtype of "mammal". So the possible values of the type "cat" are a subset of the possible values of the type "mammal".

In contrast, neither are the mutable things a subset of the immutable things nor the other way round. It's not the case that everything mutable is immutable nor that everything immutable is mutable. The two types are disjoint.

As a total aside, the names `car` and `cdr` for "head" and "tail" are honestly some of the most baffling historical relics in all of computing.

So the problem is that the semantic of methods (car, cdr) is not well defined: it is either "give me that member" or "give me that member and guarantee next time the result will be same". And the solution is to clearly separate those by adding more method names.

The cons example is conflating implementation details (return the value passed in to cons) with the semantics (return the left-side of this pair that was instantiated by cons). In the first case it is a category error to think about mutability. In the second mutability makes perfect sense.

Moreover, I suspect it is possible to construct an interface such that to prove statically that you can Liskov Substitute a type into it would be equivalent to deciding Halt: All you need are extensional semantics in your type system.

Yep, I wondered that for a few optimizations in Racket. It's harder than it looks, probably something about covariant or contravariant types, I gave up.

Isn't NSMutableArray a subclass of NSArray in a few languages?

as far as my set theoretical intuition goes, immutable has to be a subtype of mutable, if anything.

Because if mutable is a sub type of immutable, it wouldnt be right to give a mutable value when the receiver expected immutable values. The same is also true if one reverses the relationship, the mutable operations should not be defined on the immutable, and if they were that would be dumb because the immutable implementations should fail, which is silly.

The fact that it requires so much explanation, indicates the level of degradation in the reasoning ability of the audience. A value of a subtype shall deliver all of the expectations of its super type, because it is wearing both the hats of super type and sub type.