1. 5

Relational parametricity is an important property of type theories. It implies both the heavily lauded “type safety” property and the slightly quieter but perhaps more interesting “abstraction safety” property. It’s also violated in many, many languages (notably, not Haskell).

This paper notes that parametricity is a kind of invariance which lets you read out “free theorems” which hold merely by the forms of invariance allowed by a type (or kind). Noether’s Theorem in physics states that continuous invariances of physical laws let you read out “conservation theorems” that the system satisfies such as the conservation of momentum or energy.

Can Noether’s Theorem arise naturally from the relational parametricity of a suitably design type system? This paper demonstrates that the answer is yes.

  1.