Curry's paradox

[recursive-types] [totality]

In the simply-typed lambda calculus (which has only function types and a base type), infinite loops are impossible and all programs halt. Surprisingly, this stops being true once recursive types are added, even if no recursive functions or loops are present in the language.

In most languages, there are plenty of ways to write programs that do not terminate, and finding one more is not a soundness issue. However, in total languages (ones in which all programs halt), this does present a soundness issue and the allowable forms of recursive types must be restricted.

The recursive types in question are those that contain a function or method which takes the same type as an argument, which can be used to build a nonterminating computation as follows:

newtype Curry = Curry { r :: Curry -> Int }

f c = r c c
loop = f (Curry f)

type curry = { r : curry -> int }

let f c = c.r c
let loop = f { r = f }

interface Curry {
  public int r(Curry x);
}
static int loop() {
  Curry c = new Curry() {
    public int r(Curry x) { return x.r(x); }
  };
  return c.r(c);
}

In logic, this is known as Curry's paradox.^{1 2} (This has nothing to do with "function currying", other than being named after the same person.) Under the propositions-as-types viewpoint, it causes inconsistency: by replacing Int with any proposition $P$ (including False), the loop function above proves $P$.

To avoid this problem, languages that aim for logical consistency (e.g. the proof assistants Coq and Agda) ban recursive types that take themselves as arguments to functions or methods (so-called "negative recursion"), avoiding Curry's paradox.

(In fact, due to a different issue, banning negative recursion is often not enough, and recursive types must be restricted further to "strictly positive recursion" to remain consistent. See Positivity, strict and otherwise)