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.
#======================#
| First, some notation |
#======================#
x, y, z - values
A, B, C - expressions
f, g, h - function names
v, w - variable names / identifiers
Here is the correspondence between our notation, and the syntax of the
four languages in question,
Notation
x == y
var v = A
func f(x, y) {A}
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
A[B/v] means A, with B substituted for (unbound occurrances of) v.
A === B means that A and B are equivalent (interchangable)
expressions.
#================#
| The invariants |
#================#
Arithmetic
~~~~~~~~
(For standard library +, *, -, /)
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)
A2 fails in python because "hi " + "there" != "there" + "hi ".
Booleans
~~~~~~
B0. if A then B else C === if A == true then B else C
Comparisons
~~~~~~~~~
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 #0-#3. Every language considered has NaN,
so #4 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"
Variable Definitions
~~~~~~~~~~~~~~~~~~
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
Functions
~~~~~~~
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]
Miscellany
~~~~~~~~
M0. "Identifiers may be escaped without changing their meaning."
id === \u0069\u0064
Fun fact - in Ocaml,
let update x = lift2 LocMap.add x [[[type checked]]]
let update = lift2 LocMap.add [[[didn't]]]
#==============#
| The results! |
#==============#
H - Haskell
C - C
P - Python
J - Javascript
1 - Holds
0 - Does not hold
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
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 prefere Haskell to Javascript.