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:
You can't be 100% sure an algorithm will work for all inputs by experimenting it on some.
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?