07:58 <d_bot> <Cyclomatic Complexity> hi

08:04 <d_bot> <Cyclomatic Complexity> i want to have a small-step lambda-calculus reducer (not necessarily CBV), but..

08:04 <d_bot> <Cyclomatic Complexity> - substitution based interpretation has O(n) cost in the size of the body. (iirc, the same is true for both debruijn indices and levels, but it's n in the size of env for one of them)

08:04 <d_bot> <Cyclomatic Complexity> - embedding binders in host lang's functions (HOAS?) makes it hard to compare data-structures

08:04 <d_bot> <Cyclomatic Complexity> - machine based things have a local context beyond the term itself

08:04 <d_bot> <Cyclomatic Complexity>

08:04 <d_bot> <Cyclomatic Complexity> ideally, i'd also like to benefit as naturally as possible from OCaml's sharing, and to stay pure

08:04 <d_bot> <Cyclomatic Complexity> for instance, naive idea would be to use pointers for vars, but then we'd leave the world of pure data structures.

08:05 <d_bot> <Cyclomatic Complexity> i imagine there's something obvious I'm missing, with a natural implementation, good complexity, etc.

23:56 <d_bot> <Shon F> This is from the realm of interested non-expert fiddling around, but I’ve just done a POC implementation of ABTs (from harpers PFPL) using “immutable refs” for variable binding. You might find it interesting (Tho, being immutable, it doesn’t help with the performance of substitution at all): https://github.com/shonfeder/um-abt/blob/8c2a205ea1cc143b97dfaac7312500ffd93718e2/lib/abt.ml#L8