Tonight I finished an Idris port of McBride’s co-de-Bruijn implemented by Dan Doel (links in the readme): “Everybody’s Got To Be Somewhere”.
The idea is to apply the linear treatment of variables to the intuitionistic lambda. That is, build on the fact that in linear logic the starting sequent is A ⊢ A: variable constructors don’t carry any additional structural information, but only signal that we have a single formula in context, which is what we use immediately. Then we have to sprinkle weakening/contraction over the rest of the rules, i.e., every lambda should know immediately whether its argument is used or not, and every application should say how the variables are distributed between the function and the argument. Along the way, it turns out that we enter the magical world of Schanuel toposes aka Kleisli-category of free algebras over the inclusion monad. All these scary words stand for the fact that we are essentially carrying around a bundle that shows how to weaken the context to the needed one.
The benefit of this thing is not entirely clear, but for example hereditary substitution becomes structurally recursive, which is always a win for total languages. In general, McBride hints at more efficient and convenient typecheckers for provers.