Posted by ibobev 1 day ago
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.
Whether or not something belongs into a type system is ultimately determined by the type system. We can choose whether or not mutability is considered a part of a type.
> 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).
This is a bit too simplistic IMO. You're talking about name bindings, the article is talking more about things like interior mutability.
Rebinding a name is ... generally not a type system concern by my understanding.
When you say "we can choose mutability as a part of a type", the question is, what kind of errors are we trying to prevent? What is the semantics we want to give? From that it should be obvious whether it can be subtype or not.
really? i honestly dont have _too_ much experience with functional languages, basically only elixir and consequently some amount of erlang in that vain... but i'd feel like thats not the same? but it may be that my point of view is too narrow.
from my experience with that functional language, the equivalent to this scenario would be a struct - and wherever i can mutate properties within it -- or need to reconstruct the struct from scratch.
both have technical consequences, eg if i passed the struct into a consumer somewhere which keeps it, it would get the "modified" version automatically when the property was changed
but on reconstruction, it'd have to introduce some kind of event listener to handle the reconstruction.
simple example for such a scenario would be eg a session within a SSE api. the mutated struct would trivially allow for an uninterrupted stream no matter how long the session is extended, the latter needs to pay attention so its not opening a memory leak to support that feature.
- 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
Also, Back In The Old Days memory was very expensive and precious so short identifiers were important. Often labels were tightly constrained, for example being limited to six upper-case characters so they would fit in a single word.
The concept is to make things easier for people who are familiar with the language. Making things harder for that group is always counterproductive, because they are the only people who can do any useful work.
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.
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.
In C# ReadOnlyCollection<T> and ImmutableArray<T> are two completely different things for this exact reason.