What type system fits the subclass of λ-terms that can be reduced optimally?

Question

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that Lamping's algorithm is optimal and superior to naive strategies.

In order to use this in practice, one can write programs on the untyped lambda calculus and experimentally test if Lamping's Algorithm works on them for some inputs. It it does, the term is probably on that subset. For example, my answer to this question is a Church-nat sorting algorithm that was developed this way. That is inconvenient for 2 obvious reasons:

1. You can't be 100% sure an algorithm will work for all inputs by experimenting it on some.

2. Programming on the untyped lambda calculus can lead to human type errors.

An immediate solution to problem #2 would be to instead write your programs in a type system on the Lambda Cube (such as System F), but that doesn't work quite well in practice because algorithms on the optimal subset often rely on Scott-encoded data structures (as depicted on my answer above), which are excluded from those type systems. And about problem #1, I'm aware of some type systems based on light logics, but I found them overly complicated and I'm not sure how they could be used in practice.

What type system better fits the subclass of λ-terms that can be reduced optimally, in a way that could be used as the type system of a practical programming language?

Answer 1

I think that the type system you want is elementary affine logic with fixpoints.

A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, is that types do not ensure termination: unlike usual logical system, cut-elimination follows from a structural property of proofs (namely, stratification), the logical complexity of formulas does not play any role. Types in EAL only give you well-formedness properties (like progress, i.e., normalization doesn't get stuck; or the fact that the normal form will have a certain shape).

The fact that cut-elimination holds regardless of types means that you can add arbitrary type fixpoints to EAL and you still get normalization with the same complexity bounds (elementary), because you still have stratification. With type fixpoints, Scott numerals get the following type:

$$\mu \beta.\forall \alpha.(\beta\multimap\alpha)\multimap\alpha\multimap\alpha$$

A paper that uses EAL+type fixpoints explicitly is

Patrick Baillot. On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy. Information and Computation 241: 3-31, 2015.

You will find formal definitions there. However, I am afraid that no implementation exists.