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. noelwelsh · 1789890453 · focus · HN ↗

      A nitpick: Types are properties of expressions, not values. Type errors happen at compile time, before code runs. Values only exist at run time.

      1. pxeger1 · 1789891090 · focus · HN ↗

         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.

Unofficial Hacker News client; not affiliated with Y Combinator.