As we look towards implementing effect interpreters and incremental builds, type erasure presents itself as a promising strategy for designing the implementation of these features.
This document discusses how we might implement type erasure in a language like Roc, with regard to various language features.
Certain effects, like Map2 and Storage, must store polymorphic values whose types are not reflected in the type of the effect. Doing so requires rank-2 types, first order emulation of rank-2 types, or type erasure.
Rank-2 types are not intended to be supported. Even supporting rank-2 types in limited contexts requires first-order emulation to achieve optimal performance, or else compilation via type erasure, so their value for Roc is nebulous in the context of the other options.
A first-order emulation requires whole-program analysis for evaluation, similar to the first-order emulation provided by lambda sets. This slows compilation and adds another facet that incremental compilation must work around (see below).
Type erasure is more costly than a first-order emulation, and requires boxing (on the heap in general, though in some cases boxes need not live on the heap).
Type erasure provides the benefit of a uniform interface that is not polymorphic to a host’s glue code, and eases incremental compilation significantly (see below).
Effects using Map2 are almost certainly not dominated by the overhead of boxing. Stored is intended mainly for tests and its boxes can be allocated in static memory. As such, the overhead of erasure for effects is considered to be negligible relative to the benefits it provides.
Today, the compilation of Roc programs requires several whole-program analyses. Besides monomorphization, which requires analyses linear in the call stack of a function, abilities induce dependency analyses that are not reflected in the call stack of a function, and lambda sets can also require arbitrarily-deep analyses. These analyses are powerful because they allow Roc to whittle down closures and interfaces to forms that have no runtime cost by trading off compile-time.
However, during development feedback loops, this is often an undesirable tradeoff - indeed, many developers may prefer lower compile times by trading off runtime cost if it improves their feedback loops. As it stands, Roc’s compile times must grow super-linearly to the size of a Roc project. Ideally, Roc compile times would be amortized at near-constant for incremental changes (see incremental compilation below), or be strictly linear to the size of a Roc project.
By type-erasing abilities (via dictionary passing) and lambda sets (via boxed closures), we get closer to cold development builds of Roc projects being linear in the size of the project. It doesn’t get us quite there because of monomorphization, but separate ideas with regard to that can also be discussed.
Ideally, hot builds of Roc projects would be linear in the incremental change to a Roc project, and require linear space in the size of the incremental change (amortized constant space and time relative to the project size). Today, with the best approaches we are able to imagine so far, incremental changes must require super-linear time and space relative to the size of the change, and the time and space complexity is bounded by the size of the entire Roc project and all its dependencies (!).
In development mode, as it is for cold development builds, incremental compilation should be as fast as possible. Type erasure of lambda sets and abilities gives us a mechanism to localize at least those features to individual modules or top-level functions in the incremental compilation scheme. This brings us closer to incremental compilations that are linear in both time and space relative to the size of the incremental change. Like cold development builds, incremental builds may still be super-linear to the incremental change in both time and space due to monomorphization, but reducing three “hard” facets to one is a win.