Has anyone used Pottier and Gauthier's polymorphic defunctionalization in a modular compiler?

Question

Defunctionalization is a program transformation that converts higher-order programs into first-order programs. The idea is that given a program, there are only finitely many lambda-abstractions, so you can replace each lambda with an id, and each function application with a call to an apply procedure which branches on that id. This is sometimes used in compilers for functional languages, but its applicability is limited by the fact that defunctionalization is a whole-program transformation (you must statically know all of the functions in the program), and so only whole-program compilers make use of it.

However, Pottier and Gauthier have a given a polymorphic typed defunctionalization algorithm using a more sophisticated typing involving GADTs. Now, given their encoding, it's possible to add a catch-all case to their lambda datatype that isn't a tag, but which contains a higher-order function. This means that it should be possible to use their encoding to defunctionalize on a module-by-module basis.

Has anyone done this, and point me to a compiler using this idea? (Toy compilers are okay, and in fact preferred.)

Answer 1

One approach is described by

Georgios Fourtounis and Nikolaos S. Papaspyrou. 2013. Supporting Separate Compilation in a Defunctionalizing Compiler. SLATE 2013.

As @gasche mentions:

A different approach at the problem would be to consider that each module can define its own "defunctionalized functions" type and dispatcher/handler.

You can "link" those types and handlers with a specialized linker. Unlike using open datatypes, you concatenate the list of constructors and the case functions. But the linker must add cases for partial application: Without whole-program analysis, you cannot predict which partial applications can be used for which function, so you add all cases. An $n$-ary function can be partially applied to $i$ arguments (with $0< i < n$) and produce a function of arity $n-i$, which can be partially applied again.

Answer 2

Now, given their encoding, it's possible to add a catch-all case to their lambda datatype that isn't a tag, but which contains a higher-order function. This means that it should be possible to use their encoding to defunctionalize on a module-by-module basis.

Could you elaborate a bit more on what you mean here? I don't understand how adding a base case (would that be to the datatype, to the pattern-matching of the dispatching function, or both?) helps modularity in the way you described; by the way, why do you mean exactly by "module by module" basis?

I can imagine a "base case" being used, inside a given module/program, for selective defunctionalization: you would have an additional constructor to your reified function type that is not a tag, but simply embeds all 'a -> 'b functions, so that packing a function in this constructor, instead of giving it a reified tag, would prevent its defunctionalization.

A different approach at the problem would be to consider that each module can define its own "defunctionalized functions" type and dispatcher/handler. Functions from module M1 would have type M1.arrow and be applied using M1.apply, etc. While that works well for first-order uses of the functions, I don't quite well see how you could extend it to higher-order function (which shouldn't have to know where their functional argument come from): if you bundle a function with its dispatcher, you're re-entering the realm of indirect function calls.

Finally, there is in the paper you referenced a quick mention of the whole-program vs. modular approach, but I don't see how it relates to your proposal. What they describe is expressed in terms of "open extensions" of both functions and data types (functions and types that could be defined across several independent modules). This is mostly a ML-way to describe the fact that you may defer the combination of analysis/transformations of independent modules at link-time, relaxing the necessity of whole-program transformation.