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. antonvs · 1789897068 · focus · HN ↗

      > 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.

Unofficial Hacker News client; not affiliated with Y Combinator.