Module Generation without Regret
Yuhi Sato

Yukiyoshi Kameyama

Takahisa Watanabe

Department of Computer Science
University of Tsukuba
Tsukuba, Japanyuhi@logic.cs.tsukuba.ac.jp

Department of Computer Science
University of Tsukuba
Tsukuba, Japan
kameyama@acm.org

Department of Computer Science
University of Tsukuba
Tsukuba, Japan
takahisa@logic.cs.tsukuba.ac.jp

Abstract1

Modules are an indispensable mechanism for providing abstraction to programming languages. To reduce the abstraction overhead in the usage of modules, Watanabe et al. proposed a language for generating and manipulating code ofmodules, and implemented it via a translation to plain MetaOCaml. Unfortunately, their solution has a serious problem ofcode explosion if functors are repeatedly applied to modules.
Another problem in their solution is that it does not allow
nested modules.
This paper proposes a refined translation for a two-stage
typed language with module generation where nested modules are allowed. Our translation does not suffer from thecode-duplication problem. The key idea is to use the genlet
operator in latest MetaOCaml, which performs let insertion
at the code-generation time to allow sharing of code fragments. To our knowledge, our work is the first to apply
genlet to code generation for modules. We conduct an experiment using a microbenchmark, and the result shows that
our method is effective to reduce the size of generated codethat would have been exponentially large.

Program generation breaks the trade-off between productivity and performance, and has been studied intensively[14]. Multi-Stage Programming (MSP) languages such as
MetaML provide a way to generate programs against runtime parameters while static safety assurance is guaranteed.
Unfortunately, it is difficult to guarantee its safety beyond
term generation, and generating a module is not allowed in
MetaOCaml, a multi-stage extension of OCaml.
A module system in ML is highly valuable for providing
high-level abstraction as well as from developing practicalapplications. Large programs can be developed efficiently
using modules, as they allow us to build each software component independently, and to compose them in a safe way toachieve reusability and maintainability. On the practical side,
MirageOS1 is a successful example of large-scale applications which use a number of modules. In the implementationof MirageOS, OS components such as device drivers andprotocols are implemented as independent libraries, whichcontains thousands of modules. On the research side, interesting extensions using modules have been proposed: modular
implicits [18], extensible language-integrated query [15] andtagless-final embedding [2].
Inoue et al. [7] were the first to propose a language extension for generating code of a module in the MSP style. They
investigated the abstraction overhead in ML-style modules,
and pointed out that the problem may be solved in a hypothetical extension with module generation. Watanabe et al.
[17] proposed a language λ <M > for generating the code of amodule, and implemented the language. They have also conducted an experiment to show that the abstraction overhead
in modules can be reduced. Unfortunately, their approach
has another problem; code generated by their method canbecome so large that it may not compile.
In this paper, we proposed a language and its implementation that solve the problems left open by Watanabe et al.
First, we introduce a new translation from λ <M > to MetaOCaml to solve the code-explosion problem in Watanabe etal.’s approach. Our key idea is to use the genlet primitivein MetaOCaml for let-insertion, to avoid code duplication.
Second, we show that our language allows nested modules incode generation. Third, we briefly mention the type system

CCS Concepts • Software and its engineering → General programming languages.
Keywords Program Generation, Modules, Type Safety, Program Transformation
ACM Reference Format:
Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe. 2020.
Module Generation without Regret. In Proceedings of the 2020 ACM
SIGPLAN Workshop on Partial Evaluation and Program Manipulation(PEPM ’20), January 20, 2020, New Orleans, LA, USA. ACM, New
York, NY, USA, 13 pages. https://doi.org/10.1145/3372884.3373160

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies
are not made or distributed for profit or commercial advantage and that
copies bear this notice and the full citation on the first page. Copyrights
for components of this work owned by others than the author(s) must
be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee. Request permissions from permissions@acm.org.
PEPM ’20, January 20, 2020, New Orleans, LA, USA© 2020 Copyright held by the owner/author(s). Publication rights licensed
to ACM.
ACM ISBN 978-1-4503-7096-7/20/01. . . $15.00
https://doi.org/10.1145/3372884.3373160

Introduction

1 https://mirage.io

PEPM ’20, January 20, 2020, New Orleans, LA, USAof our language. Furthermore, we discuss several interesting
topics on modules such as the code of a functor.
The rest of this paper is organized as follows: §2 shows thebenefits of modular programming and describes the previous
work for module generation and its problems. We introduce
our solution in §3. §4 defines our source language that allows
module generation. §5 defines the translation from the source
language to MetaOCaml and mentions the type system. The
experiments on microbenchmark and their results are shownin §6. We discuss our translation in §7 and describe therelated work in §8. §9 give conclusion and future work.

Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe

This section introduces the motivating example and illustrates the benefits of modular programming. It also explains
a summary of previous studies on module generation andtheir problems.

reusable, testable and maintainable programs. The functor
provides a common implementation. The signature supports
a loosely coupled implementation which is independent of
the module implementation. Therefore, we can easily swap
the implementation. For example, to change the destinationof logs from the standard output to a file, we create a newmodule FileLogger that implements the signature LOG, andapply the Main. Also, a mockup version of the module Tcp
that does not actually communicate is useful for unit testing.
Second, large-scale applications may be built easily withmodules and functors. By dividing a large program into
smaller modules, we can ask an expert to develop each module independently of the others. To assemble these modules,
nested modules are essential. In the real world, the website
of MirageOS is built with up to 10 functor applications, andthe Mirage repository hosts hundreds of libraries which use
modules [13].

2.1

2.2

2

Motivating Example

Modular Approach

The module system allows us to build clean, maintainable
and large-scale applications. Our motivating example is a
simple implementation of an echo server:
module Main ( Log : LOG ) ( Tcp : TCP ) = structmodule Server = MakeServer ( Tcp )let echo msg =Log . info ("[ echo ] Received : "^ msg );Log . info ("[ echo ] Send : "^ msg );msg
let start =let tcp = Tcp . create " localhost " 7777 in
Server . start tcp echo
endThis program creates a new network service which accepts
a connection on the TCP port 7777, receives a message, andechoes the message back to the client and outputs logs. We
briefly explain an ML module. A module (structure) consists of components that are declarations of values, types,
and nested modules, and a parameterized module is called af unctor . The type of a module is called a siдnature, which
is an interface to the module. In the above functor Main,
the implementations of modules Log and Tcp are abstracted
by signatures LOG and TCP respectively. The functor Main
makes the nested module Server which is a server libraryon the given module Tcp, and passes the component (function) echo to the function Server.start as a callback. To
run the echo server, we apply the functor to two modules
that implement the signatures, create a new module M, andcall its start function:
let module M = Main ( PrintLogger ) ( Tcp ) in
M . start ;;There are several reasons to use modules and functors
to build applications in this way. First, it helps us to write

Module Generation

Modular programs sometimes suffer from performance penalty; modules obtained by functor applications may haveruntime overhead due to indirection. In the above example,
the function Log.info is called via an indirect access. Also,
the function Server.start is called with repeated indirections because the functor MakeServer refers to the module
Tcp. In general, programs including many repeated functor
applications possibly have serious performance penalty.
Watanabe et al. [17] gave the language λ <M > , an extensionof MetaOCaml, that allows generation of code of a module.
They used first-class modules for generating and manipulating code of a module, that can be passed to and returned
from functions.
Figure 1 shows the functor Main written in λ <M > . For thesake of explanation, the functor Main is simplified and has
the function echo only.
Let us explain MetaOCaml very briefly. MetaOCaml provides three multi-stage operators ⟨⟩, ∼, and run . Brackets⟨e⟩ generate code of the expression e and escape ∼ e exempts the expression e from the brackets. When the typeof e is τ , the type of ⟨e⟩ is τ code. The expression run ecompiles the code e and executes it. In Figure 1, the mainfunctor (function) receives code of a module and returns a
new code of a module. $ is a new operator added to λ <M > ,which extracts code of a component from code of a module.
$log.info means that extract the code of the function info
from the code of the module log. Thus, the ∼($log.info)
part is replaced with the code of the function log.info, andthe abstraction overhead is eliminated.
Watanabe et al. implemented λ <M > by a translation to
MetaOCaml. Its main role is to eliminate a module withinbrackets, which is not allowed in MetaOCaml. Their idea
is to turn the code of a module into a module containing
code. Figure 2 shows the functor Main translated from Figure
1. The type of the function echo is translated from stringModule Generation without Regret

module type MAIN = sig
val echo : string -> stringend
let main = fun ( log : ( module LOG ) code ) -><( module struct
let echo = fun msg ->~( $log . info )("[ echo ] Received : "^ msg );~( $log . info )("[ echo ] Send : "^ msg );msg
end : MAIN ) >Figure 1. Main functor written in λ <M >module type MAIN ' = sig
val echo : ( string -> string ) codeend
let main = fun ( log : ( module LOG )) ->( module structmodule Log = ( val log )let echo = < fun msg ->~( log . info ) ("[ echo ] Received : "^ msg );~( log . info ) ("[ echo ] Send : "^ msg );msg >end : MAIN ')Figure 2. A MetaOCaml program translated from Figure 1-> string to (string -> string) code, and the return
type of the function main is translated from (module MAIN)
code to (module MAIN’). The operators added to λ <M > areeliminated by the translation, and we can run the resulting
code in Figure 2.
2.3 Code Explosion Problem
Unfortunately, Watanabe et al.’s translation has a serious
problem in that the size of generated code may increase exponentially. An illustrative example is the module printLogger
which implements the signature LOG. The code of the module
printLogger written in λ <M > is shown below.
module type LOG = sig
val warn : string -> unit
val info : string -> unit
end
let printLogger = <( module struct
let print = fun level -> fun msg ->let t = Unix . localtime ( Unix . time () ) in
Printf . printf " [% s] %d :% d :% d\n%s\n"level t . tm_hour t. tm_min t. tm_sec msg
let warn = fun msg -> print " WARN " msg
let info = fun msg -> print " INFO " msg
end : LOG ) >The module printLogger exposes two functions, warn andinfo, resp. to display the log level and the timestamp, resp.
The function print is an auxiliary function for formatting
the log. The above program is translated to the following
one:

PEPM ’20, January 20, 2020, New Orleans, LA, USA

module type LOG = sig
val warn : ( string -> unit ) code
val info : ( string -> unit ) codeend
let printLogger = ( module struct
let print = < fun level -> fun msg ->let t = Unix . localtime ( Unix . time () ) in
Printf . printf " [% s] %d :% d :% d\n% s \ n "level t. tm_hour t. tm_min t. tm_sec msg >let warn = < fun msg ->let print = fun level -> ... inprint " WARN " msg >let info = < fun msg ->let print = fun level -> ... inlet warn = print " WARN " msg inprint " INFO " msg >end : LOG )The problem here is that the function warn is defined in
the function info even though it is not used. To avoid freereferences in the result, Watanabe et al.’s translation inserts
all let-binding up to the i-th function into the i +1-th binding.
Hence, it inserts a total of n · (n − 1)/2 let-bindings where
n is the value of components. The program of the function
Main.echo is shown below, which is created by applying thefunctor main to the module printLogger.
# let module Main = ( val main printLogger ) in Main . echo ;;- : ( string -> string ) code = . <(* echo *)fun msg_23 ->(* info *)( fun msg_16 ->let print_20 level_17 msg_18 =let t_19 = Unix . localtime ( Unix . time () ) in
Stdlib . Printf . printf " [% s ] % d :% d :% d \ n % s\n"level_17 t_19 . Unix . tm_hour t_19 . Unix . tm_min t_19 .
Unix . tm_sec msg_18 in
let warn_22 msg_21 = ( print_20 " WARN " ) msg_21 in( print_20 " INFO " ) msg_16 )( " [ echo ] Received : " ^ msg_23 ) ;(* info *)( fun msg_16 ->let print_20 level_17 msg_18 =let t_19 = Unix . localtime ( Unix . time () ) in
Stdlib . Printf . printf " [% s ] % d :% d :% d \ n % s\n"level_17 t_19 . Unix . tm_hour t_19 . Unix . tm_min t_19 .
Unix . tm_sec msg_18 in
let warn_22 msg_21 = ( print_20 " WARN " ) msg_21 in( print_20 " INFO " ) msg_16 )( " [ echo ] Send : " ^ msg_23 ) ;msg_23 >.

The problem in this code is that the function info is defined
twice in the function echo. An ideal code would define a
let-binding for the function info locally and dereference thelet-bound variable twice.
In the worst case, the code size increases exponentiallyin the number of functor applications. 2 In the previous
example, as a function is used via a module twice, the size ofthe generated code is (approximately) doubled. If the function
is used twice in another functor, the size of the code wouldbe (approximately) four times as large as the original one.
2 Since Watanabe et al. used first-class modules to represent modules as

expressions, functors are represented by normal functions over first-classmodules.

PEPM ’20, January 20, 2020, New Orleans, LA, USA

We want to eliminate the overhead from large applications
which use many functor applications, as the code-explosion
problem becomes more serious. Generating such a huge codetakes a lot of time and space, and may cause compilation
failures. Compiler optimization is not useful, since the codeis generated before compilation. The problems above aresummarized as follows.
• The size of the translated code is proportional to thesquare of the number of components.
• Code duplication occurs when the same component isreferenced multiple times from outside of the module.
• The size of the generated code is proportional to the
exponential in the number of functor applications.
2.4

Other Problems

We found a few other problems in Watanabe et al.’s study.
First, their source language was too liberal to be translated
to plain MetaOCaml which does not allow code of modules.
Consider the following example:< let x = 10 + 20 in( module struct let y = 1 end : S) > ;;where S is an appropriate signature. It is translated to:let x = 10 + 20 in( module struct let y = <1> end : S ') ;;The subexpression 10+20 is executed at the future stage inthe first expression, while it is executed at the present stage
in the second expression, violating the distinction of stages.
Second, their language did not allow nested modules asfollows:
module M = structmodule N = struct x = 10 end
let y = N . x + N.x
end

where the module N is a nested module which may be referred
to in the components of M. Nested modules are useful in
expressing a certain class of programs, as described above.

3

Our Proposal

We introduce a refined translation for the language withmodule generation to solve the code-explosion problem described in the previous sections. Our translation performs
dynamic let-insertion, which allows code fragments to beshared among different components of modules. In this section, we explain how the translation works using examples.
The formal definition of our language and translation will
be given in the next section.
Let-insertion is a well-known technique for code sharing
in program transformation (partial evaluation, in particular)[3]. It can be implemented in various ways, and here we
review two most relevant approaches for let-insertion.

Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe

3.1

Static let-Insertion by shift and reset

The first approach uses the delimited-control operators shift
and reset [4], which are available in Scheme/Racket, SML,
OCaml, Scala, and other modern programming languages. In
OCaml and MetaOCaml, they are implemented as an external
library [9]. In this approach, a let expression is packaged
with shift, and the destination for let-insertion is marked byreset. The let expression is inserted at run time. Note thatthe destination of let-insertion is determined statically inthis approach.
The let-insertion technique via shift and reset has beenstudied in program generation [8]. Unfortunately, the technique is insufficient to solve the problem in Watanabe et al.’stranslation. Since the translator does not know (before code
generation) how many times a functor is applied to modules,
it is hard to find the optimal destination for let-insertion
statically.
Let us investigate why a static let-insertion does not solve
the code-duplication problem. Consider the following program with a first-class module:
let mcod = <( module struct
let x1 = 10 + 20
let x2 = x1 + x1
end : S) > ;;where S is a suitable signature. Watanabe et al.’s translation removes the code of modules, and the above code istranslated to:let mcod0 = ( module struct
let x1 = <10 + 20 >let x2 = <~ x1 + ~x1 >end : S ') ;;But the component x2 alone does not make sense becauseof free occurrences of x1, and we need to supply the valueof x1 when we use x2. Instead of naively inlining the codefor x1 to get (10+20)+(10+20), we insert a let expression
to obtain:
let mcod0 = ( module struct
let x1 = <10 + 20 >let x2 = < let t = 10 + 20 in t + t >end : S ') ;;which is a duplication-free code. So far, so good.
As the next step, we apply the following functor fnctr to
macd0 (Watanabe et al. use the first-class modules, hence, afunctor becomes a normal function):
let fnctr mcod = ( module struct
let x = <~ mcod . x1 + ~ mcod .x2 >end : T) ;;fnctr mcod0 ;;For the sake of simplicity, the unpacking of module mcod isomitted. The result of the last line is the following module:( module struct
let x = <(10+20) + ( let t = 10+20 in t + t ) >end : T)

Module Generation without Regret

The final result still contains the code 10+20 twice, whichshows the static let-insertion does not completely solve theproblem. An ideal result would be the following.
( module struct
let x = < let t = 10 + 20 in t + (t + t) >end : T )We can expect that the last result can be obtained by letinsertion, but the destination of let-insertion is the outermost position of nested functor applications. In general, we
may want to apply functors to modules multiple times, andthe ideal destination may be quite distant from the original
position of a let expression.
3.2 Dynamic let-Insertion by genlet
The second way uses the genlet primitive [11] in MetaOCaml3 which performs let-insertion. Unlike let-insertion via
shift and reset, let-insertion by genlet works in code generators only. The notable point in genlet is that a program
need not specify the destination of let-insertion, which isdetermined dynamically when the code is actually generated.
Let us consider the following example using genlet:
let x = genlet <10 + 20 > in <~x + ~x >The genlet primitive is a normal function, which generates a
fresh future-stage variable, a let binding that binds it to theargument of genlet, and returns the code that refers to thisvariable. The generated let binding is inserted somewherein the code, which is decided dynamically. An intermediate
term in this execution is the following.
< let t = 10 + 20 in~( let x = <t > in <~x + ~x >) >which evaluates to the code below.
< let t = 10 + 20 in t + t >The resulting code has no duplicated occurrences of 10 +20.
The destination of let-insertion by genlet is the outermost
location that causes no scope-extrusion problem, namely,
free variables in the argument of genlet should not go beyond
their binders. In summary, genlet is useful to avoid code
duplication in program generation.
The next question is whether genlet is useful for module generation, and how we can solve the code-duplication
problem with modules.
Actually, our solution is very simple; for each value component in a module, we insert the genlet primitive at the
topmost position of the right-hand side of a value component, and that’s all. For instance, we rewrite the previous
module mcod0 to the following one:let mcod1 = ( module struct
let x1 = genlet <10 + 20 >let x2 = genlet <~ x1 + ~x1 >end : S ') ;;3 Available in BER MetaOCaml version N107 and later.

PEPM ’20, January 20, 2020, New Orleans, LA, USA

where two occurrences of genlet are introduced. Other
parts of the program are kept intact.
Although simple, the reason why our solution works israther complicated. Let us consider the execution of mcod1
alone. The right-hand side of each value component of amodule is evaluated one by one, and the function genlet iscalled twice. For the x1 component, we get <let t1 = 10
+ 20 in t1> as its value. The result of the execution of thex2 component is rather unexpected, as it returns <let t1 =10 + 20 in let t2 = t1 + t1 in = t2>. This is quite
different from the result of a simple-minded computation
for x2, which is <let t2 = (let t1 = 10 + 20 in t1) +(let t1 = 10 + 20 in t1) in t2>.
The reason why we got non-duplicating code for x2 issomewhat complicated. 4 For the x1 component, we get <lett1 = 10 + 20 in t1> as its value, which is not surprising.
When we evaluate genlet <e>, we do not immediately get<let t = e in ...t>; rather, it returns an internal data
structure (a triple) consisting of a set of free variables, thebody <e>, and a list of let bindings to be inserted in future.
In other words, genlet <e> is evaluated only partially andthe let-insertion is delayed, similar to lazy evaluation. When
we retrieve the value of the triple at the top level (for instance, the value is printed), let bindings in this triple areinserted at the topmost positions which do not cause thescope-extrusion problem. Coming back to the evaluationof the term genlet <∼x1 + ∼x1>, the value of x1 is a
triple which contains potential dynamic let-insertion. Hence,
there are two nested dynamic let-insertion, and its result has
nested let-bindings such as <let t1 = 10 + 20 in let t2= t1 + t1 in ...>.
Our finding in this paper is the above machinery of genlet
works as well in the presence of modules and functors. To
see it, we consider the evaluation of the term fnctr mcod1,
which simulates a functor application using first-class modules. When we evaluate the term, again the dynamic letinsertion triggered by genlet in mcod1 is delayed until the
result of the whole term is printed. When we print it, dynamic let-insertion by two genlet is actually performed, andwe get the following ideal code as nested let bindings:( module struct
let x = < let t1 = 10 + 20 in
let t2 = t1 + t1 in t1 + t2 >end : T)

Since let bindings for t1 and t2 are nested, it is clear that let
insertion was performed after the evaluation of mcod1.
This feature of genlet has been considered useful in code
generation, but as far as we know, it has not been studied
whether genlet can work beyond module boundaries, until
the work presented in this paper.
4 Our explanation here is essentially due to Kiselyov’s explanation for genlet,

available from the BER MetaOCaml repository on GitHub.

PEPM ’20, January 20, 2020, New Orleans, LA, USA

4

Source Language

Our source language is a two-stage programming language
which is an extension of core MetaOCaml. It includes standard lambda-calculus with primitive operators, let expression, and multi-stage operators for code generation. In thiswork, we confine ourselves to a minimal language to express
our results. We assume that no name collision occurs among
the components of modules and signatures. Extending ourlanguage to a more realistic one is left for future work.
Figure 3 defines the syntax of terms where the index i iseither 0 (present stage) or 1 (future stage). We use metavariables mi for stage-i modules (structures), s i for sequences ofstage-i components, c i for stage-i components of modules,
i for stage-ie for expressions, e i for stage-i expressions, em
first-class modules, x for variables, X for module names, andt for types. A module mi is either a module name X , a struci ). For convenience,ture, or an unpacking expression (val em
we slightly extend the unpacking operator in OCaml so thati ).x is a valid syntax, but it can be easily resolved(val emi ), andby introducing the declaration module X = (val em
relacing it to X .x for a fresh name X . We sometimes omit
the index i in e i .
The syntax for terms is mostly standard except the following. The term m.x is a reference to the x-component of
the module m, and $ and run_module are new operators
introduced by Watanabe et al. If x is bound to code of a firstclass module, $x .y refers to the code of the y-component of
the module, thus the $-operator turns code of module to amodule of code. The run_module runs the code of a module. ⟨⟩, ∼, and run are the standard multi-stage operators
in MetaOCaml, while we take a different syntax for code ofa module < (module mi : M) >. This distinction is introduced since we do not allow ∼ (the splicing operator) to be
applied to the code of a module. In addition, because the terme 1 does not include a module, there is no other way to makethe code of a module, and our syntax rejects expressions thatcannot be translated as the example in §2.4. Our syntax isnatural because it provides two operators that make the codeand two operators that decompose the code.
Figure 4 defines the syntax of types. We use metavariables M for types of a module, S for a sequence of types ofcomponents, C for types of components, and σ for typesof expressions. Types consist of those types in the simplytyped lambda calculus, code types, code-of-module types,
reference to type components, and CSP (Cross-Stage Persistence) for types %σ . Whereas CSP for terms in MetaOCaml
allows one to embed a present-stage value into future-stage
code, Watanabe et al. use CSP for types to embed a presentstage type into future-stage modules. In this work we also
introduced the type (module M) mcod to distinguish thecode type for modules than that for terms (τ code) in order
to disallow code of functors.5
5 see §7 about this choice.

Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabeimi ::= X | struct s i end | (val em)

s i ::= ϵ | c i s i
c i ::= type t | type t = σ | module X = mi | let x :σ = e ie ::= e 0 | e 1
e 0 ::= ⟨e 1 ⟩ | run e 0
10| < em> | (run_module e 0 : M) | x | X .x | em

| p(e 0, · · · , e 0 ) | fun x → e 0 | e 0 e 0 | let x = e 0 in e 0
e 1 ::= ∼ e 0 | $x .x | x | X .x
| p(e 1, · · · , e 1 ) | fun x → e 1 | e 1 e 1 | let x = e 1 in e 1iem::= (module mi : M)

Figure 3. Syntax for terms

M ::= sig S end
S ::= ϵ | C S
C ::= type t | type t = σ | module X : M | val x : σ
σ ::= t | X .t | $x .t | σ → σ | τ code | %σ | (module M)| (module M) mcod
where τ is module-free
Figure 4. Syntax for types
A typing environment is a sequence of declarations(type t)i , (type t = σ )i , (module X : M)i , and (val x : σ )iwhere i is a level (stage). In this work i is either 0 or 1.
Our type system is based on Leroy’s type system for modules [12], and the classic type system λ◦ for multi-stage
language (see [5] for instance), however, we have made ourown modifications. Here we only explain the most typicaltyping rules, and the complete typing rules are shown inAppendix A.
The well-formedness rule for nested modules is:
E ⊢i M wf
E, X i ⊢i S wf
X i < Dom(E)E ⊢i (module X i : M) S wf
where E ⊢i means a typing judgment at the stage i andwf for well-formedness. At the stage i, only the elements
annotated with i in the environment E may be dereferenced.
M wf requires that all component names of M are mutually
distinct, or else the condition X i < Dom(E) is not satisfied.
The typing rule for code of a module is shown below:
E ⊢1 (module m 1 : M) : (module M)
E ⊢0 < (module m1 : M) > : (module M) mcod
The rule for dereferencing a component in code of a module
is as follows:Module Generation without Regret(val x : (module (sig S end)) mcod)i ∈ E S = S 1 (val y : σ ) S 2
E ⊢i $x .y : σ [t ← (val x).t | t ∈ Dom(S 1 )] code

Since the $-operator turns code of a module to a module ofcode, its y-component should have the code type. This rule
has an additional complexity in that we need to substitute atype variable t by (val x).t in the type σ in the conclusion.
To see its reason, consider the following example: let x be
< (module struct type t = int let y : t = 10 end : S) >.
If the typing rule does not do substitution, the type of $x .y
is t, which is a free type variable. By the substitution, it will
become (val x).t, which refers to the t-component of thefirst-class module bound to x (the type int in this case).

5

Our Translation

We introduce a refined translation from our source language
to plain MetaOCaml by improving Watanabe et al.’s one in
two respects. The first is to fix bugs. Indeed their source
language contains code of functors, which cannot be (easily)translated to programs in plain MetaOCaml. We have refined
their source language and define a type-preserving translation here. The second improvement is the better performanceof translated code, which is the main subject of this paper. In
this section, we explain the key part of our translation andthe differences from Watanabe’s translation. The complete
definition of our translation is shown in Appendix B.
5.1

Definitions

We use the notation [[ · ]]i for our translation, which is parameterized by the level i (for i = 0, 1). [[ e 0 ]]0 is the resultof the translation for a level-0 (present-stage) expression e 0 ,and similarly [[ e 1 ]]1 for a level-1 (future-stage) expression
e 1 . [[ ⟨e 1 ⟩ ]]0 is translated to ⟨[[ e 1 ]]1 ⟩. We may omit the index
i in an expression e i . Our translation sometimes needs anadditional parameter d, which shall be explained shortly.
Let us explain the key rules for translation. First, we translate code of a module to a module of code as follows:[[ < (module m : M) > ]]0 = (module [[ m ]]1 : [[ M ]]1 )The outermost brackets are eliminated and the componentsof the module will be translated at level 1. (The translation
rules for the level 0 do not do much work, and are omitted.)
Next, we define a level-1 translation of a type declaration
in a module as follows:[[ val x : σ ]]1 = val x : [[ σ ]]1 code[[ type t ]]1 = type t[[ type t = σ ]]1 = type t = [[ σ ]]1[[ module X : M ]]1 = module X : [[ M ]]1
The type of a value component is translated to the code type.
A type component and a nested module are passed throughby the translation.

PEPM ’20, January 20, 2020, New Orleans, LA, USA

The level-1 translation for terms in a module is also interesting and defined as follows:[[ let x : σ = e ]]1 = let x : [[ σ ]]1 code = genlet ⟨[[ e ]]1 ⟩[[ type t ]]1 = type t[[ type t = σ ]]1 = type t = [[ σ ]]1[[ module X = m ]]1 = module X = [[ m ]]1
A value component is translated into code of the value andgenlet is inserted in front of it, to allow code sharing.
So far, the translation is compositional and simple, but
we need one twist here. Since the translation for code ofmodules moves brackets from outside of a module to inside
a component, it must manage the change of stages for areference in a value component, otherwise the result will
have a dangling reference. For this purpose, we introduce
an additional parameter d in [[ · ]]di , where d is the set of
declarations that may be referenced in the translation, hence
their levels must be adjusted through the translation. Fora sequence s of components at level 1, we accumulate thecomponent c to the set d as follows:[[ ϵ ]]d1 = ϵ([[ c s ]]d1 =[[ c ]]d1 [[ s ]]d1[[ c ]]d1 [[ s ]]c1 ,d(c is a type component)(otherwise)

Because variables (component names) in d have level 1 before
the translation, and level-0 expressions are bound to them,
we need to splice them. Hence, the rules for variables are:(∼ x (x ∈ Dom(d))
1[[ x ]]d =x(otherwise)(∼ (X .x) (X ∈ Dom(d))[[ X .x ]]d1 =X .x(otherwise)[[ $x 1 .x 2 ]]d1 = (val x 1 ).x 2
where Dom(d) is the set of variable names in the domain ofd. The third rule above is the one for dereferencing x 2 inthe code x 1 . After the translation, x 1 becomes a first-classmodule that consists of code of a component, thus we should
translate it to (val x 1 ).x 2 to look up the value of x 2 . Although
MetaOCaml does not allow such an expression, we can translate it to X .x 2 after declaring module X = (val x 1 ).
The run_module operator is translated depending on
the type of the target module. The translation eliminates the
run_module operator and defines a new module. The newmodule contains an unpacked module X where X is a fresh
name, and components of module X .
[[ (run_module e : sig S end) ]]d0
= (module structmodule X = (val [[ e ]]d0 )(X, S) ▷ •end : sig [[ S ]]0 end)PEPM ’20, January 20, 2020, New Orleans, LA, USA

The rule (X, S)▷• applies a run-primitive to each value component in module X of type S. The run_module is applied
to a nested module and the run-primitive is propagated.
(X, ϵ) ▷ • = ϵ(X, (val x : σ ) S) ▷ • = let x : σ = run X .x
(X, S) ▷ •(X, (type t = σ ) S) ▷ • = type t = X .t
(X, S) ▷ •(X 1, (module X 2 : M) S) ▷ • = module X 2 =(val [[ (run_module (module X 1 .X 2 : M) : M) ]]ϵ0 )(X 1, S) ▷ •5.2

Translation Preserves Typing

We can prove that the following form of simple type preservation holds for our translation. If E ⊢0 e : σ is derivable inour type system, then [[ E ]]d0 ⊢0 [[ e ]]d0 : [[ σ ]]d0 is derivablefor the empty set d. We assume here that the translation fora typing environment E is defined similarly for the sequenceof typing components C, and that the target type system hasa typing rule for genlet, which is the same as the one forthe standard let. The proof is straightforward but lengthy,so omitted in this paper.

6

Performance

We have implemented our language through the translationin the previous section, and conducted a few experiments
against microbenchmarks. The result is quite positive for our
claims in that the code-explosion problem in the Watanabe
et al.’s study is solved, or at least, drastically reduced as longas we have experimented.
The microbenchmarks created by Watanabe et al. express
a domain-specific optimization for arithmetic expressions
such as an expression 0 + n → n using the tagless-final
embedding [2]. Figure 5 shows the core part of the benchmark written in λ <M > . The tagless-final style uses module
types to embed syntax and typing rules of the object language. The module type S specifies a type int_t representing a numeric type in the object language, int representing a numeric literal, and the functions add, sub, mul anddiv correspond to four arithmetic operations. The function
suppressAddMulZero is a program translator in such an
object language. It is given an expression of type (moduleS) code and returns code of a module after performing the
optimization. By applying it repeatedly, a fully optimized
module can be obtained. In this section, the depth refers to
the number of repeated functor applications. For the complete implementation, see Watanabe et al.’s paper [16].
The code-explosion problem shows up if we use Watanabe et al.’s translation for the above program. The function
suppressAddMulZero, given a module m, splices the components of m into (the code of) a new module. For example, inYuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe

module type S = sig
type int_t
val int : int -> int_t
val add : int_t -> int_t
val sub : int_t -> int_t
val mul : int_t -> int_t
val div : int_t -> int_t
end

->
->
->
->

int_t
int_t
int_t
int_t

let suppressAddMulZero = fun (m: ( module S )code ) -><( module structtype int_t = $m . int_t * bool
let int = fun n1 ->if n1 = 0 then (~( $m . int ) 0, true )else (~( $m . int ) n1 , false )let add = fun n1 -> fun n2 ->match (n1 , n2 ) with
(n1 , b1 ) ,(n2 , b2 ) ->if ( b1 && b2 ) then (~( $m . int ) 0 ,true )
else ~( $m . add ) n1 n2
let sub = fun n1 -> fun n2 ->if n1 = n2 then (~( $m . int ) 0, true )else ~( $m . sub ) n1 n2
let mul = fun n1 -> fun n2 ->match (n1 , n2 ) with
(n1 , b1 ) ,(n2 , b2 ) ->if ( b1 || b2 ) then (~( $m . int ) 0 ,true )
else ~( $m . mul ) n1 n2
let div = fun n1 -> fun n2 ->match (n1 , n2 ) with
(n1 ,_) ,(n2 ,_) ->(~( $m . div ) n1 n2 , false )end : S) >let rec fix depth m =if depth <= 0 then melse fix ( depth -1) ( suppressAddMulZero m )Figure 5. Core Part of The Benchmarks

the int component, the m.int code is spliced twice. Thus, as
the depth increases, the size of the generated code increases
exponentially.
We use the following programs for experiments.
1. A MetaOCaml program translated from the benchmark
program by our translator.
2. A MetaOCaml program translated from the benchmark
program by Watanabe et al’s translator.
3. A naive OCaml program that expresses the benchmark
without code generation.
For these programs, we measure the memory usage, the execution time of generated code and the time for code generation and compilation. The measurement result is the averageof 10 trials. We conduct these experiments on Ubuntu 18.04

Module Generation without Regret

10

8

0.030

naive (no code generation)
Watanabe et al.
ours

107
106
105
10

4

10

3

102

0.020
0.015
0.010
0.005

101
10

Watanabe et al.
ours

0.025
execution time [s]memory usage [KB]

PEPM ’20, January 20, 2020, New Orleans, LA, USA

0.000

0

0

20

40

60

80

0

100

2

the number of functor applications

Figure 6. Memory Usage
1.8

time for code generation [s]execution time [s]

1.4
1.2
1.0
0.8
0.6
0.4
0.2
0.0
0

20
40
60
80
the number of functor applications

16

Figure 8. Execution Time (zoom in)naive (no code generation)
Watanabe et al.
ours

1.6

4
6
8
10
12
14
the number of functor applications

Figure 7. Execution Time

Watanabe et al.
ours

3

102
101
100
10-1
10-2
10-3

100

LTS, Xeon E3-1225 v6@3.3GHz, Memory 32GB, BER MetaOCaml N107 (OCaml 4.07.1), byte code compiler. The memory
usage is measured using the GNU time command for compiled executables, defined by the maximum resident set sizeof the process during its lifetime.
Figure 6 shows the memory usage where the horizontal(vertical, resp.) axis is the number of functor applications(memory usage on a logarithmic scale, resp.). The programtranslated by Watanabe et al.’s consumes the memory exponentially, and the experiment was only performed up to
depth 16. On the other hand, the memory usage of ours
is linear. The naive program without code generation uses
a recursive module to repeatedly apply a functor for normalization. The recursive module contains several nested
modules, and these are captured each time the functor isapplied. Therefore, the memory usage of the naive programis larger than ours which creates at most 100 modules.
Figure 7 shows the execution time (excluding the time forcode generation). The result shows that the generated modules run faster than the naive one. Our program is about 30%
faster than Watanabe et al.’s (Figure 8). Our non-duplicatingcode reduces the number of steps in program execution andencourages optimization by the compiler.

10

0

20
40
60
80
the number of functor applications

100

Figure 9. Time for Code Generation

Figure 9 shows the time for code generation and compilation where the vertical axis is a logarithmic scale. The timeof Watanabe et al.’s program increases exponentially, whileours has a gentle slope.
In our benchmark, functors are applied to modules quite
a few times, but it is not an unrealistic experiment. Since theimplementation of MirageOS contains a number of functor
applications, a unikernel that runs web service has functor
applications of depth up to 10. At depth 10, the execution
time is 0.15 seconds for the naive program (without code
generation), while it is only 0.012 seconds for our program.
MirageOS actually contains more indirections than this, because it contains a large number of components and nested
modules. Hence, we expect that the benefit of efficient code
generation for modules will be greater.

7

Discussion

7.1

Code of Functors

This design choice was motivated by the following consideration. We first point out that removing this restriction
may be possible, but needs an extra cost. Let us consider an
expression <fun m -> (module ...)> of type ((module

PEPM ’20, January 20, 2020, New Orleans, LA, USAA) -> (module B)) code, which is code of a functor in
our representation. Since plain MetaOCaml prohibits modules within brackets, the brackets should be translated away,
and one possible solution is to use the unstaging translation by Kiselyov [10]. There is, however, a problem withthis solution, in that the unstaging translation translates abracket-expression to a thunk, and it would severely degrade
the performance of generated code and also complicate thewhole translation.
We think that applications for code of functors are notsufficiently appealing, in the way that the cost mentioned
above is justified in the context of program generation. As
is discussed in this paper, functor applications are a major
source of indirections and penalize performance, and the
purpose of making use of the code-generation technique isto optimize (inline) functor applications. Since MetaOCaml
is generative, we cannot manipulate code inside brackets,hence the code of functors may not be further optimized.
7.2

Remaining Duplicated Code

Although our translation eliminates most code duplication,
it still allows duplicated code to be generated at the top level.
For example, if the module printLogger is at the top level(i.e., its code is run), the function info and warn containthe code of the function print. Namely, each component
has no duplicated code, but duplicated may exist between
top-level components. We think that this is not a serious
problem, as such duplication appears only at the top level,
and the performance problem is solved using our solution
as is shown in the previous section.

8

Related WorkIn this section, we explain several closely related work to
our work. For comparison, we pick up three previous works,
Macros, Flambda and MLton, which can eliminate module
overhead at compile time. We also mention Functoria, whichhelps developers build applications that use many modules,
as well as other research on using genlet.
Macros [20] are an extension of OCaml which allows typesafe compile-time metaprogramming. It provides constructors such as quoting <<e>> and splicing $e and can manipulate code fragments similar to MetaOCaml. Macros fully
support the OCaml language including the module system,and the abstraction overhead of modules can be eliminatedin a similar way as ours. However, our approach can generate code specialized for the runtime environment, such as
the number of CPU cores and memory size.
Flambda [6] is an optimizer of the OCaml compiler which
inlines a program whenever possible. Since functor application is the target of inlining for Flambda, an indirection
discussed in this paper might be eliminated by Flambda, too.
Also, MLton [1] is an optimizing compiler for the Standard
ML, which aggressively inlines functors. While both of these

Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe

two studies are fully automated, our approach has its own
merit in that one is given full control as to how and whatcode is generated.
Functoria [13] is a domain-specific language mainly usedin MirageOS, which can manipulate modules and functors
to build modular applications. Its main purpose is to scrap
the boilerplate associated with programs which use modules.
Functoria generates an OCaml program from a configurationthat describes how to combine modules. Since MetaOCaml
does not allow code of modules to be generated as values,
Functoria currently uses an ad hoc approach to generate
code of modules as strings. We hope that our work improves
the implementation of Functoria in the future.
In this study, we have extensively used the genlet primitivein MetaOCaml, which is not yet used in many applications,but has huge potential in realizing code sharing in various
forms. As another application of using genlet, a recent study
by Yallop and Kiselyov [19] makes use of genlet for generating mutually-recursive definitions.

9

Conclusion

In this paper, we have proposed a refined translation for an
extension of core MetaOCaml that can generate and manipulate code of modules. We have conducted experiments for
micro-benchmarks and shown that our translation gives anspace- and time- efficient code for applications which need
repeated applications of functors to modules. Our approachprovides a way to explicitly perform the domain-specificoptimizations, in the programmer’s responsibility, without
relying on a compiler. We think that MirageOS is one of suchapplications where approximately 10-times nested functor
applications are used in practice.
Our contributions in this paper are summarized as follows. First, we experimentally confirmed that dynamic let
insertion by genlet can go across the boundaries of modules
and functors, and can be used to avoid the code duplication problem in a relatively large codebase. Second, we have
solved the code-explosion problem in the previous study by
Watanabe et al., and opened a way to generate code using
high-level programming which makes heavy use of module
abstraction. Third, we have extended λ <M > to allow code
generation of submodules, gave a complete formulation including run_module , and studied its type system.
In future work, we plan to extend our source language toa more realistic one, such as side effects and polymorphism,
mutually-recursive modules, and also develop practical applications using our language for generation of code of modules.
Investigating theoretical foundation of genlet is also an interesting future work.

Module Generation without RegretA

PEPM ’20, January 20, 2020, New Orleans, LA, USA

Typing Rules

E ⊢i m : M(module X : M )i ∈ E(M-Var)E ⊢i X : M
E ⊢i M wf

E ⊢i s : S(M-Str)struct s end : sig S end

E ⊢i

E ⊢i

S wf
(WF-Sig)
E ⊢i sig S end wf

E ⊢i em : (module M )E ⊢i (val em ) : M(M-Val)E ⊢i S wf
E ⊢i s : S
E ⊢i ϵ wf
E ⊢i σ wf

E ⊢i ϵ : ϵ(WF-Empty)
E⊢i e : M

E, x i ⊢i S wf

x i < Dom(E)E ⊢i (val x i : σ ) S wf

E⊢i σ wf

E, (val x :σ )i ⊢i s : S

t i < Dom(E)E ⊢i (type t ) S wf

(WF-Val)

E ⊢i(WF-TypeAbs)
E ⊢i σ wf

E ⊢i

σ wf

E, type t =σ ⊢it i < Dom(E)S wf

E ⊢i (type t = σ ) S wf
E ⊢i M wf

E, X i ⊢i S wf

(type t ) s : (type t ) S

E, (type t = σ )i ⊢i s : S
E ⊢i(WF-Type)t i < Dom(E)E ⊢i (module X i : M ) S wf

E⊢i (module X =m) s : (module X :M ) S
E ⊢i e : σ(E-Var)E ⊢i X .t wf(val x : (module sig S end) mcod)0 ∈E (type t = τ ) ∈S
E ⊢i $x .t wf
E ⊢i σ1 wf
E ⊢i

E ⊢i σ2 wf

σ1 → σ2 wf(val x : (module (sig S end)) mcod)i ∈E S =S 1 (val y:σ ) S 2(T-Dot)E⊢i $x .y : σ [t ←(val x ).t |t ∈Dom(S 1 )] codeE ⊢i σ1 wf
E ⊢i(T-DotCode)E ⊢i e 1 : σ1 → σ2
E ⊢i
E ⊢i e 1 : σ1

(E-DotCode)(E-Fun)E ⊢i e 2 : σ1e 1 e 2 : σ2

(E-App)E, (val x : σ1 )i ⊢i e 2 : σ2
(E-Let)E ⊢i let x = e 1 in e 2 : σ2

E ⊢i M wf
E ⊢i m : M(E-Mod)(module m : M ) : (module M )E ⊢0 σ wf(T-Csp)E ⊢1 % σ wf

E ⊢i

E ⊢i M wf(T-Mod)E ⊢i (module M ) wf

E ⊢1 e : τ(E-Bra)E ⊢0 ⟨e ⟩ : τ codeE ⊢1 (module M ) wf
E ⊢0 (module M ) mcod wf(E-Dot)E, (val x : σ1 )i ⊢i e : σ2
fun x → e : σ1 → σ2

(T-Arr)E ⊢1 τ wf(T-Code)E ⊢0 τ code wf

S = S 1 (val x : σ ) S 2

E ⊢i X .x : σ [t ← X .t | t ∈ Dom(S 1 )](T-Var)(type t = τ ) ∈ S(S-Mod)(val x : σ ) ∈ E(module X : sig S end)i ∈ E

t wf(S-Type)(WF-Mod)E ⊢i x : σ(module X : sig S end)i ∈ E

t i < Dom(E)(type t = σ ) s : (type t = σ ) SE ⊢i σ wf

E ⊢i(S-Let)(S-TypeAbs)

E⊢i m : M E⊢i M wf E, (module X :M )i ⊢i s : S X i <Dom(E)X i < Dom(E)(type t = σ ) ∈ E

x i <Dom(E)E⊢i (let x :σ = e) s : (val x :σ ) S
E, (type t )i ⊢i s : S

E, type t ⊢i S wf

(S-Empty)

E ⊢0 e : σ code
(E-Esc)E ⊢1 ∼ e : σ(T-ModCode)E ⊢0 e : σ code
(E-Run)E ⊢0 run e : σFigure 10. Typing rules for types

E ⊢1 em : (module M )E ⊢0 < em > :(module M ) mcod

(E-BraMod)

E ⊢0 em : (module M ) mcod
E ⊢0

(run_module em : M ) : (module M )(E-Runmod)

Figure 11. Typing rules for terms

PEPM ’20, January 20, 2020, New Orleans, LA, USA

B

Translation

Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe(X, S) ▷ •(X, ϵ) ▷ • = ϵ[[ m ]]di(X, (val x : σ ) S) ▷ • = let x : σ = run X .x[[ X ]]di = X(X, S) ▷ •[[ struct s end ]]di = struct [[ s ]]di end[[ (val e) ]]di = (val [[ e ]]di )[[ s ]]di(X, (type t = σ ) S) ▷ • = type t = X .t
(X, S) ▷ •(X 1, (module X 2 : M) S) ▷ • = module X 2 =(val [[ (run_module (module X 1 .X 2 : M) : M) ]]ϵ0 )(X 1, S) ▷ •[[ ϵ ]]di = ϵ[[ c s ]]d0 = [[ c ]]d0 [[ s ]]d0([[ c ]]d1 [[ s ]]d1
1[[ c s ]]d =[[ c ]]d1 [[ s ]]c1 ,d(c is a type component)(otherwise)[[ c ]]diFigure 13. Translation related to run_module[[ M ]]i[[ type t ]]di = type t[[ type t = σ ]]di = type t = [[ σ ]]i[[ module X = m ]]di = module X = [[ m ]]di[[ let x : σ = e ]]d0 = let x : [[ σ ]]0 = [[ e ]]d0[[ let x : σ = e ]]d1 = let x : [[ σ ]]1 code = genlet ⟨[[ e ]]d1 ⟩[[ e ]]di[[ sig S end ]]i = sig [[ S ]]i end[[ S ]]i[[ ϵ ]]i = ϵ[[ C S ]]i = [[ C ]]i [[ S ]]i[[ C ]]i[[ x ]]d0 = x(∼x[[ x ]]d1 =x[[ type t ]]i = type t(x ∈ Dom(d))(otherwise)[[ type t = σ ]]i = type t = [[ σ ]]i[[ module X : M ]]i = module X : [[ M ]]i[[ X .x ]]d0 = X .x(
∼ (X .x) (X ∈ Dom(d))
1[[ X .x ]]d =X .x(otherwise)[[ fun x → e ]]di = fun (x : [[ σ ]]i ) → [[ e ]]di[[ e 1 e 2 ]]di = [[ e 1 ]]di [[ e 2 ]]di[[ let x = e 1 in e 2 ]]di = let x = [[ e 1 ]]di in [[ e 2 ]]di[[ ⟨e⟩ ]]d0 = ⟨[[ e ]]d1 ⟩[[ ∼ e ]]d1 =∼ [[ e ]]d0[[ run e ]]d0 = run [[ e ]]d0[[ $x 1 .x 2 ]]di = (val x 1 ).x 2[[ (module m : M) ]]di = (module [[ m ]]di : [[ M ]]i )[[ < (module m : M) > ]]d0 = (module [[ m ]]d1 : [[ M ]]1 )[[ (run_module e : sig S end) ]]d0 = (module structmodule X = (val [[ e ]]d0 )[[ val x : σ ]]0 = val x : [[ σ ]]0[[ val x : σ ]]1 = val x : [[ σ ]]1 code[[ σ ]]i[[ t ]]i = t[[ X .t ]]i = X .t[[ $x .t ]]i = (val x).t[[ σ1 → σ2 ]]i = [[ σ1 ]]i → [[ σ2 ]]i[[ σ code ]]0 = [[ σ ]]0 code if σ is module-free[[ %σ ]]1 = σ[[ (module M) ]]i = (module [[ M ]]i )[[ (module M) mcod ]]0 = (module [[ M ]]1 )Figure 14. Translation for types(X, S) ▷ •end : sig [[ S ]]0 end)

Figure 12. Translation for terms

Acknowledgments
The second author is partly supported by MEXT’s Grant-inAid for Scientific Research (B) No. 18H03218.

Module Generation without Regret

References[1] 1997. MLton, a whole program optimizing compiler for Standard ML.
http://www.mlton.org. (1997).
[2] Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finallytagless, partially evaluated: Tagless staged interpreters for simpler
typed languages. J. Funct. Program. 19, 5 (2009), 509–543. https://doi.org/10.1017/S0956796809007205[3] Olivier Danvy. 1996. Pragmatic Aspects of Type-Directed Partial Evaluation. Technical Report. BRICS Report Series RS-96-15. 27 pages.
[4] Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In
Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP 1990, Nice, France, 27-29 June 1990. 151–160. https://doi.org/10.1145/91556.91622[5] Rowan Davies. 1996. A Temporal-Logic Approach to Binding-Time
Analysis. In Proceedings, 11th Annual IEEE Symposium on Logic in
Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996.
184–195. https://doi.org/10.1109/LICS.1996.561317[6] Xavier Leroy et al. 2019. Chapter 21. Optimisation with Flambda.
The OCaml system release 4.09. (2019). https://caml.inria.fr/pub/docs/
manual-ocaml/flambda.html[7] Jun Inoue, Oleg Kiselyov, and Yukiyoshi Kameyama. 2016. Staging
beyond terms: prospects and challenges. In Proceedings of the 2016 ACM
SIGPLAN Workshop on Partial Evaluation and Program Manipulation,
PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. 103–108.
https://doi.org/10.1145/2847538.2847548[8] Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan. 2011.
Shifting the stage - Staging with delimited control. J. Funct. Program.
21, 6 (2011), 617–662. https://doi.org/10.1017/S0956796811000256[9] Oleg Kiselyov. 2012. Delimited control in OCaml, abstractly and concretely. Theor. Comput. Sci. 435 (2012), 56–76. https://doi.org/10.1016/j.
tcs.2012.02.025[10] Oleg Kiselyov. 2015. Generating Code with Polymorphic let: A Ballad of Value Restriction, Copying and Sharing. In Proceedings ML
Family / OCaml Users and Developers workshops, ML Family/OCaml
2015, Vancouver, Canada, 3rd & 4th September 2015. 1–22. https://doi.org/10.4204/EPTCS.241.1[11] Oleg Kiselyov. 2017. Let-insertion as a primitive. (2017). http://okmij.
org/ftp/ML/MetaOCaml.html#genlet

PEPM ’20, January 20, 2020, New Orleans, LA, USA[12] Xavier Leroy. 2000. A modular module system. J. Funct. Program. 10, 3(2000), 269–303. http://journals.cambridge.org/action/displayAbstract?
aid=54525[13] Gabriel Radanne, Thomas Gazagnaire, Anil Madhavapeddy, Jeremy
Yallop, Richard Mortier, Hannes Mehnert, Mindy Preston, and David J.
Scott. 2019. Programming Unikernels in the Large via Functor Driven
Development. CoRR abs/1905.02529 (2019). arXiv:1905.02529 http://arxiv.org/abs/1905.02529[14] Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth,
Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov,Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel,and Kunle Olukotun. 2015. Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems. In 1st Summit
on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015,
Asilomar, California, USA. 238–261. https://doi.org/10.4230/LIPIcs.
SNAPL.2015.238[15] Kenichi Suzuki, Oleg Kiselyov, and Yukiyoshi Kameyama. 2016. Finally,safely-extensible and efficient language-integrated query. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and
Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20- 22, 2016. 37–48. https://doi.org/10.1145/2847538.2847542[16] Takahisa Watanabe. 2017. Program Generation for ML Modules. (2017).
http://logic.cs.tsukuba.ac.jp/~takahisa/module-generation.html[17] Takahisa Watanabe and Yukiyoshi Kameyama. 2018. Program generation for ML modules (short paper). In Proceedings of the ACM SIGPLAN
Workshop on Partial Evaluation and Program Manipulation, Los Angeles,
CA, USA, January 8-9, 2018. 60–66. https://doi.org/10.1145/3162072[18] Jeremy Yallop. 2016. Staging generic programming. In Proceedings ofthe 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program
Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016.
85–96. https://doi.org/10.1145/2847538.2847546[19] Jeremy Yallop and Oleg Kiselyov. 2019. Generating mutually recursive definitions. In Proceedings of the 2019 ACM SIGPLAN Workshop
on Partial Evaluation and Program Manipulation, PEPM@POPL 2019,
Cascais, Portugal, January 14-15, 2019. 75–81. https://doi.org/10.1145/
3294032.3294078[20] Jeremy Yallop and Leo White. 2015. Modular macros. OCaml Usersand Developers Workshop. (2015).