@zyang yes, good catch, these are binary trees!
so the important thing with de bruijn shifts is that going under binders is functorial. in the simplest case, it means that you can define renaming as a functor, and your substitution will be given by a monad relative to that functor.
but this is incredibly inefficient - you now need to traverse the term twice to perform substitution - one to perform renaming under a binder, and one to do the actual substitution.
a better trick is explained in the papers on "Modules over monads", because there is a module involved, it's possible to define the lifting operation (mbind) mutually with the substitution operation. this simplifies the implementation considerably (now you don't even need renamings).
(the really cool thing is that this generalises to polymorphic calculi, the language i'm working on has parametric polymorphism and uses a term-level substitution that's indexed by a type-level substitution)
the code in the screenshot is representing debruijn indeces using Maybe, ie "Just" is "Succ", but there's a very easy way to generalise it to proper de bruijn terms implemented using Fin.
So if you can apply your technique to the code-below, I can translate it to proper de bruijn terms :D
=> More informations about this toot | View the thread | More toots from zanzi@mathstodon.xyz
=> View zyang@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).