Dependent tagless final
Biri N.
PEPM 2022 - Proceedings of the 2022 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2022, pp. 1-13, 2022
Tagless final embedding provides a solution to the expression problem that allows efficient code generation, thanks to multi-staged evaluation. It can, however, be a challenge to compose effectful language fragments in this embedding. This paper proposes a dependent tagless final embedding that uses dependent types to ease the composition of effects. We show that this extension preserves the multi-staging capabilities of tagless final and can help scope effects in domain-specific languages.