Thread

1. js8 · 1789889511 · focus · HN ↗

   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.

   1. rtpg · 1789890879 · focus · HN ↗

      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.

      1. js8 · 1789891982 · focus · HN ↗

         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.

         1. skew-aberration · 1789896886 · focus · HN ↗

            A system programming language needs to match hardware where mutability is associated with memory addresses, something functional languages can afford to abstract away.

Unofficial Hacker News client; not affiliated with Y Combinator.