Programming Languages

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.