Invariants help us reason about our programs. Herein lies a list of invariants you might expect to hold, and a table showing whether or not they hold for four languages: Haskell, C, Python, and Javascript.
This page is split into three parts: first I’ll introduce the notation I’ll use to write down the invariants, then I’ll list a bunch of invariants you might want to hold, and finally I’ll say whether or not they hold in Haskell, C, Python, and Javascript.
The four language’s we’re going to compare have totally different syntax. Instead of writing each invariant down four times, in the syntax of each language, I’m going to pick one notation and stick to it. I’ll use variables to stand for the following things:
x, y, z - values
A, B, C - expressions
f, g, h - function names
v, w - variable names / identifiers
And this notation:
Notation
x == y
var v = A
func f(x, y) {A}
to mean these things in each of the four languages:
Javascript
x === y
var v = A;
var f = function(x, y) {A};
Python
x == y
v = A
def f(x, y):
A
C
x == y
<type> v = A;
<type> f(x, y) {A}
Haskell
x == y
v = A
f x y = A
Finally, I’ll use A[B/v] means A, with B substituted for
(unbound occurrances of) v.
And I’ll write an invariant as A === B; meaning that A and B are
equivalent expressions.
I will assume that all function declarations are top-level, and that code snippets are taken from function bodies.
Identity
A0. x + 0 = 0 + x = x
A1. x * 1 = 1 * x = x
Commutativity
A2. x + y = y + x
A3. x * y = y * x
Associativity
A4. (x + y) + z = x + (y + z)
A5. (x * y) * z = x * (y * z)
Inverse
A6. x - x = 0
A7. x / x = 1.0
Distributivity
A8. (x + y) * z = (x * z) + (y * z)
(Assuming that +, *, -, / are the operations as defined in the
standard library, as opposed to, e.g., being defined via operator
overloading.)
B0. if A then B else C === if A == true then B else C
C0. x == x
C1. If x < y then not y < x
C2. x < y or y < x or x == y
C3. x <= y iff not y < x
C4. If x < y and y < z then x < z
The existence of NaN breaks C0-C3. Every language considered has NaN, so C4 is the only property with a hope of surviving. It may hold in C, Python, Haskell.
It does not hold in Javascript:
"2" < 3 && 3 < "04" && "04" < "2"
D0. A variable may be replaced by its definition:
var v = A; B === B[A/v]
D0'. In pure code, a variable may be replaced by its definition:
var v = A; B === B[A/v], A, B pure
F0. A function may be replaced by its definition:
func f() {A}; B === B[A/f()]
F0'. In pure code, a function may be replaced by its definition:
func f() {A}; B === B[A/f()], A, B pure
F1. Calling a function is the same as evaluating its arguments and
then evaluating its body with the parameters replaced by the
evaluated arguments:
func f(x) {A}; f(B) === var x = B; A[*x/x]
M0. Identifiers may be escaped without changing their meaning:
id === \u0069\u0064
This does not hold in OCaml:
let update x = lift2 LocMap.add x [[[type checked]]]
let update = lift2 LocMap.add [[[didn't]]]
It also does not hold in Javascript: see “direct” and “indirect” eval.
V0. A variable takes the value it is assigned:
var v = 0; v evaluates to 0
V1. A function call may not change the value of a variable it was not passed:
var v = 0; f(); v evaluates to 0
V2. A function call may not change the value of a variable it was passed:
var v = 0; f(v); v evaluates to 0
Using the following abbreviations:
H - Haskell
C - C
P - Python
J - Javascript
1 - Holds
0 - Does not hold
The results are as follows:
H C P J
A0 1 1 1 0
A1 1 1 1 0
A2 1 1 0 0
A3 1 1 1 0
A4 0 0 0 0
A5 0 0 0 0
A6 0 0 0 0
A7 0 0 0 0
A8 0 0 0 0
B0 1 0 0 0
C0 0 0 0 0
C1 0 0 0 0
C2 0 0 0 0
C3 0 0 0 0
C4 1 1 1 0
D0 1 0 0 0
D0' 1 1 1 0
F0 1 0 0 0
F0' 1 0 0 0
F1 1 1 0 0
M0 1 1 1 0
V0 1 1 1 1
V1 1 1 1 1 (dynamic scope breaks this)
V2 1 1 1 1 (C++ breaks this)
This table is conservative. Where there is a 0, I know of a counterexample. But the 1s are merely my best guesses; perhaps some of them should be 0s. I’d be interested to hear of counterexamples.
FYI, this is why I like Haskell more than Javascript.