Tracking Data-Flow with Open Closure Types
Gabriel Scherer1 and Jan Hoffmann2

arXiv:1312.0018v1 [] 29 Nov 2013

1

INRIA Paris-Rocquencourt
2
Yale University

Abstract. Type systems hide data that is captured by function closures
in function types. In most cases this is a beneficial design that enables
simplicity and compositionality. However, some applications require explicit information about the data that is captured in closures.
This paper introduces open closure types, that is, function types that are
decorated with type contexts. They are used to track data-flow from the
environment into the function closure. A simply-typed lambda calculus
is used to study the properties of the type theory of open closure types.
A distinctive feature of this type theory is that an open closure type of
a function can vary in different type contexts. To present an application
of the type theory, it is shown that a type derivation establishes a simple non-interference property in the sense of information-flow theory. A
publicly available prototype implementation of the system can be used
to experiment with type derivations for example programs.
Keywords: Type Systems, Closure Types, Information Flow

1

Introduction

Function types in traditional type systems only provide information about the
arguments and return values of the functions but not about the data that is
captured in function closures. Such function types naturally lead to simple and
compositional type systems.
Recently, syntax-directed type systems have been increasingly used to statically verify strong program properties such as resource usage [8, 7, 6], information
flow [5, 15], and termination [1, 3, 2]. In such type systems, it is sometimes necessary and natural to include information in the function types about the data
that is captured by closures. To see why, assume that we want to design a type
system to verify resource usage. Now consider for example the curried append
function for integer lists which has the following type in OCaml.
append : int list → int list → int list
At first glance, we might say that the time complexity of append is O(n) if n
is the length of the first argument. But a closer inspection of the definition of
append reveals that this is a gross simplification. In fact, the complexity of the
partial function call app par = append ℓ is constant. Moreover, the complexity
of the function app par is linear—not in the length of the argument but in the
length of the list ℓ that is captured in the function closure.

2

Gabriel Scherer and Jan Hoffmann

In general, we have to describe the resource consumption of a curried function f : A1 → · · · → An → A with n expressions ci (a1 , . . . , ai ) such that ci
describes the complexity of the computation that takes place after f is applied
to i arguments a1 , . . . , ai . We are not aware of any existing type system that can
verify a statement of this form.
To express the aforementioned statement in a type system, we have to decorate the function types with additional information about the data that is captured in a function closure. It is however not sufficient to directly describe the
complexity of a closure in terms of its arguments and the data captured in the
closure. Admittedly, this would work to accurately describe the resource usage in
our example function append because the first argument is directly captured in
the closure. But in general, the data captured in a closure f a1 · · · ai can be any
data that is computed from the arguments a1 , . . . , ai (and from the data in the
environment). To reference this data in the types would not only be meaningless
for a user, it would also hamper the compositionality of the type system. It is
for instance unclear how to define subtyping for closures that capture different
data (which is, e.g., needed in the two branches of a conditional.)
To preserve the compositionality of traditional type systems, we propose to
describe the resource usage of a closure as a function of its argument and the
data that is visible in the current environment. To this end we introduce open
closure types, function types that refer to their arguments and to the data in the
current environment.
More formally, consider a typing judgment of the form Γ ⊢ e : σ, in a type
system that tracks fine-grained intensional properties characterizing not only
the shape of values, but the behavior of the reduction of e into a value (e.g.,
resource usage). A typing rule for open closure types, Γ, ∆ ⊢ e : [Γ ′ ](x:σ) → τ ,
captures the idea that, under a weak reduction semantics, the computation of
the closure itself, and later the computation of the closure application, will have
very different behaviors, captured by two different typing environments Γ and
Γ ′ of the same domain, the free variables of e. To describe the complexity of
append, we might for instance have a statement
ℓ:int list ⊢ append ℓ : [ℓ:int list ](y:int list ) → int list .
This puts us in a position to use type annotations to describe the resource usage
of append ℓ as a function of ℓ and the future argument y. For example, using
type-based amortized analysis [6], we can express a bound on the number of
created list notes in append with the following open closure type.
append : [](x:int list 0 ) → [x:int list 1 ](y:int list 0 ) → int list0 .
The intuitive meaning of this type for append is as follows. To pay for the cons
operations in the evaluation of append ℓ1 we need 0·|ℓ1 | resource units and to pay
for the cons operations in the evaluation of append ℓ1 ℓ2 we need 0·|ℓ1 | + 1·|ℓ2 |
resource units.
The development of a type system for open closure types entails some interesting technical challenges: term variables now appear in types, which requires
mechanisms for scope management not unlike dependent type theories. If x ap-

Tracking Data-Flow with Open Closure Types

3

pears in σ, the context Γ, x:τ, y:σ is not exchangeable with Γ, y:σ, x:τ . Similarly,
the judgment Γ, x:τ ⊢ e2 : σ will not entail Γ ⊢ let x = e1 in e2 : σ, as the return type σ may contain open closures scoping over x, so we need to substitute
variables in types.
The main contribution of this paper is a type theory of open closure types
and the proof of its main properties. We start from the simply-typed lambda
calculus, and consider the simple intensional property of data-flow tracking, annotating each simply-typed lambda-calculus type with a single boolean variable. This allows us to study the metatheory of open closure types in clean and
straightforward way. This is the first important step for using such types in more
sophisticated type systems for resource usage and termination.
Our type system for data-flow tracking captures higher-order data-flow information. As a byproduct, we get our secondary contribution, a non-interference
property in the sense of information flow theory: high-level inputs do not influence the (low-level) results of computations.
To experiment with of our type system, we implemented a software prototype
in OCaml (see Section 5). A full version of this article, containing the full proofs
and additional details and discussion, is available online.3
Related Work. In our type system we maintain the invariant that open closure
types only refer to variables that are present in the current typing context. This
is a feature that distinguishes open closure types from existing formalisms for
closure types.
For example, while our function type [Γ Φ ](x:σ1 ) → σ2 superficially resembles a contextual arrow type [Ψ ](σ1 → σ2 ) of contextual type theory[12, 14, 16],
we are not aware of any actual connection in application or metatheory with
these systems. In particular, the variable in our captured context Γ Φ are bound
occurrences of the ambient typing context, while the context Ψ of a contextual
type [Ψ ]T binds metavariables to be used to construct inhabitants. As such a
binding can make sense in any context, our substitution judgment has no counterpart in contextual type theory, or other modal type theories for multi-stage
programming ([11, 17]).
Having closure types carry a set of captured variables has been done in the
literature, as for example in Leroy [9], which use closure types to keep track of
of dangerous type variables that can not be generalized without breaking type
safety, or in the higher-order lifetime analysis of Hannan et al. [4], where variable
sets denote variables that must be kept in memory. However, these works have
no need to vary function types in different typing contexts and subtyping can be
defined using set inclusion, which makes the metatheory significantly simpler. On
the contrary, our scoping mechanism allows to study more complex properties,
such as value dependencies and non-interference.
The classical way to understand value capture in closures in a typed way
is through the typed closure conversion of Minamide et al. [10]. They use existential types to account for hidden data in function closures without losing
3

http://hal.inria.fr/INRIA-RRRT/hal-00851658

4

Gabriel Scherer and Jan Hoffmann

compositionality, by abstracting over the difference between functions capturing
from different environments. Our system retains this compositionality, albeit in
a less apparent way: we get finer-grained information about the dependency of
a closure on the ambient typing environment. Typed closure conversion is still
possible, and could be typed in a more precise way, abstracting only over values
that are outside the lexical context.
Petricek et al. [13] study coeffects systems with judgments of the form C r Γ ⊢
e : τ and function types C s σ → τ , where r and s are coeffect annotations over
an indexed comonad C. Their work is orthogonal to the present one. They study
comonadic semantics and algebraic structure of effect indices. These indices are
simply booleans in our work but we focus on the syntactic scoping rules that
arise from tracking each variable of the context separately.
The non-interference property that we prove is different from the usual treatment in type systems for information flow like the SLam Calculus [5]. In SLam,
the information flow into closure is accounted for at abstraction time. In contrast,
we account for the information flow into the closure at application time.

2

A Type System for Open Closures

We define a type system for the simplest problem domain that exhibits a need
for open closure types. Our goal is to determine statically, for an open term e,
on which variables of the environment the value of e depends.
We are interested in weak reduction, and assume a call-by-value reduction
strategy. In this context, an abstraction λx.e is already a value, so reducing
it does not depend on the environment at all. More generally, for a term e
evaluating to a function (closure), we make a distinction between the part of the
environment the reduction of e depends on, and the part that will be used when
the resulting closure will be applied. For example, the term (y, λx.z) depends
on the variable y at evaluation time, but will not need the variable z until the
closure in the right pair component is applied.
This is where we need open closure types. Our function types are of the form
[Γ Φ ](x:σ φ ) → τ , where the mapping Φ from variables to Booleans indicates
on which variables the evaluation depends at application time. The Boolean φ
indicates whether the argument x is used in the function body. We call Φ the
dependency annotation of Γ . Our previous example would for instance be typed
as follows.
y:σ 1 , z:τ 0 ⊢ (y, λx.z) : σ ∗ ([y:σ 0 , z:τ 1 ](x:ρ0 ) → τ )
The typing expresses that the result of the computation depends on the variable
y but not on the variable z. Moreover, result of the function in the second
component of the pair depends on z but not on y.
In general, types are defined by the following grammar.
Types ∋ σ, τ, ρ ::=
| α
| τ1 ∗ τ2
| [Γ Φ ](x:σ φ ) → τ

types
atoms
products
closures

Tracking Data-Flow with Open Closure Types
Scope-Context-Nil
∅⊢
Scope-Product
Γ ⊢ τ1
Γ ⊢ τ2
Γ ⊢ τ1 ∗ τ2

Scope-Context
Γ ⊢σ

Scope-Atom
Γ ⊢

Γ, x:σ ⊢

Γ ⊢α

Scope-Closure
Γ0 , Γ1 ⊢
Γ0 ⊢ σ
Γ0 , Γ1 ⊢

5

Γ0 , x:σ ⊢ τ

[Γ0Φ ](x:σ φ )

→τ

Fig. 1. Well-scoping of types and contexts

The closure type [Γ Φ ](x:σ φ ) → τ binds the new argument variable x, but not
the variables occurring in Γ which are reference variables bound in the current
typing context. Such a type is well-scoped only when all the variables it closes
over are actually present in the current context. In particular, it has no meaning
in an empty context, unless Γ is itself empty.
We define well-scoping judgments on contexts (Γ ⊢) and types (Γ ⊢ σ). The
judgments are defined simultaneously in Figure 1 and refer to each another. They
use non-annotated contexts: the dependency annotations characterize data-flow
information of terms, and are not needed to state the well-formedness of static
types and contexts.
Notice that the closure contexts appearing in the return type of a closure,
τ in our rule Scope-Closure, may capture the variable x corresponding to the
function argument, which is why we chose the dependent-arrow–like notation
(x:σ) → τ rather than only σ → τ . There is no dependency of types on terms in
this system, this is only used for scope tracking.
Note that Γ ⊢ σ implies Γ ⊢ (as proved by direct induction until an atom
or a function closure is reached). Note also that a context type [Γ0 ](x:σ) → τ is
well-scoped in any larger environment Γ0 , Γ1 : the context information may only
mention variables existing in the typing context, but it need not mention all of
them. As a result, well-scoping is preserved by context extension: if Γ0 ⊢ σ and
Γ0 , Γ1 ⊢, then Γ0 , Γ1 ⊢ σ.
A Term Language, and a Naive Attempt at a Type System. Our term
language, is the lambda calculus with pairs, let bindings and fixpoints. This
language is sufficient to discuss the most interesting problems that arise in an
application of closure types in a more realistic language.
Terms ∋ t, u, e ::=
|
|
|
|
|
|

x
(e1 , e2 )
πi (e)
λx.e
tu
let x = e1 in e2

terms
variables
pairs
projections (i ∈ {1, 2})
lambda abstractions
applications
let declarations

For didactic purposes, we start with an intuitive type system presented in
Figure 2. The judgment Γ Φ ⊢ e : σ means that the expression e has type σ, in

6

Gabriel Scherer and Jan Hoffmann
Product
Γ Φ 1 ⊢ e 1 : τ1

Var
Γ, x:σ, ∆ ⊢
Γ 0 , x:σ 1 , ∆0 ⊢ x : σ

Γ Φ ⊢ πi (e) : τi

Let-Tmp
Γ Φdef ⊢ e1 : σ

Γ Φbody , x:σ φ ⊢ e2 : τ

Γ Φ , x:σ φ ⊢ t : τ
Φ

Proj
Γ Φ ⊢ e : τ1 ∗ τ2

Γ Φ1 +Φ2 ⊢ (e1 , e2 ) : τ1 ∗ τ2

Lam
0

Γ Φ 2 ⊢ e 2 : τ2

φ

Γ ⊢ λx.t : [Γ ](x:σ ) → τ

Γ

φ.Φdef +Φbody

App-Tmp
(Γ0 , Γ1 )Φfun ⊢ t : [Γ0Φclos ](x:σ φ ) → τ
(Γ0 , Γ1 )

Φfun +Φclos +φ.Φarg

⊢ let x = e1 in e2 : τ

(Γ0 , Γ1 )Φarg ⊢ u : σ
⊢tu:τ

Fig. 2. Naive rules for the type system

the context Γ carrying the intensional information Φ. Context variable mapped
to 0 in Φ are not used during the reduction of e to a value. We will show that
the rules App-Tmp and Let-Tmp are not correct, and introduce a new judgment
to develop correct versions of the rules.
In a judgment Γ 0 ⊢ λx.t : [Γ Φ ](x:σ 0 ) → τ , Γ is bound only in one place (the
context), and α-renaming any of its variable necessitates a mirroring change in
its right-hand-side occurrences (Γ Φ but also in σ and τ ), while x is independently
bound in the term and in the type, so the aforementioned type is equivalent to
[Γ Φ ](y:σ) → τ [y/x]. In particular, variables occurring in types do not reveal
implementation details of the underlying term.
The syntax φ.Φ used in the App-Tmp and Let-Tmp rules is a product, or
conjunction, of the single boolean dependency annotation φ, and of the vector
dependency annotation Φ. The sum Φ1 + Φ2 is the disjunction. In the Let-Tmp
rule for example, if the typing of e2 determines that the evaluation of e2 does not
depend on the definition x = e1 (φ is 0), then φ.Φdef will mark all the variables
used by e1 as not needed as well (all 0), and only the variables needed by e2 will
be marked in the result annotation φ.Φdef + Φbody .
In the scoping judgment Γ ⊢ [Γ Φ ](x:σ) → τ , the repetition of the judgment
Γ is redundant. We could simply write [Φ](x:σ) → τ ; – because in our simplified
setting the intensional information Φ can be easily separated from the rest of
the typing information, corresponding to simply-typed types. However, we found
out that such a reformulation made technical developments harder to follow; the
Γ Φ form allows one to keep track precisely of the domain of the dependency
annotation, and domain changes are precisely the difficult technical aspect of
open closure types. For a more detailed discussion of this design point, see the
full version of this article.
Maintaining Closure Contexts. As pointed out before, the rules App-Tmp
and Let-Tmp of the system above are wrong (hence the “temporary” name):
the left-hand-side of the rule App-Tmp assumes that the closure captures the
same environment Γ that it is computed in. This property is initially true in the
closure of the rule Lam, but is not preserved by Let-Tmp (for the body type) or

Tracking Data-Flow with Open Closure Types

Subst-Context-Nil
y\Ψ
Γ, y:ρ, ∅
Γ

Subst-Context
y\Ψ
Γ, y:ρ, ∆ ⊢ σ
Γ, ∆′ ⊢ τ
Γ, y:ρ, ∆, x:σ

y\Ψ

Γ, ∆′ , x:τ

Subst-Product
y\Ψ
Γ, y:ρ, ∆ ⊢ σ1
Γ, ∆′ ⊢ τ1

Subst-Atom
Γ, y:ρ, ∆
Γ, y:ρ, ∆ ⊢ α

Γ, y:ρ, ∆ ⊢ σ2

Γ, y:ρ, ∆ ⊢ σ1 ∗ σ2
Subst-Closure-Notin
Γ0 , Γ1 , y:ρ, ∆
Γ0 , Γ1 , y:ρ, ∆ ⊢ [Γ0Φ ](x:σ1φ ) → σ2

y\Ψ

7

y\Ψ

Γ, ∆′

y\Ψ

Γ, ∆′ ⊢ α

Γ, ∆′ ⊢ τ2

y\Ψ

Γ, ∆′ ⊢ τ1 ∗ τ2

y\Ψ

Γ 0 , Γ 1 , ∆′

y\Ψ

Γ0 , Γ1 , ∆′ ⊢ [Γ0Φ ](x:σ1φ ) → σ2

y\Ψ

Γ, ∆′ , Γ1′

Subst-Closure
Γ, y:ρ, ∆, Γ1
Γ, y:ρ, ∆ ⊢ σ1

y\Ψ

′

Γ, ∆ ⊢ σ1

Γ, y:ρ, ∆, x:σ1 ⊢ σ2

Γ, y:ρ, ∆, Γ1 ⊢ [Γ Φ1 , y:ρχ , ∆Φ2 ](x:σ1φ ) → σ2

y\Ψ

y\Ψ

Γ, ∆′ , x:σ1 ⊢ τ2

Γ, ∆′ , Γ1′ ⊢ [Γ Φ1 +χ.Ψ , ∆′

Φ2

](x:σ1φ ) → τ2

Fig. 3. Type substitution

App-Tmp (for the return type). This means that the intensional information in a
type may become stale, mentioning variables that have been removed from the
context. We will now fix the type system to never mention unbound variables.
We need a closure substitution mechanism to explain the closure type τf =
[Γ Φ , y:ρχ ](x:σ φ ) → τ ψ of a closure f in the smaller environment Γ , given dependency information for y in Γ . Assume for example that y was bound in a
let binding let y = e . . . and that the type τf leaves the scope of y. Then we
have to adapt the type rules to express the following. “If f depends on y (at
application time) then f depends on the variables of Γ that e depends on.”
y\Ψ

We define in Figure 3 the judgment Γ, y:ρ, ∆ ⊢ σ
Γ, ∆′ ⊢ τ . Assuming
that the variable y in the context Γ, y:ρ, ∆ was let-bound to an definition with
usage information Γ Ψ , this judgment transforms any type σ in this context in a
type τ in a context Γ, ∆′ that does not mention y anymore. Note that ∆ and ∆′
have the same domain, only their intensional information changed: any mention
of y in a closure type of ∆ was removed in ∆′ . Also note that Γ, y:ρ, ∆ and Γ, ∆′ ,
or σ and τ , are not annotated with dependency annotations themselves: this is
only a scoping transformation that depends on the dependency annotations of
y in the closures of σ and ∆.
As for the scope-checking judgment, we simultaneously define the substituy\Ψ

tions on contexts themselves Γ, y:ρ, ∆
Γ, ∆′ . There are two rules for substituting a closure type. If the variable being substituted is not part of the closure
type context (rule Subst-Closure-Notin), this closure type is unchanged. Otherwise (rule Subst-Closure) the substitution is performed in the closure type,
and the neededness annotation for y is reported to its definition context Γ0 .

8

Gabriel Scherer and Jan Hoffmann

The following lemma verifies that this substitution preserves well-scoping of
contexts and types.
y\Ψ

Lemma 1 (Substitution and scoping). If Γ, y:ρ, ∆ ⊢ and Γ, y:ρ, ∆
y\Ψ

Γ, ∆′ then Γ, ∆′ ⊢. If Γ, y:ρ, ∆ ⊢ σ and Γ, y:ρ, ∆ ⊢ σ
Γ, ∆′ ⊢ τ .

Γ, ∆′ ⊢ τ then

We can now give the correct rules for binders:
Let

Γ Φdef ⊢ e1 : σ

Γ Φbody , x:σ φ ⊢ e2 : τ

Γ, x:σ ⊢ τ

x\Φdef

Γ ⊢ τ′

Γ φ.Φdef +Φbody ⊢ let x = e1 in e2 : τ ′
App

(Γ0 , Γ1 )Φfun ⊢ t : [Γ0Φclos ](x:σ φ ) → τ
(Γ0 , Γ1 )Φarg ⊢ u : σ

Γ0 , Γ1 , x:σ ⊢ τ

x\Φarg

Γ0 , Γ1 ⊢ τ ′

(Γ0 , Γ1 )Φfun +Φclos +φ.Φarg ⊢ t u : τ ′
Lemma 2 (Typing respects scoping). If Γ ⊢ t : σ holds, then Γ ⊢ σ holds.
This lemma guarantees that we fixed the problem of stale intensional information: types appearing in the typing judgment are always well-scoped.
y\Ψ

′

It is handy to introduce a convenient derived notation Γ Φ ⊢ τ
Γ ′Φ ⊢ τ ′
that is defined below. This substitution relation does not only remove y from
the open closure types in Γ , it also updates the dependency annotation on Γ to
add the dependency Ψ , corresponding to all the variables that y depended on –
if it is itself marked as needed.
Γ, y:ρ, ∆ ⊢ τ
Γ Φ1 , y:ρχ , ∆Φ2 ⊢ τ

3

y\Ψ

y\Ψ

Γ, ∆′ ⊢ τ ′

Γ Φ1 +χ.Ψ , ∆′

Φ2

⊢ τ′

A Big-Step Operational Semantics

In this section, we will define an operational semantics for our term language, and
use it to prove the soundness of the type system (Theorem 1). Our semantics is
equivalent to the usual call-by-value big-step reduction semantics for the lambdacalculus in the sense that computation happens at the same time. There is
however a notable difference.
Function closures are not built in the same way as they are in classical bigstep semantics. Usually, we have a rule of the form V ⊢ λx.t =⇒ (V, λx.t) where
the closure for λx.t is a pair of the value environment V (possibly restricted to its
subset appearing in t) and the function code. In contrast, we capture no values
at closure creation time in our semantics: V ⊢ λx.t =⇒ (∅, λx.t). The captured
values will be added to the closure incrementally, during the reduction of binding
forms that introduced them in the context.

Tracking Data-Flow with Open Closure Types

9

Consider for example the following two derivations; one in the classic big-step
reduction, and the other in our alternative system.
Classic-Red-Let
c

x:v ⊢ x =⇒ v

c

x:v, y:v ⊢ λz.y =⇒ ((x 7→ v, y 7→ v), λz.y)
c

x:v ⊢ let y = x in λz.y =⇒ ((x 7→ v, y 7→ v), λz.y)
Our-Red-Let

x:v ⊢ x =⇒ v
y\v

x:v, y:v ⊢ λz.y =⇒ ([x, y], ∅, λz.y)
(∅, λz.y)
([x], y 7→ v, λz.y)
x:v ⊢ let y = x in λz.y =⇒ ([x], y 7→ v, λz.y)
Rather than capturing the whole environment in a closure, we store none at
all at the beginning (merely record their names), and add values incrementally,
just before they get popped from the environment. This is done by the value
x\v

substitution judgment w
w′ that we will define in this section. The reason for
this choice is that this closely corresponds to our typing rules, value substitution
x\Φ

being a runtime counterpart to substitution in types Γ ⊢ σ
Γ ′ ⊢ σ ′ ; this
common structure is essential to prove of the type soundness (Theorem 1).
Note that derivations in this modified system and in the original one are
in one-to-one mapping. It should not be considered a new dynamic semantics,
rather a reformulation that is convenient for our proofs as it mirrors our static
judgment structure.
Values and Value Substitution. Values are defined as follows.
Val ∋ v, w ::=
| vα
| (v, w)
| ([xj ]j∈J , (xi 7→ vi )i∈I , λx.t)

values
value of atomic type
value tuples
function closures

The set of variables bound in a closure is split into an ordered mapping
(xi 7→ vi )i∈I for variables that have been substituted to their value, and a simple
list [xj ]j∈J of variables whose value has not yet been captured. They are both
binding occurrences of variables bound in t; α-renaming them is correct as long
as t is updated as well.
To formulate our type soundness result, we define a typing judgment on values
Γ ⊢ v : σ in Figure 4. An intuition for the rule Value-Closure is the following.
Internally, the term t has a dependency Γ Φ on the ambient context, but also
dependencies (τiψi ) on the captured variables. But externally, the type may not
′
mention the captured variables, so it reports a different dependency Γ Φ that
corresponds to the internal dependency Γ Φ , combined with the dependencies
(Ψi ) of the captured values. Both families (ψi )i∈I and (Ψi )i∈I are existentially
quantified in this rule.
In the judgment rule, the notation (xj : τj )j<i is meant to define the environment of each (xi : τi ) as Γ Φ , plus all the (xj : τj ) that come before xi in the

10

Gabriel Scherer and Jan Hoffmann
Value-Atom
Γ ⊢

Value-Product
Γ ⊢ v1 : τ1
Γ ⊢ v2 : τ2

Γ ⊢ vα : α

Γ ⊢ (v1 , v2 ) : τ1 ∗ τ2

Value-Closure
Γ, Γ1 ⊢
Γ

Φ

, (xi :τiψi )i∈I , x:σ φ

∀i ∈ I, Γ, (xj :τj )j<i ⊢ vi : τi
Γ Φ , (xi :τiψi )i∈I , x:σ φ ⊢ τ

⊢t:τ

(xi )\(Ψi )

′

Γ Φ , x:σ φ ⊢ τ ′

′

Γ, Γ1 ⊢ (dom Γ, (xi 7→ vi )i∈I , λx.t) : [Γ Φ ](x:σ φ ) → τ ′
Fig. 4. Value typing
Subst-Value-Product
y\v
y\v
w1
w1′
w2
w2′

Subst-Value-Atom
y\v
vα
vα
Subst-Value-Closure
([xj1 , . . . , xjn , y], (xi 7→ wi )i∈I , t)

(w1 , w2 )
y\v

y\v

(w1′ , w2′ )

([xj1 , . . . , xjn ], (y 7→ v)(xi 7→ wi )i , t)

Subst-Value-Closure-Notin
y∈
/ (xj )j∈J
([xj ]j∈J , (xi 7→ wi )i∈I , t)

y\v

([xj ]j∈J , (xi 7→ wi )i∈I , t)

Fig. 5. Value substitution

(xi )\(Ψi )

typing judgment Γ Φ , (xi : τi )i∈I , x : σ φ ⊢ t. The notation . . .
. . . denotes
the sequence of substitutions for all (xi , Ψi ), with the rightmost variable (introduced last) substituted first: in our dynamic semantics, values are captured by
the closure in the LIFO order in which their binding variables enter and leave
the lexical scope.

Substituting Values. The value substitution judgment, define in Figure 5, is
an operational counterpart to the substitution of variables in closures types.
Lemma 3 (Value substitution preserves typing). If (Γ ⊢ v : ρ), (Γ, y:ρ ⊢
w : σ), (Γ, y:ρ ⊢ σ

y\Ψ

Γ ⊢ τ ) and (w

y\v

w′ ) hold, then (Γ ⊢ w′ : τ ) holds.

The Big-Step Reduction Relation. We are now equipped to define in Figure 6 the big-step reduction relation on well-typed terms V ⊢ e =⇒ v, where
V is a mapping from the variables to values that is assumed to contain at least
V
all the free variables of e. The notation w 2 w′ denotes the sequence of substitutions for each (variable, value) pair in V2 , from the last one introduced in
the context to the first; the intermediate values are unnamed and existentially
quantified.

Tracking Data-Flow with Open Closure Types
Red-Var
V ⊢ x =⇒ V (x)

Red-Lam
V ⊢ λx.t =⇒ (dom V, ∅, λx.t)

Red-Proj
V ⊢ e =⇒ (v1 , v2 )

Red-Let
V ⊢ e1 =⇒ v1

V, V1 ⊢ u =⇒ varg

V ⊢ e2 =⇒ v2

V ⊢ (e1 , e2 ) =⇒ (v1 , v2 )

V, (x 7→ v1 ) ⊢ e2 =⇒ v2

v2

x\v1

v2′

V ⊢ let x = e1 in e2 =⇒ v2′

V ⊢ πi (e) =⇒ vi
Red-App

Red-Pair
V ⊢ e1 =⇒ v1

11

V, V1 ⊢ t =⇒ (dom V, V2 , λy.t′ )
V, V1 , V2 , y 7→ varg ⊢ t′ =⇒ w

w

y\varg

w′

V2

w′′

V, V1 ⊢ t u =⇒ w′′
Fig. 6. Big-step reduction rules
Classic-Red-Lam
c
W ⊢ λx.t =⇒ (W, λx.t)
Classic-Red-App
c
W ⊢ t =⇒ (W ′ , λy.t′ )

Classic-Red-Let
c
W ⊢ e1 =⇒ w1

c

W, x 7→ w1 ⊢ e2 =⇒ w2
c

W ⊢ let x = e1 in e2 =⇒ w2
c

W ⊢ u =⇒ warg

c

W ′ , y 7→ warg ⊢ t′ =⇒ w

c

W ⊢ t u =⇒ w
Fig. 7. Classic big-step reduction rules

We write V : Γ ⊢ if the context valuation V , mapping free variables to values,
is well-typed according to the context Γ . The definition of this judgment is given
in the full version.
Theorem 1 (Type soundness). If Γ Φ ⊢ t : σ, V : Γ ⊢ and V ⊢ t =⇒ v then
Γ ⊢ v : σ.
Finally, we recall the usual big-step semantics for the call-by-value calculus
with environments, in Figure 7, and state its equivalence with our utilitarian
semantics. Due to space restriction we will only mention the rules that differ,
and elide the equivalence proof, but the long version contains all the details.
There is a close correspondence between judgments of both semantics, but as
the value differ slightly, in the general cases the value bindings of the environment
will also differ. We state the theorem only for closed terms, but the proof will
proceed by induction on a stronger induction hypothesis using an equivalence
between non-empty contexts.
Theorem 2 (Semantic equivalence). Our reduction relation is equivalent
c
with the classic one on closed terms: ∅ ⊢ t =⇒ v holds if and only if ∅ ⊢ t =⇒ v
also holds.
To formulate our induction hypothesis, we define the equivalence judgment
c

V ⊢ v = W ⊢ w; on each side of the equal sign there is a context and a value,
the right-hand side being considered in the classical semantics.

12

Gabriel Scherer and Jan Hoffmann
c

c

∅⊢ =∅⊢
c

V ⊢ v1 = W ⊢ w1

V ⊢ =W ⊢

c

c

V ⊢ =W ⊢

V ⊢v=W ⊢w
c

c

V, x 7→ v ⊢ = W, x 7→ w ⊢
c

V ⊢ v2 = W ⊢ w2
c

V ⊢ vα = W ⊢ vα
c

c

V, xi 7→ vi ⊢ = W ′ ⊢

V ⊢ =W ⊢

c

V ⊢ ((xi 7→ vi )i∈I , λx.t) = W ⊢ (W ′ , λx.t)

V ⊢ (v1 , v2 ) = W ⊢ (w1 , w2 )

Fig. 8. Equivalence of semantic judgements.
c

The stronger version of the theorem becomes the following: if V ⊢ = W ⊢
c

c

and V ⊢ t =⇒ v and W ⊢ t =⇒ w, then V ⊢ v = W ⊢ w.

4

Dependency Information as Non-Interference

We can formulate our dependency information as a non-interference property.
Two valuations V and V ′ are Φ-equivalent, noted V =Φ V ′ , if they agree on
all variables on which they depend according to Φ. We say that e respects noninterference for Φ when, whenever V ⊢ e =⇒ v holds, then for any V ′ such
that V =Φ V ′ we have that V ′ ⊢ e =⇒ v also holds. This corresponds to the
information-flow security idea that variables marked 1 are low-security, while
variables marked 0 are high-security and should not influence the output result.
This non-interference statement requires that the two evaluations of e return
the same value v. This raises the question of what is the right notion of equality
on values. Values of atomic types have a well-defined equality, but picking the
right notion of equality for function types is more difficult. While we can state a
non-interference result on atomic values only, the inductive subcases would need
to handle higher-order cases as well.
Syntactic equality (even modulo α-equivalence) is not the right notion of
equality for closure values. Consider the following example: x:τ 0 ⊢ let y =
x in λz.z : [x:τ 0 ](z : σ 1 ) → σ. This term contains an occurrence of the variable
x, but its result does not depend on it. However, evaluating it under two different
contexts x:v and x:v ′ , with v 6= v ′ , returns distinct closures: (x 7→ v, λz.z) on
one hand, and (x 7→ v ′ , λz.z) on the other. These closures are not structurally
equal, but their difference is not essential since they are indistinguishable in any
context. Logical relations are the common technique to ignore those internal
differences and get a more observational equality on functional values. They
involve, however, a fair amount of metatheoretical effort that we would like to
avoid.
Consider a different example: x:τ 0 ⊢ λy.x : [x:τ 1 ](y:σ 0 ) → τ . Again, we could
use two contexts x:v and x:v ′ with v 6= v ′ , and we would get as a result two closures: x:v ⊢ λy.x =⇒ (x 7→ v, λy.x) and x:v ′ ⊢ λy.x =⇒ (x 7→ v ′ , λy.x).
Interestingly, these two closures are not equivalent under all contexts: any context applying the function will be able to observe the different results. However,
our notion of interference requires that they can be considered equal. This is

Tracking Data-Flow with Open Closure Types
Equiv-Pair
Γ ⊢ v1 =Φ0 v1′ : σ1

Equiv-Atom
Γ ⊢ vα =Φ0 vα : α

Γ ⊢ v2 =Φ0 v2′ : σ2

Γ ⊢ (v1 , v2 ) =Φ0 (v1′ , v2′ ) : σ1 ∗ σ2

Equiv-Closure
∀i ∈ I, Γ, (xj :τj )j<i ⊢ vi : τi
Γ Φ , (xi :τiψi )i∈I , x:σ φ ⊢ τ

13

(xi )\(Ψi )

′

Γ Φ , (xi :τiψi )i∈I , x:σ φ ⊢ t : τ

Γ Φ , x:σ φ ⊢ τ ′

∀i ∈ I, Ψi ⊆ Φ0 =⇒ vi =Φ0 vi′
′

Γ ⊢ ((xi 7→ vi )i∈I , λy.t) =Φ0 ((xi 7→ vi′ )i∈I , λy.t) : [Γ Φ ](x:σ) → τ ′
Fig. 9. Value equivalence

motivated by real-world programming languages that only output a pointer to
a closure in a program that returns a function.
While the aforementioned closures are not equal in any context, they are in
fact equivalent from the point of view of the particular dependency annotation for
which we study non-interference, namely x:τ 0 . To observe the difference between
those closures, we would need to apply the closure of type [x:τ 1 ](y : σ) → τ , so
would be in the different context x:τ 1 .
This insight leads us to our formulation of value equivalence in Figure 9.
Instead of being as modular and general as a logical-relation definition, we fix
a global dependency Φ0 that restricts which terms can be used to differentiate
values.
Our notion of value equivalence, Γ ⊢ v =Φ0 v ′ : σ is typed and includes
structural equality. In the rule Equiv-Closure, we check that the two closures
values are well-typed, and only compare captured values whose dependencies
are included in those of the global context Φ0 , as we know that the others will
not be used. This equality is tailored to the need of the non-interference result,
which only compares values resulting from the evaluation of the same subterm
– in distinct contexts.
Theorem 3 (Non-interference). If Γ Φ0 ⊢ e : σ holds, then for any contexts
V, V ′ such that V =Φ0 V ′ and values v, v ′ such that V ⊢ e =⇒ v and V ′ ⊢
e =⇒ v ′ , we have Γ ⊢ v =Φ0 v ′ : σ. In particular, if σ is an atomic type, then
v = v ′ holds.

5

Prototype Implementation

To experiment with our type system, we implemented a software prototype in
OCaml. At around one thousand lines, the implementation mainly contains two
parts.
1. For each judgement in this paper, a definition of corresponding set of inference rules along with functions for building and checking derivations.
2. A (rudimentary) command-line interface that is based on a lexer, a parser,
and a pretty-printer for the expressions, types, judgments and derivations of
our system.

14

Gabriel Scherer and Jan Hoffmann

For the scope checking judgments for context and types, the implementation
checks well-scoping of the given contexts and types. It either builds a derivation
using the well-scoping rules or fails to do so because of ill-scoped input.
For the typing judgment, the implementation performs some inference. Given
a type context Γ and an expression e, it returns Φ, σ, and a derivation Γ Φ ⊢ e : σ
if such a derivation exists. Otherwise it fails. The substitution and reduction
judgments are deterministic and computational in nature. Our implementation
takes the left-hand side a judgement (with additional parameters) and computes
the right-hand-side of the judgment along with a derivation.
Below is an example of interaction with the prototype interface:
% make
% ./closures.byte -str "let y = (y1, y2) in (y, \(x:\sigma) z)"
Parsed expression: let y = (y1, y2) in (y, λ(x:σ) z)
The variables (y1, y2, z) were unbound; we add them to the default
environment with dummy types (ty_y1, ty_y2, ty_z) and values
(val_y1, val_y2, val_z).
Inferred typing:
y1:ty_y11 ,y2:ty_y21 ,z:ty_z0 ⊢
let y = (y1, y2) in (y, λ(x:σ) z)
: ((ty_y1 * ty_y2) * [y1:ty_y10 ,y2:ty_y20 ,z:ty_z1 ](x:σ 0 ) → ty_z)
Result value:
((val_y1, val_y2), ([y1,y2,z], ((y 7→ (val_y1, val_y2))), λ(x) z))

In this example, adapted from the starting example of the article, y:σ 1 , z:τ 0 ⊢
(y, λx.z), one can observe that the value z is marked as non-needed by the
global value judgment, but needed in the type of the closure λx.z. Besides, the
computed value closure has captured the local variable y, but still references the
variables y1, y2, and z of the outer context.
The prototype can also produce ASCII rendering of the typing and reduction
derivations, when passed --typing-derivation or --reduction-derivation.
This can be useful in particular in the case of typing or reduction errors, as a
way to locate the erroneous sub-derivation.
The complete source code of the prototype is available at the following URL:
http://gallium.inria.fr/~scherer/research/open_closure_types

6

Discussion

Before we conclude, we highlight three technical points that deserve a more
in-depth discussion and that are helpful link our work to existing and future
work.
Typed Closure Conversion. It is interesting to relate our open closure types
and typed closure conversion of Minamide et al. [10]. In the classical semantics,

Tracking Data-Flow with Open Closure Types

15

a λ-term Γ ⊢ λx.e : σ1 → σ2 evaluates under the value binding W to a pair
(W, λx.e), which can be given the type (Γ ∗ (Γ → σ1 → σ2 )) (writing Γ for the
product of all types in the context). To combine closures of the same observable type that capture different environments, one needs to abstract away the
environment type by using the existential type ∃ρ.(ρ ∗ (ρ → σ → τ )).
In our specific semantics, a closure that was originally defined in the environment Γ, ∆ but is then seen in the environment Γ , only captures the values of
variables in ∆. Typed closure conversion is still possible, but we would need to
give it the less abstract type ∀Γ.∃ρ(ρ ∗ (Γ → ρ → σ1 → σ2 )). This reflects how
our open closure types allow closure types to contain static information about
variables of the current lexical context, while still allowing free composition of
closures that were initially defined in distinct environments. Our closure types
evolve from a very open type, at the closure construction point, into the usual
“closure conversion” type that is completely abstract in captured values, in the
empty environment.

Subtyping and Conservativity. As mentioned, our type system is not conservative over the simply-typed lambda-calculus because of the restriction on
substitution of function types (domain types must be preserved by substitution). This is not a surprise as our types provide more fine-grained information
without giving a way to forget some of this more precise information. Regaining
conservativity is very simple. One needs a notion of subtyping allowing to hide
variables present in closure types (eg., [Γ, ∆](x : σ1 ) → σ2 ≤ [Γ ](x : σ1 ) → σ2
whenever σ1 , σ2 are well-scoped under Γ alone). Systematically coercing all functions into closures capturing the empty environment then gives us exactly the
simply-typed lambda-calculus.

Polymorphism. We feel the two previous points could easily be formally integrated in our work. A more important difference between our prototypical
system and a realistic framework for program analysis is the lack of polymorphism. This could require significantly more work and is left for future work.
We conjecture that adding abstraction on type variables (and their annotation
φ) is direct, but a more interesting question is the abstraction over annotated
contexts Γ Φ . For example, we could want to write the following, where κ is a
formal context variable:
⊢ λf.λx.λy.f yx : ∀καβγ.([κ](x:α) → [κ](y:β) → γ) → ([κ](y:β) → [κ](x:α) → γ)
Polymorphism seems to allow greater flexibility in the analysis of functions taking functions as parameters. This use of polymorphism is related to the “resource
polymorphism” of [7], which serves the same purpose of leaving freedom to input
functions. Open closure types on the other hand, are motivated by expressions
that return function closures; the flip side of the higher-order coin.

16

7

Gabriel Scherer and Jan Hoffmann

Conclusion

We have introduced open closure types and their type theory. The technical
novelty of the type system is the ability to track intensional properties of function
application in function closures types. To maintain this information,we have to
update function types when they escape to a smaller context. This update is
performed by a novel non-trivial substitution operation. We have proved the
soundness of this substitution and the type theory for a simply-typed lambda
calculus with pairs and let bindings.
To demonstrate how our open closure types can be used in program verification we have applied this technique to track data-flow information and to ensure
non-interference in the sense of information-flow theory. We envision open closure types to be applied in the context of type systems for strong intensional
properties of higher-order programs, and this simple system to serve as a guideline for more advanced applications.
We already have preliminary results from an application of open closure types
in amortized resource analysis [7, 6]. Using them, we were for the first time able to
express a linear resource bound for the curried append function (see Section 1).
Acknowledgments. This research is based on work supported in part by
DARPA CRASH grant FA8750-10-2-0254 and NSF grant CCF-1319671. Any
opinions, findings, and conclusions contained in this document are those of the
authors and do not reflect the views of these agencies.

References
1. Abel, A.: Semi-continuous Sized Types and Termination. Log. Methods Comput.
Sci. 4(2) (2008)
2. Barthe, G., Grégoire, B., Riba, C.: Type-Based Termination with Sized Products.
In: Computer Science Logic, 17th Ann. Conf. (CSL’08). pp. 493–507 (2008)
3. Chin, W.N., Khoo, S.C.: Calculating Sized Types. High.-Ord. and Symb. Comp.
14(2-3), 261–300 (2001)
4. Hannan, J., Hicks, P., Liben-Nowell, D.: A Lifetime Analysis for Higher-Order
Languages. Tech. rep., The Pennsylvania State University (1997), http://www.
cse.psu.edu/~ hannan/papers/live.ps.gz
5. Heintze, N., Riecke, J.G.: The SLam Calculus: Programming with Secrecy and
Integrity. In: 25th Symp. on Principles of Programming Languages (POPL’98).
pp. 365–377 (1998)
6. Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis.
ACM Trans. Program. Lang. Syst. (2012)
7. Jost, S., Hammond, K., Loidl, H.W., Hofmann, M.: Static Determination of Quantitative Resource Usage for Higher-Order Programs. In: 37th Symp. on Principles
of Programming Languages (POPL’10). pp. 223–236 (2010)
8. Lago, U.D., Petit, B.: The Geometry of Types. In: 40th Symp. on Principles of
Programming Languages (POPL’13). pp. 167–178 (2013)
9. Leroy, X.: Polymorphic Typing of an Algorithmic Language. Research report 1778,
INRIA (1992)

Tracking Data-Flow with Open Closure Types

17

10. Minamide, Y., Morrisett, J.G., Harper, R.: Typed Closure Conversion. In: 23rd
Symp. on Principles of Programming Languages (POPL’96). pp. 271–283 (1996)
11. Moggi, E., Taha, W., Zine El-abidine Benaissa, Sheard, T.: An idealized metaml:
Simpler, and more expressive. In: 8th Europ. Symp. on Programming (ESOP’99).
pp. 193–207 (1999)
12. Nanevski, A., Pfenning, F., Pientka, B.: Contextual Modal Type Theory. ACM
Trans. Comput. Log. 9(3) (2008)
13. Petricek, T., Orchard, D., Mycroft, A.: Coeffects: Unified static analysis of contextdependence. In: Automata, Languages, and Programming - 40th Int. Colloq.
(ICALP’13). pp. 385–397 (2013)
14. Pientka, B., Dunfield, J.: Programming with Proofs and Explicit Contexts. In: 10th
International Conference on Principles and Practice of Declarative Programming
(PPDP’08). pp. 163–173 (2008)
15. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
16. Stampoulis, A., Shao, Z.: Static and User-Extensible Proof Checking. In: 39th
Symp. on Principles of Programming Languages (POPL’12). pp. 273–284 (2012)
17. Tsukada, T., Igarashi, A.: A Logical Foundation for Environment Classifiers. Logical Methods in Computer Science 6(4) (2010)

