Support delayed substitutions

[fizruk]

When implementing evaluation of terms for $\lambda$-calculus or similar systems, NbE algorithms outperform other implementations by a large margin. It appears that the main ingredient here is the delayed substitutions. As mentioned in the «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»¹, it seems reasonable to generalize terms with delayed substitution with a variation on free foil:

data ScopedClosure sig n where
  ScopedClosure :: Binder n l -> Closure sig l -> ScopedClosure sig n

data Closure sig n where
  VarC
    :: Name n -> Closure sig n
  Closure
    :: Subst (Closure sig) n o   -- Environment (values of captured variables).
    -> sig (ScopedClosure sig n) (Closure sig n)
    -> Closure sig o

It could be useful to add this variation under Control.Monad.Free.Foil.Delayed, possibly with generic conversion to/from regular free foil.

Footnotes

1. Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. 2024. Free Foil: Generating Efficient and Scope-Safe Abstract Syntax. 4th International Conference on Code Quality (ICCQ), Innopolis, Russian Federation, 2024, pp. 1-16 http://doi.org/10.1109/ICCQ60895.2024.10576867 (arXiv version at https://arxiv.org/abs/2405.16384) ↩