Static Interpretation
By Martin Elsman and Mads Tofte
Interpretation of Standard ML Modules at Compile time
The MLKit regards the Modules language as a linking language, which describes how pieces of code are glued together. The dynamic semantics of Modules in the Definition of Standard ML can be regarded as describing an interpreter which combines runtime environments. However, nothing in the dynamic semantics of Modules depends on runtime values. Therefore, the dynamic semantics can be used as a specification of how code fragments can be combined. By taking this approach, the MLKit is able to perform all module-level execution during compilation. Neither structures, nor signatures, nor functors exist at runtime. Conceptually, the modules language is simply used for putting together pieces of declarations from the Core Language.
Functors are elaborated when they are declared, as in most ML compilers. Thus type errors in functors are caught already when the functor is declared (as opposed to when it is applied). However, when the MLKit has elaborated a functor declaration, it postpones code generation for the functor until the functor is applied. Indeed, if a functor is applied to two different arguments, code for its body will be generated twice. We refer to this approach to Module compilation as static interpretation. Static interpretation has important advantages:
Propagation of Compile-Time Information Across Module Boundaries
When the body of a functor is compiled, the actual argument to which it is applied is known. Thus one can make use of the information the compiler has about the actual argument when code is generated for the functor body. Region Information is a case in point. For example, consider:
functor F(X: sig
type t
val f : int -> t
val g : t -> int * int
end) =
struct
val it = #1(g(f(5)))
end;
The formal parameter signature for X
does not give any region type
schemes for f
and g
. For example, the signature does not say whether g
creates the pair it returns in a fresh region, or perhaps always
returns some fixed pair which resides in a global
region. Consequently, region inference of the body of F
is not
possible: we cannot know whether the pair returned by g
can be
deallocated after the first projection has been applied to it. Now
consider an application of F
:
structure S = F(struct
type t = int
fun f(n:int) = n
fun g(n:int) = (n,n)
end)
Region inference of the actual argument to the call of F
shows that
the actual g
creates a fresh pair. The code generated for the
application will be equivalent to:
local
type t = int
fun f(n:int) = n
fun g(n:int) = (n,n)
in
val it = #1(g(f(5))
end
Therefore, region inference will determine that the pair created by g
can indeed be reclaimed after the first projection has been applied to
it.
No Module-Level Code at Runtime
Since modules are interpreted statically, there is no runtime code for creating structures. Such code can be quite large and it is often only executed once. Signature matching generates no code either, not even in the case where signature matching imposes a less polymorphic type on a value in a structure. The theory behind all this and a proof of its correctness may be found in Martin Elsman’s ICFP’99 paper Static Interpretation of Modules.