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)


    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 like Haskell more than Javascript.