upvote
> Mutability is a property of variable, not of a value. [...] This has nothing to do with whether it can be reassigned (i.e. mutability).

I feel like you're using "mutable" wrong, as it's used colloquially. E.g. in JS, MDN itself talks about "reassignment"[0] and not "mutability" even though people often use "mutability" as a word to refer to the distinction between `const` and `let`. The only mention of mutability there is:

> Others may prefer `let` for non-primitives that are mutated

I.e. explicitly using `let` for mutated arrays, even if not reassigned, to make the signal mutability (which JS cannot express).

Note that you used "reassignment" which is the specific word for "mutating a binding", but the article is not referring to bindings at all.

[0] https://developer.mozilla.org/en-US/docs/Web/JavaScript/Refe...

reply
This post is about data structures, which are values, but like variables, they also contain values. Therefore they can be mutable. You can argue that a mutable data structure is an object not a value, I suppose. But it can go in the same place as a value, so it makes sense to talk about subtyping.
reply
Which is why "data structures" probably also belong in the "variables" column.
reply
Experimentally, at least one major programming language (Rust) places mutability into the type system.

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.

reply
You have a point; I am looking at it from quite functional programming perspective, because that's how type systems are typically understood. So from that perspective, interior mutability is a form of rebinding.

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.

reply
A system programming language needs to match hardware where mutability is associated with memory addresses, something functional languages can afford to abstract away.
reply
> So from that perspective, interior mutability is a form of rebinding

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.

reply
> it may be that my point of view is too narrow

Not sure if you're just being polite but, in case you're doubting, functional languages make that distinction too.

Haskell has `Data.Vector.Vector` vs `Data.Vector.Mutable.MVector`.

Clojure has `transient`.

OP is just mistaken.

reply
A nitpick: Types are properties of expressions, not values. Type errors happen at compile time, before code runs. Values only exist at run time.
reply
Fair enough. Although I don't fully subscribe to the dichotomy of compile vs run time, we can say that.
reply
In semantics, types are properties of values and expressions. Type safety is about whether the type of an expression always matches the type of the value it evaluates to.
reply
Doesn’t this break down with dependent type systems?
reply
> Types are properties of values, not variables.

In statically typed languages, variables and expressions have a compile-time type and values have a run-time type.

> Mutability is a property of variable, not of a value.

In which languages?

In D, mutability is a property of a type. And variables and expressions have a compile-time type and values have a run-time type, so mutability is also a property of variables, expressions, and values.

(Immutability is also transitive in D, so an immutable value cannot have mutable parts, including mutable references, and a variable with an immutable type cannot contain a value or reference with any mutable parts.)

reply
> Types are properties of values, not variables.

In computer science, specifically programming language theory, types are properties of terms (syntactic expressions). It wouldn’t be possible in general to typecheck a program before running it if you had to have a value before you could discover its type.

reply