Type-Safe Generation of Modules inApplicative and Generative Styles
Yuhi Sato

Yukiyoshi Kameyama

yuhi@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

Abstract

1

The MetaML approach for multi-stage programming provides the static guarantee of type safety and scope safety
for generated code, regardless of the values of static parameters. Modules are indispensable to build large-scale programs in ML-like languages, however, they have a performance problem. To solve this problem, several languages
proposed recently allow one to generate ML-style modules.
Unfortunately, those languages had the problems of limited
expressiveness, incomplete proofs, and code explosion.
This paper proposes two-stage programming languages
for module generation, which solve all the above issues. Ourlanguages accommodate two styles: first-class modules withgenerative functors and second-class modules with applicative functors. Module generation in both styles is shown tohave their own merits by concrete examples. We present
type systems, and type-preserving translations from our languages to plain MetaOCaml. We also show the results ofperformance measurements, which confirms the effectiveness of our languages.

Modules provide a high-level abstraction mechanism to programming languages. They are indispensable to build largescale programs in ML-family languages, just like classes inmany object-oriented languages, and type classes in Haskell.
Coq1 and MirageOS2 are two successful examples of largescale applications in OCaml, a dialect of ML-family languages, both of which extensively use modules. While modules are useful as building blocks of large programs and allow
separate compilation, the independent nature of modules
sometimes has a performance problem, as a function call ina different module needs indirection. Although each software system including MirageOS solves this problem in its
own way, a uniform and natural solution is called for, andseveral authors proposed to apply the program-generation
technique to modules to improve the performance.
Program generation, or multi-stage programming, is toseparate the execution of programs into two or more stages.
At the first stage, code is generated, and at the second stage,
the generated code is executed. The result of the second
stage may also be code, and the same pattern may continue
at the third and later stages. The generated code at earlier
stages can be specialized in some input data (static data).
The merit of this separation is that the specialized code withthe other input data (dynamic data) is expected to run fasterthan the original, unspecialized code. Among various studies
on program generation, the MetaML approach [16, 19] uses
quasi-quotation to represent generated code, and focuses
on giving the static guarantee of type safety of any generated code. MetaOCaml3 , a multi-stage extension of OCaml,
is one of the most successful languages in the MetaML-styleprogram generation [10, 17]. MetaOCaml allows the generation of terms only, since the foundational type theory for
MetaML-style languages [8, 18] targets them only.
This paper addresses the efficiency problem for ML-style
modules, and proposes two languages that allow generation of ML-style modules in a type-safe way. We are not
the first to propose such a language. Inoue et al. [9] were
the first to argue an imaginary extension of MetaOCaml
which allows generating code of modules. Later, Watanabe
et al. [20] and Sato et al. [15] proposed concrete languages

CCS Concepts: • Software and its engineering → General programming languages.
Keywords: Program Generation, Modules, Type Safety, Program Transformation
ACM Reference Format:
Yuhi Sato and Yukiyoshi Kameyama. 2021. Type-Safe Generationof Modules in Applicative and Generative Styles. In Proceedingsof the 20th ACM SIGPLAN International Conference on Generative
Programming: Concepts and Experiences (GPCE ’21), October 17–
18, 2021, Chicago, IL, USA. ACM, New York, NY, USA, 13 pages.
https://doi.org/10.1145/3486609.3487209
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 notmade or distributed for profit or commercial advantage and that copies bear
this notice and the full citation on the first page. Copyrights for componentsof this work owned by others than ACM must be honored. Abstracting withcredit is permitted. To copy otherwise, or republish, to post on servers or toredistribute to lists, requires prior specific permission and/or a fee. Request
permissions from permissions@acm.org.
GPCE ’21, October 17–18, 2021, Chicago, IL, USA© 2021 Association for Computing Machinery.
ACM ISBN 978-1-4503-9112-2/21/10. . . $15.00
https://doi.org/10.1145/3486609.3487209

Introduction

1 https://coq.inria.fr
2 https://mirage.io
3 http://okmij.org/ftp/ML/MetaOCaml.html

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

for generating and manipulating code of modules as well as
implemented the language, and showed that applying program generation to ML-style modules reduces the overheadof modules for several examples. Sato et al. solved a code
explosion problem in Watanabe et al.’s study that the size ofgenerated code may increase exponentially in certain programs. Unfortunately, these proposals are premature, andhave several problems. First, they are implemented by translating to MetaOCaml, however, no formal properties on thetranslations, such as type preservation, were proved. Hence,
it is not certain whether all terms in their languages aretranslated. Second, while their languages can generate firstclass modules with generative functors, there exist examples
that need module generation with second-class modules andapplicative functors, which are the standard functors in thecurrent OCaml. Finally, several important features in modular programming such as abstract types and nested modules
are not supported by existing languages.
In this paper, we propose two programming languages
and study their type-theoretic foundation, which solve theabove problems. Namely, our languages allow one to generate ML-modules in the applicative style with second-classmodules, and in the generative style with first-class modules.
We show that there is a useful program which can be written
in the applicative style, but not in the generative style. We
formalize a type system for the language in the applicative
style, and show that a translation from it to plain MetaOCaml
preserves typing. The translation is implemented on top of
MetaOCaml, and our experiment shows that both the performance problem by module separation and the code explosion
problem are resolved by our system.
Various works in the literature proposed languages forgenerating high-level abstractions such as modules. Racket’s
module system with submodules [7] is one of the closest toours, which enables phase separation for language extensions, and coexists with the hygienic macro system. Ourlanguages are hygine, and have nested modules and phaseseparation, hence they share many features. A major difference between the two is that we take the purely generative4
approach, which allows us to prove the static assurance oftype safety5 for all generated code. In fact, types help a lot incode generation, and abstract types are key for the abstractions by ML-style modules. In this paper, we devote ourselves
to build a type-theoretic foundation of our languages to eliminate the problems above, and to our knowledge, this paper
gives the first type system for module generation, which
has a complete definition and a translation to MetaOCaml.
It is an interesting future work to investigate how our languages can be used for language extensions as studied in theliterature.
4 In the purely generative language, once code values are generated, theycannot be inspected or analyzed.
5 Strictly speaking, type safety holds for our language without the run
primitive.

Yuhi Sato and Yukiyoshi Kameyama

Our contribution is summarized as follows.
• We define two languages that allow module generationin two stages. The first one has first-class modules andgenerative functors as in the existing works, while thesecond one has second-class modules and applicative
functors, which has never been studied as the targetof module generation in the literature.
• Our languages have important features in ML-style
modular programming such as abstract types and nested modules, which are missing in the earlier works.
• By concrete examples, we show that module generation in the applicative style is useful to eliminate
indirect calls beyond module boundaries.
• We formulate precise type systems for our languages.
The traditional type system for applicative functors
has involved typing rules to cope with paths, and we
successfully generalize it to the two-stage language formodule generation. We prove that translations fromour languages to plain MetaOCaml preserve typing.
• We implement the translations, and conduct the performance measurements, which show that our two
languages can eliminate the overhead of functor applications and are free from code explosion.
The rest of this paper is organized as follows: Section
2 explains several important concepts about ML-modules.
Section 3 shows concrete examples written in our languages
and explains how our languages are useful in writing codeand improving efficiency. Section 4 formally introduces ourlanguages and their type systems, and Section 5 gives typepreserving translations to plain MetaOCaml. Section 6 shows
the results of experiments on a microbenchmark. Section 7
states the related work, and Section 8 gives conclusion andfuture work.

2

Background: ML-modules

Modules are a language feature in OCaml to package relevant
definitions and separate specifications and implementations,which allow us to develop large-scale applications in a typesafe way that achieves reusability and maintainability. Thissection illustrates the basics and key features of modules by
examples.
2.1

Structures

Structures correspond to implementations of modules, which
are defined by a sequence of components. The components
consist of definitions of types, values, and modules.
Figure 1 shows an example of a structure that represents a
set of integers. The structure IntSet is defined by the expression struct ... end, and has two type components, elt_t and
set_t, that represent the type of the element and the type ofthe set, respectively. In this case, the type elt_t is definedas the type int, and the set_t is defined as the list of elt_t.

Type-Safe Generation of Modules inApplicative and Generative Styles

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

module IntSet =structtype elt_t = int
type set_t = elt_t list
let rec member elt set =match set with
| []→ false| hd :: tl → elt = hd|| member elt tl
end

module type EQ =sigtype tval eq : t → t → boolend
module MakeSet ( Eq : EQ ): SET =structtype elt_t = Eq .t
type set_t = elt_t list
let rec member elt set =match set with
| []→ false| hd :: tl → Eq . eq elt hd|| member elt tl
end

Figure 1. Structure for the Set Module
module type SET =sigtype elt_ttype set_t
val member : elt_t → set_t → bool
end

Figure 3. Functor for Set
module IntEq : EQ =structtype t = int
let eq x y = Int . equal x y
end
module StringEq : EQ =structtype t = string
let eq x y = String . equal x y
end
module IntSet = MakeSet ( IntEq )module StringSet = MakeSet ( StringEq )Figure 2. Signature for the Set Module
In addition, it has the value component member which returns whether the argument set contains the argument elt.
Components can be referenced from outside the structureby the dot notation. For example, we write IntSet.member
to refer to the function member. Module structures may be
simply called modules.
2.2

Signatures correspond to a specification, or an interface, ofmodules. Signatures achieve data abstraction to eliminate
programs that depend on an implementation of modules.
Therefore, signatures make it easy to modify or replace animplementation of modules, which improves the maintainability of programs.
Continuing with the example in Figure 1, users of IntSet
should not know the implementation details. To hide thefact that the set is implemented by the list, we can define thesignature SET for the structure IntSet as shown in Figure
2. The signature SET is defined by the expression sig ... end,
which contains a sequence of specifications for the components in the IntSet. elt_t and set_t are abstract types thathide an implementation of corresponding type components.
The function member takes values of types elt_t and set_t,
and returns a value of type bool.
A structure can be sealed in OCaml. For instance, by defining module IntSet’ = (IntSet : SET), the equivalence
IntSet’.elt_t = int does not hold.
2.3

Figure 4. Integer Set and String Set by Functor

Signatures

Functors

Functors are modules parameterized by modules and correspond to functions over modules, which achieve reusability.
Figure 3 shows an example of a functor that makes a moduleof sets. The signature EQ has the type component t, and thefunction eq, which is intended to be an equality function
over the type t. The functor MakeSet takes a module Eq withthe signature EQ, and creates a SET module using Eq as theelements of the set. Figure 4 re-defines the structure IntSet
in Figure 1 by applying the functor MakeSet to IntEq. IntEq
is a structure that contains the concrete components for integers, sealed with EQ. We can get another SET structure by
applying MakeSet to another structure with the signature
EQ. StringSet is obtained by applying MakeSet to a string
structure.
2.4

Modules vs Classes

ML-style modules provide a useful abstraction to programs,
just as classes in object-oriented languages do. However,there are significant differences between the two.
The first, and most notable, difference is that classes canhave states, while modules without side effects cannot. In
ML, stateful objects should be created by another means.
Another difference is that the signature of a module canhave abstract types. The signature SET in Figure 2 has thetype components elt_t and set_t, which are left unspecified. They can be used in SET as if they are actual types.

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Yuhi Sato and Yukiyoshi Kameyama

module type SYMBOL_TABLE =sigtype symbol
val string2symbol : string → symbol
val symbol2string : symbol → string
end
module SymbolTable () : SYMBOL_TABLE =structtype symbol = int
let table =(* allocate internal hash table*)
Hashtbl . create initial_size
let string2symbol x =(* lookup ( or insert ) x *)let symbol2string n =match Hashtbl . find table n with| Some x → x| None→raise ( Failure " bad symbol " )endmodule ST1 = SymbolTable ()module ST2 = SymbolTable ()Abstract types make it possible to write many interesting
programs or programming patterns such as modular implicits [21], and tagless-final embedding [2].
2.5

Generative Functors vs Applicative Functors

Two semantics for functors have been studied in the literature [4]. Generative functors are standard in Standard ML:
for a functor 𝐹 and a module 𝑀, applying 𝐹 to 𝑀 twice(i.e. 𝐹 (𝑀) twice) would generate modules whose signatures
are not compatible. A canonical example for the usefulnessof this semantics is the functor SymbolTable in Figure 5,
which is taken from Dreyer’s thesis [4]. This example represents a symbol table implemented with a hash table. The
signature SYMBOL_TABLE hides a concrete type of the symbol
and an internal hash table, and exposes two components:
string2symbol and symbol2string to interconvert between
symbol and string. The generative functor SymbolTable
makes a structure sealed with SYMBOL_TABLE. The parenthesis () is used to specify a generative functor in OCaml. The
components string2symbol and symbol2string access tothe internal hash table table. The notable point lies in theimplementation of symbol2string. The exception Failure
should never be raised while the symbol n is obtained bystring2symbol in the same structure, as the corresponding string can be found in the table. In generative semantics, type checking can guarantee that no exceptions will
be raised. For example, assuming the structures ST1 andST2 instantiated by the functor SymbolTable, ST1.symbol
is not equal to ST2.symbol. Thus, a symbol obtained by
ST2.string2symbol is never given to ST1.symbol2string.
On the other hand, applicative functors are standard in
OCaml: applying 𝐹 to 𝑀 twice would always generate modules whose signatures are compatible. The functor MakeSet
in Figure 3 is appropriate for applicative semantics. For example, assuming two structures generated by the same functor
application MakeSet(IntEq), since they have the same typeand equality function for integers, there is no reason to distinguish them.
2.6

First-Class Modules vs Second-Class Modules

In ML, the module language exists in a separate layer fromthe core language for expressions, and hence modules aresecond-class objects. There is an extension of ML that treats
modules as ordinary values, which are called first-class modules. First-class modules allow one to dynamically dispatcha module with conditional expressions and define a functionthat takes a module and returns it. Functions over first-classmodules need to have generative semantics in the sense thatthe modules returned by applying such functions to firstclass modules must have fresh signatures, that cannot be
equal to other signatures.
OCaml (MetaOCaml) supports both first- and second-classmodules. Second-class modules are packed into first-classmodules and unpacked from first-class modules. OCaml uses

Figure 5. Symbol Table
the syntax (module m:S) to pack the module m with thesignature S into a value of type (module S), and the syntax(val m) unpacks m to a module. Components inside firstclass modules can only be accessed via unpacked modules.

3

Examples of Module Generation

This section shows concrete examples of module generationin the languages for applicative functors with second-classmodules, and the one for generative functors with first-classmodules. We will show different examples for each language,
which reveals the merits of each language.
3.1

Examples with Applicative Functors andSecond-Class Modules

We show examples in the language with applicative functors and second-class modules, which is called 𝜆 <𝐴> (𝐴 for
applicative).
Our first example is MakeSet, the standard example for
ML-modules. To manipulate and generate code of modules,
𝜆 <𝐴> provides two multi-stage constructors in addition to
the constructors added to Watanabe et al.’s language. To illustrate these constructors, we first give an example of the
MakeSet program in 𝜆 <𝐴> (Figure 6). Following Watanabe etal.’s language, our 𝜆 <𝐴> provides a constructor $ to extract
code of a component from code of a module. For instance, if
Eq is code of a module that has a value component eq of type
𝜏, then ($Eq).eq is the code of this value component of type𝜏 code. Similarly, we can extract the type component: suppose Eq is code of a module that contains a type componentt = int, ($Eq).t refers to the type int.

Type-Safe Generation of Modules inApplicative and Generative Styles

module MakeSet =functor ( Eq : EQ mcod ) →⟨⟨ ( structtype elt_t = $Eq .t
type set_t = elt_t list
let rec member elt set =match set with
| []→ false| hd :: tl → ~( $Eq . eq ) elt
hd || member elt tl
end : SET ) ⟩⟩module IntEq =⟨⟨ ( structtype t = int
let eq = (=)
end : EQ ) ⟩⟩module IntSet = Runmod ( MakeSet ( IntEq ): SET )

Figure 6. MakeSet Functor in 𝜆 <𝐴>
module MakeSet =functor ( Eq : EQ ') →( structtype elt_t = Eq .t
type set_t = elt_t list
let member = genlet< let rec member elt set =match set with
| []→ false| hd :: tl → ~( Eq . eq ) elt hd|| member elt tl
in member >end : SET ')module IntEq =( structtype t = int
let eq = genlet <(=) >end : EQ ')module IntSet =structmodule X = MakeSet ( IntEq )type elt_t = X. elt_ttype set_t = X. set_t
let member = Runcode . run X. member
end

Figure 7. MakeSet Translated from 𝜆 <𝐴> to MetaOCaml
The key point in 𝜆 <𝐴> is to distinguish code of modules
from code of core expressions to avoid expressions that cannot be translated. To do so, we introduce a type mcod, brackets ⟨⟨⟩⟩, and an escape ≈, for code of modules. For example,
assuming a structure 𝑚 has the type 𝑀, ⟨⟨𝑚⟩⟩ has the type
𝑀 mcod. Furthermore, if 𝑋 is bound to ⟨⟨𝑚⟩⟩, then 𝑋 canbe spliced into other code of a module such as ⟨⟨...(≈ 𝑋 )...⟩⟩.
Continuing with the example in Figure 6, MakeSet has thetype functor(Eq: EQ mcod) -> SET mcod, and IntEq has

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

the type SET mcod. The result of the functor application
MakeSet(IntEq) is given to Runmod, then IntSet has thetype SET.
Figure 7 shows a program translated from Figure 6, where
the definitions of SET’ and EQ’ are omitted. Through thetranslation, constructors for module generation are eliminated as the genlet primitive is inserted into the body of thecomponent member. The role of genlet in the latest MetaOCaml6 is to perform let-insertion to share generated code.
Sato et al. [15] proposed to use genlet to avoid code explosion.
Our second example shows the usefulness of applicative
functors. We borrow an example from Leroy’s paper [11],which implements dictionaries by a functor MakeDict:module type DICT =sigtype key
type 'a dictval empty : 'a dictval add : key → 'a → 'a dict → 'a
dictval find : key → 'a dict → 'aend
module MakeDict =functor ( Key : EQ ) →( structtype key = Key .t
type 'a dict = ( key * ' a) list...
end : DICT )The parameter Key of MakeSet is the key of this dictionary.
We can extend the functor with the operation domain that
returns the set of keys of a dictionary. The simplest way
is to make a module for the set of keys inside the functor
MakeDict using the functor MakeSet:
module MakeDict =functor ( Key : EQ ) →( struct...
module KeySet = MakeSet ( Key )let domain dict =.. KeySet . member ..
end : DICT )To eliminate the abstraction overhead of functor applications,
we can rewrite the above program in 𝜆 <𝐴> as follows:
module MakeDict =functor ( Key : EQ mcod ) →⟨⟨ ( struct...
module KeySet = ≈ ( MakeSet ( Key ) )let domain dict =.. KeySet . member ..
end : DICT ) ⟩⟩6 http://okmij.org/ftp/ML/MetaOCaml.html

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Suppose functors are given the generative semantics, thenthe set of keys returned from domain cannot be used withother sets obtained by applying MakeSet to the same module
for an element type. The types of their sets are incompatible.
For example, we consider a functor MakePrioQueue implementing priority queues that use sets in the same way as
MakeDict.
module MakePrioQueue =functor ( Elt : EQ mcod ) →⟨⟨ ( structtype elt = Elt .t
type queue = elt list
module EltSet = ≈ ( MakeSet ( Elt ))let contents queue =(* set of elements in queue *)...
end : PRIOQUEUE ) ⟩⟩Then, we give the module IntEq to the two functors:
module IntDict =Runmod ( MakeDict ( IntEq ): DICT )module IntPrioQueue =Runmod ( MakePrioQueue ( IntEq ):PRIOQUEUE )IntDict and IntPrioQueue contain the same set of integers,
but the types of their sets are not compatible. Therefore, thefollowing expression causes a type error.
IntDict . domain d =IntPrioQueue . contents q

A possible solution to this problem is to hoist MakeSetfrom MakeDict and MakePrioQueue, and to share the functor application MakeSet(IntEq). In this case, MakeDict and
MakePrioQueue take an extra argument for the set hoisted
out, in addition to the argument Key (or Elt). Unfortunately,
this solution has some problems:• All programs that use MakeDict or MakePrioQueuerequire modifications to the functor arguments, even
if some programs do not use the operations on thesets.
• Hoisting the functor application MakeSet(IntEq) to
a common point requires a non-local program transformation.
In applicative semantics, there are no such problems. Therefore, we think that applicative functors are useful for module generation. Besides the above merit, since applicative
functors and second-class modules are common in OCaml,
existing OCaml programs can be staged with a little cost if
one works in 𝜆 <𝐴> .
3.2

Examples with Generative Functors andFirst-Class Modules

In this subsection, we show examples that use generative
functors and first-class modules. We call the language as

Yuhi Sato and Yukiyoshi Kameyama

𝜆 <𝐺 > (𝐺 for generative), which is a refined version of ourpredecessors [15, 20]. The most useful aspect of 𝜆 <𝐺 > is thata program can choose code of modules. Figure 8 shows a
program where an implementation of a logger is dynamically dispatched to the main application depending on acommand-line argument. In this example, there are only two
choices: consoleLogger for printing logs to a console, or
fileLogger for writing logs to a file.
For this setting, we may be able to generate the main
application inlined for all possible combinations at compiletime, such as consoleLogApp and fileLogApp. In general,
however, applications have many runtime parameters suchas command-line arguments, and due to combinatorial explosion, it is difficult to generate all possible combinations
at compile time. Hence, generating code of modules at runtime is useful for specializing applications which have many
parameters.
Another aspect to be noted is that the abstraction overhead
can be eliminated from programs suitable for generative
functors such as the example of SymbolTable in Section 2.5.
Functors represented as ordinary functions return modules
with fresh abstract types.
𝜆 <𝐺 > provides two multi-stage constructors for modules
in addition to Watanabe et al.’s $ and run_module. One is
the type mcod for code of modules. The other is brackets⟨⟨⟩⟩ for modules. Note that escapes for modules are not introduced because the syntax becomes too complex. Since
traditional MetaOCaml can generate code of expressions,
one might think that a language for generating first-classmodules can be implemented as a lightweight extension to
MetaOCaml. Unfortunately, it is not the case for Watanabe etal.’s translation and ours, since code of ordinary expressions
and code of modules have different semantics, and they need
to be distinguished.
Figure 9 shows the MakeSet functor expressed in 𝜆 <𝐺 > . It
is translated to the program in Figure 10 by our translation.
There is a trade-off between 𝜆 <𝐴> and 𝜆 <𝐺 > . In the language 𝜆 <𝐴> , the dictionary example in the previous section
can be expressed. However, it does not allow a program thatdynamically selects a module to be specialized, since dependencies between second-class modules are solved statically.
𝜆 <𝐺 > is opposite to 𝜆 <𝐴> . OCaml supports the two styles
in a single language, and this paper is the first to propose alanguage extension of module generation for both styles.

4

Proposed Languages

We propose two languages for module generation. Due tospace limitations, we present the language 𝜆 <𝐴> here. Readers are encouraged to refer to the full version of this paper7 .
The language 𝜆 <𝐴> is a two-stage language as an extension of core MetaOCaml plus module generation. It has ordinary simply-typed lambda terms, second-class modules, and
7 http://logic.cs.tsukuba.ac.jp/~yuhiType-Safe Generation of Modules inApplicative and Generative Styles

module type LOG =sigval info : string → unit
val error : string → unit
end
let consoleLogger =⟨⟨ ( module struct
let print level msg =Printf . printf " [% s] %s\n" levelmsg
let info msg = print " INFO " msg
let error msg = print " ERROR " msg
end : LOG ) ⟩⟩let fileLogger =⟨⟨ ( module struct...
end : LOG ) ⟩⟩let makeApp ( logger : ( module LOG )mcod ) =⟨⟨ ( module struct
let start () =~( $logger . info ) " Start app ";...
end : APP ) ⟩⟩let () =let logger =if Sys . argv .(1) = " console " thenconsoleLogger
else fileLogger in
let app = makeApp logger in
let module App = ( val ( run_module
app : APP )) in
App . start () ;;Figure 8. Choosing Logger Depending on Runtime Options
let makeSet ( eq : ( module EQ ) mcod )=⟨⟨ ( structtype elt_t = $eq .t
type set_t = elt_t list
let rec member elt set =match set with
| []→ false| hd :: tl → ~( $eq . eq ) elt hd|| member elt tl
end : SET ) ⟩⟩module IntSet = ( val ( run_module( makeSet ⟨⟨ ( module structtype t = int
let eq = (=)
end : EQ ) ⟩⟩ )))Figure 9. MakeSet Functor in 𝜆 <𝐺 >multi-stage constructors for code generation. The design ofthe language is based on Leroy’s applicative-functor calculus[11], the classic type system 𝜆◦ [3], and Watanabe et al.’s
calculus [20]. We confine ourselves to a minimal language toexpress our results. Extending our language by more features

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

let makeSet ( eq : ( module EQ ') ) =( structmodule Eq = ( val eq )type elt_t = Eq .t
type set_t = elt_t list
let member = genlet< let rec member elt set =match set with
| []→ false| hd :: tl → ~( Eq . eq ) elt hd|| member elt tl
in member >end : SET ')module IntSet = ( val( module structmodule S =( val ( makeSet ( module structtype t = int
let eq = genlet <(=) >end : EQ ') ))type elt_t = S. elt_ttype set_t = S. set_t
let member = run S. member
end : EQ ))Figure 10. MakeSet Translated from 𝜆 <𝐺 > to MetaOCamlsuch as sharing constraints and computational effects is left
for future work.
4.1

SyntaxFigure 11 defines the syntax for terms in 𝜆 <𝐴> . We use
metavariables 𝑚 for module expressions, 𝑠 for a sequence ofstructure components, 𝑐 for structure components, 𝑝 for access paths, 𝑒 for core expressions, and 𝑃 for programs. Also,
𝑥, 𝑡, and 𝑋 are names for values, types, and modules, respectively. Duplicate component names are prohibited by typing
rules. In this language, base types and primitives are unspecified. Complete programs 𝑃 are sequences of structure components. For simplicity, we sometimes omit prog and end
in program examples.
We introduce brackets ⟨⟨⟩⟩, an escape ≈, and Runmod,
for module expressions. Since the module expressions aresecond class, which means that they exist on a different layer
than that of the terms. the multi-stage constructors for themshould be distinguished from those for terms, which are<>, ∼, and run. Following Watanabe et al.’s calculus, we
introduce the $ constructor to extract a component containedin code of a module as code. For example, $𝑝.𝑥 extracts thevalue component 𝑥 as code from code of a module accessedwith the path 𝑝, and its code can be spliced into other code.
$𝑝.𝑥 reads $(𝑝).𝑥. A functor definition and a restriction by asignature are defined by functor (𝑋 : 𝑀) → 𝑚 and (𝑚 : 𝑀),
respectively. They use unfamiliar syntax for Camel users, but
OCaml supports them. The key to applicative functors is thatthe access paths include a path application 𝑝 1 (𝑝 2 ), which

GPCE ’21, October 17–18, 2021, Chicago, IL, USA𝑚 ::= 𝑋 | 𝑝.𝑋 | struct 𝑠 end | (𝑚 : 𝑀) | 𝑚 (𝑝)| functor (𝑋 : 𝑀) → 𝑚| ⟨⟨𝑚⟩⟩ | ≈ 𝑚 | Runmod (𝑚 : 𝑀) | $𝑝.𝑋
𝑠 ::= 𝜖 | 𝑐 𝑠
𝑐 ::= let 𝑥 : 𝜏 = 𝑒 | type 𝑡 = 𝜏 | module 𝑋 = 𝑚
𝑝 ::= 𝑋 | 𝑝.𝑋 | 𝑝 1 (𝑝 2 ) | $𝑝.𝑋
𝑒 ::= 𝑥 | 𝑝.𝑥 | < 𝑒 > | ∼ 𝑒 | run 𝑒 | $𝑝.𝑥
| fun 𝑥 → 𝑒 | 𝑒 𝑒 | let 𝑥 = 𝑒 in 𝑒
Figure 11. Syntax of terms

𝑀 ::= sig 𝑆 end | functor (𝑋 : 𝑀1 ) → 𝑀2 | 𝑀 mcod
𝑆 ::= 𝜖 | 𝐶 𝑆
𝐶 ::= val 𝑥 : 𝜏 | type 𝑡 | type 𝑡 = 𝜏 | module 𝑋 : 𝑀
𝜏 ::= 𝑡 | 𝑝.𝑡 | 𝜏 → 𝜏 | 𝜏 code | $𝑝.𝑡
Figure 12. Syntax of types

is needed to test type equality among modules obtained byfunctor applications. Along with this, the syntax of a functor
application 𝑚(𝑝) is restricted to a path argument only.
4.2

Type System

Figure 12 defines the syntax of types. The syntax of types
is standard except the following. We use metavariables 𝑀
for module types, 𝑆 for a sequence of signature components,
𝐶 for signature components, and 𝜏 for types of core expressions. We introduce the type 𝑀 mcod to distinguish code ofmodules from code of core expressions. The signature components include an abstract type component (type 𝑡) anda manifest type component (type 𝑡 = 𝜏). The $𝑝.𝑡 refers
to the type component 𝑡 within code of a module specified
with the path 𝑝. Our language has no explicit syntax for
embedding types to code of a module, which is contrastingto Watanabe et al.’s language.
The typing environment 𝐸 is a possibly empty sequenceof signature components 𝐶 annotated with a level 𝑙. Since
𝜆 <𝐴> is a two-stage language, 𝑙 is either 0 or 1. The othertyping environment Δ is a subsequence of 𝐸. It is used in thetranslation only, and explained later.
The first group of typing judgment consists of ⊢ 𝑃 wt
for well typedness of 𝑃, and 𝐸; Δ ⊢𝑙 𝑀 wf, 𝐸; Δ ⊢𝑙 𝑆 wf,
𝐸; Δ ⊢𝑙 𝐶 wf, and 𝐸; Δ ⊢𝑙 𝜏 wf for well formedness. They
claim that the target types or expressions are well typed orwell formed under the assumptions 𝐸; Δ at the stage 𝑙. We
omit the definition in this paper.
The second group of judgements consist of 𝐸; Δ ⊢𝑙 𝑒 : 𝜏for an expression 𝑒 of type 𝜏, 𝐸; Δ ⊢𝑙 𝑚 : 𝑀 for a module

Yuhi Sato and Yukiyoshi Kameyama

expression 𝑚 of module type 𝑀, and 𝐸; Δ ⊢𝑙 𝑠 : 𝑆 for astructure 𝑠 with signature 𝑆. Most typing rules to derive a
judgment 𝐸; Δ ⊢𝑙 𝑒 : 𝜏 are standard in the type systems for
MetaML-like languages [1, 18]. Nevertheless, we explain therules for basic multi-stage constructs < 𝑒 >, ∼ 𝑒, and run 𝑒
shown below.
𝐸; Δ ⊢1 𝑒 : 𝜏(E-C)
𝐸; Δ ⊢0 < 𝑒 > : 𝜏 code

𝐸; Δ ⊢0 𝑒 : 𝜏 code
(E-E)
𝐸; Δ ⊢1 ∼ 𝑒 : 𝜏The rule E-C assigns the type 𝜏 code to the code expression< 𝑒 > if 𝑒 has type 𝜏. The levels of judgments are used to
distinguish level-1 expressions, such as 𝑒 in this rule, fromlevel-0 expressions, such as < 𝑒 >. The rule E-E is opposite
to E-C; the ’escape’ expression ∼ 𝑒 splices the code value of𝑒 into another code. For example, we can derive·; · ⊢0 let 𝑥 = < 3 > in <∼ 𝑥 + 7 > : int code
assuming that integer constants and addition are added,
We did not introduce environment classifiers [18] to keep
our type system compact. As a drawback, the scope-extrusion
problem may occur; the run-expression may receive an open
code as the value of 𝑒, causing a runtime error. However, it
should not be difficult to include environment classifiers in
our type system.
The judgment for module expressions 𝐸; Δ ⊢𝑙 𝑚 : 𝑀 has
the following typing rules for multi-stage constructors:
𝐸; Δ ⊢0 𝑚 : 𝑀 mcod
𝐸; Δ ⊢1 𝑚 : 𝑀
(M-E)
(M-C)
0
𝐸; Δ ⊢1 ≈ 𝑚 : 𝑀
𝐸; Δ ⊢ ⟨⟨𝑚⟩⟩ : 𝑀 mcod

The rule M-C assigns a type to code of a module ⟨⟨𝑚⟩⟩, and therule M-E to a splice of a module ≈ 𝑚. They are quite similar
to the counterpart rules E-C and E-E for core expressions.
The following rule M-R assigns a type to a run expression
for modules:
𝐸; Δ ⊢0 𝑚 : 𝑀 mcod
(M-R)
𝐸; Δ ⊢0 Runmod (𝑚 : 𝑀) : 𝑀
Our type system has a few involved rules.
The first one is the typing rule for the $-operator:
𝐸; Δ ⊢0 𝑝 : (sig 𝑆 1 (val 𝑥 : 𝜏) 𝑆 2 end) mcod
𝐸; Δ ⊢0 $𝑝.𝑥 : 𝜏 ′ code

(E-DotCode)To understand the rule, assume 𝜏 ′ = 𝜏. Then, the rule saysthat given 𝑝 of a module-code type and 𝑥 has type 𝜏 in themodule, $𝑝.𝑥 has the type 𝜏 code. This reflects our intention
that the $-operator converts code of a module to a module
consisting of code values. In the precise formulation, 𝜏 ′ is
𝜏 [𝑧 ← $𝑝.𝑧 | 𝑧 ∈ Dom(𝑆 1 )] code which involves a substitution; see Leroy’s calculus [11].
The second involved rule is the rule M-Strengthening
to derive the equivalence of module types:
𝐸; Δ ⊢0 𝑝 : 𝑀(M-Strengthening)
𝐸; Δ ⊢0 𝑝 : 𝑀/𝑝 0

Type-Safe Generation of Modules inApplicative and Generative Styles

The strengthening operation replaces abstract type components with manifest type components with a path. For
instance, assuming a module A has type sig type t end,
this operation translates its type to sig type t = A.t end.
Also, assuming the result type of functor application (pathapplication) F(A) is sig type t end, its strengthened typeis sig type t = F(A).t end. Intuitively, this operation
gives a module type an identity. We use a notation 𝑀/𝑝 𝑙 ,which is based on Leroy’s style [11], to strengthen the module type 𝑀 with the path 𝑝 at the level 𝑙. The level 𝑙 in 𝑀/𝑝 𝑙
is for the operation / rather than the path 𝑝, which plays therole of a flag that indicates whether it is inside mcod.
We emphasize that strengthening is needed for the applicative semantics only, which complicates the formal development, compared with the generative semantics. In themulti-stage languages, we need to consider the case when
the path 𝑝 contains the $-operator.
4.3

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

We first show an example of the translation. Consider thefollowing program written in 𝜆 <𝐴> .
module A = ⟨⟨ structtype t = int
let x:t = 1
module B = struct
val y:t = 2
end
end ⟩⟩
module A ' = Runmod (A : sig
type t = int
val x:tmodule B: sig
val y:tend
end )They are translated as follows:
module A = structtype t = int
let x:t code = <1>module B = struct
val y:t code = <2>
end
end
module A ' = structmodule X = A
type t = X.t
let x:t = run X.x
module B = structmodule Y = X.B
let y:t = run Y.y
end
end

Examples of Typing Derivation

We explain how the types for the modules and the functor
in Figure 6 is derived.
Let 𝐸 = (Eq : EQ mcod) 0 where EQ is the signature definedin Figure 3. The $-operator turns code of a module (EQ) to amodule consisting of code, hence we have:𝐸; · ⊢0 Eq : EQ mcod
→ 𝑡 → bool) code
1𝐸; · ⊢ ∼ ($Eq.eq) .: 𝑡 → 𝑡 → bool..
.
𝐸; · ⊢1 member : elt_t → elt_t list → bool
𝐸; · ⊢0 $Eq.eq : (𝑡In the last step of the above derivation, we used several
standard typing rules for terms. We also have all the typecomponents of MakeSet are suitably typed, and together
with the above derivation, we can derive the following type:
𝐸; · ⊢1 struct type elt_t = $Eq.t... end : SET
𝐸; · ⊢1 (struct type elt_t = $Eq.t... end : SET) : SET
𝐸; · ⊢0 ⟨⟨(struct type elt_t = $Eq.t... end : SET) ⟩⟩ : SET mcod

Then, we can derive ·; · ⊢0 MakeSet : EQ_SET_FUN where
EQ_SET_FUN is functor (Eq : EQ mcod) → SET mcod.
Similarly, we can derive the type for IntEq in Figure 6 as·; · ⊢0 IntEq : EQ mcod. By combining them, we can derive
the type for IntSet as follows:·; · ⊢0 MakeSet : EQ_SET_FUN 𝐸; · ⊢0 IntEq : EQ mcod·; · ⊢0 MakeSet(IntEq) : SET mcod·; · ⊢0 Runmod (MakeSet(IntEq) : SET) : SET

5

Translation to MetaOCaml

We define a translation from 𝜆 <𝐴> to plain MetaOCaml,
while we omit the one from 𝜆 <𝐺 > to plain MetaOCaml, which
is much simpler than the former.

In the translation, code of a module is translated to a module, and the type of its value components such as x translates
to a code type, for instance, int is translated to int code.
On the other hand, the type components do not change, forinstance, the abstract type t is equal to int before and after
the translation. The translation is applied recursively if codeof a module being translated has nested modules (e.g. B).
For Runmod(𝐴 : 𝑆), our translation expands all the components of 𝐴, and re-constructs a new module 𝐴 ′ by collecting
them after adding the run-primitive to the value components
such as run X.x.
5.1

Translation Rules

We explain the key rules of our translation. For a type 𝜏 anda level 𝑙, the translated type [[ 𝜏 ]]𝑙 is defined as follows:[[ 𝑡 ]]𝑙 = 𝑡[[ 𝑝.𝑡 ]]𝑙 = [[ 𝑝 ]]𝑙 . 𝑡[[ 𝜏1 → 𝜏2 ]]𝑙 = [[ 𝜏1 ]]𝑙 → [[ 𝜏2 ]]𝑙[[ 𝜏 code ]] 0 = [[ 𝜏 ]] 0 code

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Yuhi Sato and Yukiyoshi Kameyama[[ $𝑝.𝑡 ]]𝑙 = [[ 𝑝 ]]𝑙 . 𝑡which retrieves the 𝑥-component from the module 𝑋 , runs
it, and binds 𝑥 (in the new module) to its result. The runprimitive is propagated to nested modules shown below:

Essentially, types remain the same through the translation
except that the symbol $ is eliminated (in the last rule).
The translation for terms is denoted by [[ · ]]𝑙Δ , which isparameterized by the level 𝑙 (for 𝑙 = 0, 1) and the environment Δ explained later. The key rule for value components
is shown below:[[ let 𝑥 : 𝜏 = 𝑒 ]] 1Δ= let 𝑥 : [[ 𝜏 ]] 1 code = genlet < [[ 𝑒 ]] 1Δ >A value component at the level 1 is in a code of a module,
hence we change its type to a code type, and add the genlet
primitive to avoid the code-duplication problem.
For expressions, the translation is homomorphic for mostcases except the following rules:(∼ 𝑥 (𝑥 ∈ Dom(Δ))
1[[ 𝑥 ]] Δ =𝑥(𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒)(∼ ( [[ 𝑝 ]] 1 . 𝑥) (head(𝑝) ∈ Dom(Δ))[[ 𝑝.𝑥 ]] 1Δ =[[ 𝑝 ]] 1 . 𝑥(𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒)((module 𝑋 ′ : 𝑀) 𝑆)= (module 𝑋 = [[ Runmod (𝑋 . 𝑋 ′ : 𝑀) ]] 𝜖0 ) 𝑆[[ ⟨⟨𝑚⟩⟩ ]] 0Δ = [[ 𝑚 ]] 1Δ[[ ≈ 𝑚 ]] 1Δ = [[ 𝑚 ]] 0Δ

5.2

module 𝑋 = [[ 𝑚 ]] 0Δ
𝑆

𝑋

end
[[ $𝑝.𝑋 ]] 0Δ = [[ 𝑝 ]] 0 . 𝑋
The first rule translates code of a module to a module,
but the stage is raised to 1, reflecting the fact that 𝑚 is in
the code. The next rule eliminates the escape for code ofa module. The third rule translates a runmod-term whichis complicated. Its result depends on the signature 𝑆 of thetarget module since we need to build a new module. The
new module contains a nested module with a fresh nameand components. The expression 𝑆 𝑋 when 𝑆 is a value
component is defined as:((val 𝑥 : 𝜏) 𝑆)

𝑋 = (let 𝑥 : 𝜏 = run 𝑋 .𝑥) 𝑆

𝑋

Translation Preserves Typing

We can prove that the following form of simple type preservation holds for the translation. If 𝐸; Δ ⊢0 𝑒 : 𝜏 is derivablein our type system, then [[ 𝐸 ]] Δ ⊢0 [[ 𝑒 ]] 0Δ : [[ 𝜏 ]] 0 is
derivable. We assume the following two: First, the target
language is a subset of MetaOCaml, which is the same as
our language without multi-stage constructors for modules.
However, the type system in the target language is definedwithout the second environment Δ, which is obtained bysimply removing Δ from our type system. Second, the target
type system has a typing rule for genlet. The typing rule forgenlet is defined below.
𝐸 ⊢0 𝑒 : 𝜏 code
genlet 𝑒 : 𝜏 code

𝐸 ⊢0

Theorem 5.1. If 𝐸; Δ ⊢𝑙 𝑒 0 : 𝜏0 is derivable in 𝜆 <𝐴> , then[[ 𝐸 ]] Δ ⊢𝑙 [[ 𝑒 0 ]]𝑙Δ : [[ 𝜏0 ]]𝑙 is derivable.
The proof is obtained by simply applying the standard
technique of proving type preservation. The most difficult
part is to formulate the typing rules and translation rules correctly in the presence of applicative functors and generationof code and modules.

6[[ Runmod (𝑚 : sig 𝑆 end) ]] 0Δ = struct

𝑋

Other module expressions are kept intact and the environment Δ is not important for now. We omit the other clausesof the translation.

[[ $𝑝.𝑥 ]] 0Δ = [[ 𝑝 ]] 0 . 𝑥
In the first rule, Δ is the set of variables bound in the same
module (which appears as a code of the module), hence wemust add an escape (splice) to the variable after the translation. Similarly for the second rule. In the last rule, we
unconditionally eliminate $ from the paths.
The rules for [[ 𝑚 ]]𝑙Δ for a module expression 𝑚 is given
as follows:

𝑋′

Implementation and Performance

Although the main purpose of this paper is to give a solid
type-theoretic foundation to the languages for module generation, the performance of our language is not irrelevant,as the main objective of module generation is to eliminate
the overhead of functor applications (or module boundary).
We have implemented our languages using the translations in the previous section and compared the performanceof our implementation with those of the existing work. We
take a benchmark program used in existing studies suchas Watanabe et al. [20]. It implements simplification rules
for arithmetic expressions in a domain-specific language(DSL). The DSL is embedded in OCaml by the tagless-final
embedding [2], which extensively uses the module system.
Simplifications for DSL expressions such as 0 + 𝑛 → 𝑛 and
0 · 𝑛 → 0 are expressed by functors, and it is desirable toremove the overhead of functor applications.
The following functor Simp implements one of simplifications:

Type-Safe Generation of Modules inApplicative and Generative Styles

0.050

λ<M> (Watanabe et al.’s)
λ<A> (proposed)<G>
λ(proposed)

102
1

10

0

10

10-1

0.030
0.020
0.010

10-2
10-3

λ<M> (Watanabe et al.’s)
λ<A> (proposed)
λ<G> (proposed)

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

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

0.000
0

20
40
60
80
the number of functor applications

0

100

Figure 13. Time for Code Generation

2

4
6
8
10
12
the number of functor applications

1.2

λ

10

5

10
size of code [KB]

execution time [s]6naive (no code generation)<M>
λ(Watanabe et al.’s)<A>λ(proposed)
λ<G> (proposed)

1.4

16

Figure 15. Execution Time for Generated Code (zoomed)

1.8
1.6

14

1.0
0.8
0.6
0.4

<M>

(Watanabe et al.’s)
λ<A> (proposed)
λ<G> (proposed)

4

10

103
102
101
100

0.2
0.0
0

20
40
60
80
the number of functor applications

100

Figure 14. Execution Time for Generated Codemodule Simp = functor (M : S mcod ) →⟨⟨ ( structtype int_t = $M . int_t * bool
let add n1 n2 =match ( n1 , n2 ) with( x1 , b1 ) ,(x2 , b2 ) →if b1 && b2 then (~( $M . int )0, true )else if b1 then (x2 , false )
else if b2 then (x1 , false )
else (~( $M . add ) x1 x2 , false )...
end : S ) ⟩⟩The argument of Simp is code of a structure M, which expresses arithmetic expressions before simplification. The
functor Simp simplifies an addition expression when at least
one of its arguments is zero. To do this, the type M.int_t is interpreted as a pair of an arithmetic expression and a boolean
flag to indicate the expression is zero or not. Since M has thetype S mcod,$M.add refers to the code of the add-componentof M correctly, which is spliced into the resulting code, andthe overhead of an indirect function call eliminated. Our
test program applies the functor Simp to a structure manytimes such as Simp(Simp(...(M)...)), and we measured
the performance of the resulting module.

10-1

0

20
40
60
80
the number of functor applications

100

Figure 16. Size of Generated CodeWe have measured the performance of the following four
variations:• a naïve OCaml program (no code generation).
• a MetaOCaml program with Watanabe et al.’s translation.
• a MetaOCaml program in 𝜆 <𝐺 > with our translation.
• a MetaOCaml program in 𝜆 <𝐴> with our translation.
We did not include the result by Sato et al.’s translation, sincefor this benchmark the resulting program by their translation
is identical to the one in 𝜆 <𝐺 > with our translation.
We have conducted the experiments on Ubuntu 18.04 LTS,
Xeon E3-1225 v6@3.3GHz, Memory 32GB, BER MetaOCaml
N107 (OCaml 4.07.1), byte code compiler, and all the results
are the average of 10 trials. For these programs, we havemeasured the time for code generation and compilation (Figure 13), the execution time of generated code (Figure 14 and15), and the size of generated code (Figure 16) where the sizeof code is the file size in bytes,
The results can be summarized as follows. First, all approaches based on module generation outperform the naïve
program (Figure 14), thus we confirmed that it eliminates theoverhead of functor applications. Second, both of our two
languages have slightly better performance in the execution
time than Watanabe et al.’s work, while ours outperform

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

theirs in the other factors (the code-generation time and thesize of generated code). Third, in all experiments, the generative and applicative styles have quite similar performance.
Hence, and we can select a suitable style depending on ourapplications without worrying about the loss of performance.

7

Related WorkIn this section, we compare several closely related works
with our work.
One can say that our work provides a means to inline functor applications based on the programmer’s control. There
are fully automatic tools or systems to inline functor applications including Flambda [6] and MLton 8 . By aggressively
inlining functor applications, they can eliminate redundant
indirections. While automatic tools are easier to use thanhuman-controlled tools, we think the former does not always subsume the latter, just like fully automatic partial
evaluation does not always subsume programmer-controlled
program generation. In particular, when we want to inline
functor applications conditionally, based on domain-specificknowledge, or when we want to control the number of inlining (how much we inline the functor applications), humanintervention is needed.
Squid [13] is a multi-stage programming framework for
Scala, and guarantees that generated code is well-typed andwell-scoped. Parreaux and Shaikhha [12] proposed a libraryfor class generation built on top of the Squid and gave practical use cases. Unfortunately, it is difficult to simply apply
their use cases to our approach. First, classes can have states,
but modules without side effects cannot. Second, their libraryprovides a way to dynamically generate fields of classes, but
our language cannot. Achieving them in a type-safe way andgiving large-scale practical use cases are left for future work.
The MetaML-style approach taken in this work is purely
generative. Many studies take opposite approaches based on
introspection or reflection which allow the inspection or
decomposition of generated code. One of such approaches is
Racket’s module system [7] mentioned in Section 1. Anotherrelated work is SugarJ [5], which provides a library-based
approach to module systems for model-driven development.
Although their motivation is quite different from ours, there
is some technical similarity in that their modules provide
phase separation, and they consider transformers over modules just like functors over modules in our case.

8

Conclusion

In this paper, we have studied typed two-stage programming
languages for generating and manipulating code of modules. We have designed two languages that allow generating
modules in different styles, given a precise type-theoretic
formulation, and defined a type-preserving translation to
8 http://www.mlton.org

Yuhi Sato and Yukiyoshi Kameyama

plain MetaOCaml. We have also implemented program translators based on our translations and shown that despite thecomplexity of the language and the type system, the module
generation with applicative functors and second-class modules has almost identical performance compared with theexisting studies based on generative functors and first-classmodules. Thus, a programmer can choose the style withoutworrying about the performance.
One may wonder if realistic programs use deeply nested
functor applications as is used in our benchmark program,but there exist such cases. For instance, MirageOS contains
many functor applications, and its web service has functor
applications of depth up to 10 [14]. The actual MirageOS maycontain more indirections than this, hence we can expectthat the benefit of module generation would be even greater.
There are many directions for future work. First, we wantto make our languages more expressive to cover polymorphism, computational effects, and sharing constraints in modules. Second, FLambda is a fully automatic inlining systemthat works for functor applications, too. While we believethat human-controlled generation of modules and terms suchas our work can outperform the former, unifying these approaches is doable and will be interesting from the practicalaspect. Finally, ML-style modules are not the only high-level
abstractions for programming languages, and there are many
works in the literature that investigated the generation ofhigh-level abstractions such as classes. By comparing ourwork and others, we want to improve our languages and also
help improve other works.

Acknowledgments
We would like to thank the anonymous reviewers and the
PC members of GPCE 2021 for their valuable comments.
The second author is supported in part by Grant-in-Aid for
Scientific Research (B) No. 18H03218.

References[1] Cristiano Calcagno, Eugenio Moggi, and Walid Taha. 2004. ML-LikeInference for Classifiers. In Programming Languages and Systems, 13th
European Symposium on Programming, ESOP 2004, Held as Part of the
Joint European Conferences on Theory and Practice of Software, ETAPS
2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings (Lecture
Notes in Computer Science), David A. Schmidt (Ed.), Vol. 2986. Springer,
79–93. https://doi.org/10.1007/978-3-540-24725-8_7[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] 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[4] Derek Dreyer. 2005. Understanding and Evolving the ML Module System.
Ph.D. Dissertation. USA. AAI3166274.
[5] Sebastian Erdweg and Klaus Ostermann. 2017. A Module-System
Discipline for Model-Driven Software Development. Art Sci. Eng.

Type-Safe Generation of Modules inApplicative and Generative Styles
Program. 1, 2 (2017), 9. https://doi.org/10.22152/programming-journal.
org/2017/1/9[6] Xavier Leroy et al. 2019. Chapter 21. Optimisation with Flambda. The
OCaml system release 4.09. https://caml.inria.fr/pub/docs/manualocaml/flambda.html[7] Matthew Flatt. 2013. Submodules in racket: you want it when, again?.
In Generative Programming: Concepts and Experiences, GPCE’13, Indianapolis, IN, USA - October 27 - 28, 2013, Jaakko Järvi and Christian
Kästner (Eds.). ACM, 13–22. https://doi.org/10.1145/2517208.2517211[8] Yuichiro Hanada and Atsushi Igarashi. 2014. On Cross-Stage Persistence in Multi-Stage Programming. In Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa,
Japan, June 4-6, 2014. Proceedings (Lecture Notes in Computer Science),
Michael Codish and Eijiro Sumii (Eds.), Vol. 8475. Springer, 103–118.
https://doi.org/10.1007/978-3-319-07151-0_7[9] 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[10] Oleg Kiselyov. 2014. The Design and Implementation of BER MetaOCaml - System Description. In Functional and Logic Programming 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6,
2014. Proceedings. 86–102. https://doi.org/10.1007/978-3-319-071510_6[11] Xavier Leroy. 1995. Applicative Functors and Fully Transparent HigherOrder Modules. In Proceedings of the 22nd ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (San Francisco,California, USA) (POPL ’95). Association for Computing Machinery,
New York, NY, USA, 142–153. https://doi.org/10.1145/199448.199476[12] Lionel Parreaux and Amir Shaikhha. 2020. Multi-Stage Programmingin the Large with Staged Classes. In Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts
and Experiences (Virtual, USA) (GPCE 2020). Association for Computing Machinery, New York, NY, USA, 35–49. https://doi.org/10.1145/
3425898.3426961[13] Lionel Parreaux, Amir Shaikhha, and Christoph E. Koch. 2017. Squid:
type-safe, hygienic, and reusable quasiquotes. In Proceedings of the 8th
ACM SIGPLAN International Symposium on Scala, SCALA@SPLASHGPCE ’21, October 17–18, 2021, Chicago, IL, USA
2017, Vancouver, BC, Canada, October 22-23, 2017, Heather Miller,
Philipp Haller, and Ondrej Lhoták (Eds.). ACM, 56–66. https://doi.org/
10.1145/3136000.3136005[14] 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[15] 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@POPL 2020, New Orleans, LA, USA, January 20, 2020,
Casper Bach Poulsen and Zhenjiang Hu (Eds.). ACM, 1–13. https://doi.org/10.1145/3372884.3373160[16] Tim Sheard. 1998. Using MetaML: A Staged Programming Language.
In Advanced Functional Programming, Third International School, Braga,
Portugal, September 12-19, 1998, Revised Lectures (Lecture Notes in
Computer Science), S. Doaitse Swierstra, Pedro Rangel Henriques,
and José Nuno Oliveira (Eds.), Vol. 1608. Springer, 207–239. https://doi.org/10.1007/10704973_5[17] Walid Taha. 2003. A Gentle Introduction to Multi-stage Programming.
In Domain-Specific Program Generation, International Seminar, Dagstuhl
Castle, Germany, March 23-28, 2003, Revised Papers. 30–50. https://doi.org/10.1007/978-3-540-25935-0_3[18] Walid Taha and Michael Florentin Nielsen. 2003. Environment Classifiers. SIGPLAN Not. 38, 1 (Jan. 2003), 26–37. https://doi.org/10.1145/
640128.604134[19] Walid Taha and Tim Sheard. 1997. Multi-Stage Programming. In
Proceedings of the 1997 ACM SIGPLAN International Conference on
Functional Programming (ICFP ’97), Amsterdam, The Netherlands, June
9-11, 1997, Simon L. Peyton Jones, Mads Tofte, and A. Michael Berman(Eds.). ACM, 321. https://doi.org/10.1145/258948.258990[20] 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[21] 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