Call for help: Implementing defunctionalization at the type-level in the presence of a specializing compiler

[ayazhafiz]

One of Roc's goals is to provide an efficient runtime for the execution of users' programs. Central to that goal is the compilation strategy of closures, which are pervasive in functional programs.

The Roc compiler intends to guarantee defunctionalization and per-closure-specialization of programs via a technology termed "Lambda Sets". Lambda sets are a type-level feature that track the concrete function values (lambdas) a function type is inhabited by, and their respective closure sets. This data is used to unconditionally defunctionalize closures and their calls at compile time. This transformation in turns means that the Roc compiler is able to specialize higher-order functions to the concrete functions passed to them. A technology termed "Morphic" plays a large role on this. Put another way, lambda sets guarantee the transformation of a higher-order program (as most functional programs are) to a first-order program, which are greatly amenable to classical optimizations.

Despite the great promise and potential of lambda sets, we have had significant trouble implementing algorithms related to their type inference, specialization, and compilation. We believe we have developed sophisticated machinery and novel techniques for compilation in the fully-defunctionalized style described above, but as a small team of software developers and language designers, we are encumbered by what we perceive to be a continuous stream of issues that we failed to consider, or otherwise have overlooked in our implementation.

We believe strongly in the opportunity lambda sets provide, both for Roc and the space of programming languages as a whole. At this time, we believe the "low-hanging fruit" of problems related to our inference and compilation of lambda sets to be resolved, and what remain are more general theoretic and algorithmic questions. Some of these questions we believe we can resolve, but expect their analysis and implementation to take on the order of weeks; some, we believe we can resolve but do not understand their larger interaction with the language; some, we do not know of, or have an intuition for, a solution at all.

At this time, we do not believe we have a team with the right experience to develop foundational theories for the inference, specialization, and compilation of lambda sets in a language like Roc, which in turn would drive development of the Roc language implementation. We are looking for individuals that have experience in formalizing type theories, type systems, and specializing compilers, and have an interest in the goals that have been described above. If you are such an individual, we'd love to work with you in any capacity. Please reach out to us on Zulip, or comment on this issue.

If you are interested in learning more about lambda sets and Roc's use of them, you may enjoy the following resources.

• Bett�er Defunctionalization through Lambda Set Specialization (William Brandon, Benjamin Driscoll, et.al.) - the original description of defunctioanlization via Lambda Sets as used by the Roc compiler. Also describes the Morphic optimizer used by the Roc compiler.
• Definitional interpreters for higher-order programming languages - possibly the first reference to defunctionalization in the implementation of programming languages.
• Defunctionalization: Everybody Does It, Nobody Talks About It - a general description of defunctionalization, in the context of programming languages, and in other contexts too.
• Eliminating indirect calls and heap-allocated closures via defunctionalization - a blog post authored by myself describing defunctionalization via Lambda Sets in a small lambda calculus extended with coroutines.
• Ambient lambda set specialization - a description of how Roc implements the inference and specialization of type classes in the presence of lambda sets. This is one area where we believe formalization of the system and proofs of soundness/completeness would greatly aid the development of Roc's implementation.
• Roc Projects - a description of projects around lambda sets, and related projects, that may be suitable for theses.