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 v = A; 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. I will assume that all function declarations are top-level, and that code snippets are taken from function bodies. #================# | 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) 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" 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]]] Variables ~~~~~~~ V0. "A variable takes the value it is assigned." var v = 0; v === 0 V1. "A function call may not change the value of a variable it was not passed." var v = 0; f(); v === 0 V2. "A function call may not change the value of a variable it was passed." var v = 0; f(v); v === 0 #==============# | 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 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.