Abstract from the ICFP 2024 paper:

Many abstraction tools in functional programming rely heavily on general-purpose compiler optimization
\ to achieve adequate performance. For example, monadic binding is a higher-order function which yields
\ runtime closures in the absence of sufficient compile-time inlining and beta-reductions, thereby significantly
\ degrading performance. In current systems such as the Glasgow Haskell Compiler, there is no strong guarantee
\ that general-purpose optimization can eliminate abstraction overheads, and users only have indirect and
\ fragile control over code generation through inlining directives and compiler options. We propose a two-stage
\ language to simultaneously get strong guarantees about code generation and strong abstraction features. The
\ object language is a simply-typed first-order language which can be compiled without runtime closures. The
\ compile-time language is a dependent type theory. The two are integrated in a two-level type theory.
\ We demonstrate two applications of the system. First, we develop monads and monad transformers. Here,
\ abstraction overheads are eliminated by staging and we can reuse almost all definitions from the existing
\ Haskell ecosystem. Second, we develop pull-based stream fusion. Here we make essential use of dependent
\ types to give a concise definition of a concatMap operation with guaranteed fusion. We provide an Agda
\ implementation and a typed Template Haskell implementation of these developments.

The repo also contains demo implementations in Agda and Haskell), and older papers/implementations/videos.