Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example:
Nat = ∀ P : * ∀ S : Nat -> P ∀ Z : P P Zer = λ P : * λ S : Nat -> P λ Z : Nat Z Suc = λ x : Nat λ P : * λ S : Nat -> P λ Z : Nat S x two = Suc (Suc Zer)
If we built an eager type-checker and asked it to infer
Zer, it'd not halt, as
Zer's type is infinite:
two : ∀ (P : *) -> ∀ S : (∀ (P : *) -> ∀ S : (∀ (P : *) -> ∀ S : ...
But if we do it lazily, then it'd output:
Zer : ∀ P : * ∀ S : Nat -> P ∀ Z : Nat Z
Which is the same as
Nat and correct, since
Zer is indeed a proof of
Nat. One could wonder if it could accept "wrong" proofs such as
false : ∀ (P : *) -> P, for some construction of
false. The obvious approach, though, seems not to work:
false = (λ (x : ∀ (P : *) -> P) -> x) false
If we had top-level type-annotations (such as
false : ∀ (P : *) -> P), the checker would indeed accept this term. But, because of curry-style, the only way to infer the type of
false is by inferring the type of
false: it'll be stuck in an infinite loop and never output anything.
In other words, it seems that, for the subset of terms that this type-inferencer halts, it behaves as a consistent proof assistant. Of course, it works a bit differently from usual as it has infinite types and whatnot, but, intuitively, it seems to be a functional system for mathematical proofs, since it seems to be unable to accept
false or other incorrect proofs. If one is able to prove that this type-checker could never accept
false, would it indeed be well suited for mathematical proofs?