Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The page seems to describe a concept which is usually treated metatheoretically, i.e. definitional equality, in terms of assignment of mutable variables, such as in a programming language (which is what I assumed “assignment operator” would refer to). I find this presentation a little confusing.
Probably because $\coloneqq$ is overloaded and used for both assignment of mutable variables in some programming languages and a shorthand for definitions in mathematics. The two are not the same because in mathematics most definitons are static: after defining the symbol $\mathbb{Q}$ to be the rational numbers one can’t then go ahead and then define $\mathbb{Q}$ to be the real numbers instead.
@2, 3
The use of $\coloneqq$ in mathematics and functional programming and in any other context where the variables are static is called single assignment or initialization.
Wikipedia states that
In functional programming, assignment is discouraged in favor of single assignment, also called initialization. Single assignment is an example of name binding and differs from assignment as described in this article in that it can only be done once, usually when the variable is created; no subsequent reassignment is allowed.
I think it deserves its own page separate from assignment.
moved info about $\coloneqq$ in type theory over to definition article under section “single assignment operator”, since single assignment in type theory is really about definitions.
Anonymous
1 to 9 of 9