Intersection types for unbind and rebind∗
Mariangiola Dezani-Ciancaglini

Paola Giannini

Dip. di Informatica, Univ. di Torino, Italy

Dip. di Informatica, Univ. del Piemonte Orientale, Italy

Elena Zucca
DISI, Univ. di Genova, Italy

We define a type system with intersection types for an extension of lambda-calculus with unbind and
rebind operators. In this calculus, a term t with free variables x1 , . . . , xn , representing open code, can
be packed into an unbound term h x1 , . . . , xn | t i, and passed around as a value. In order to execute
inside code, an unbound term should be explicitly rebound at the point where it is used. Unbinding
and rebinding are hierarchical, that is, the term t can contain arbitrarily nested unbound terms, whose
inside code can only be executed after a sequence of rebinds has been applied. Correspondingly,
types are decorated with levels, and a term has type τ k if it needs k rebinds in order to reduce to
a value of type τ . With intersection types we model the fact that a term can be used differently in
contexts providing different numbers of unbinds. In particular, top-level terms, that is, terms not
requiring unbinds to reduce to values, should have a value type, that is, an intersection type where
at least one element has level 0. With the proposed intersection type system we get soundness under
the call-by-value strategy, an issue which was not resolved by previous type systems.

Introduction
In previous work [12, 13] we introduced an extension of lambda-calculus with unbind and rebind operators, providing a simple unifying foundation for dynamic scoping, rebinding and delegation mechanisms.
This extension relies on the following ideas:
• A term h Γ | t i, where Γ is a set of typed variables called unbinders, is a value, of a special type
code, representing “open code” which may contain free variables in the domain of Γ.
• To be used, open code should be rebound through the operator t[r], where r is a (typed) substitution
(a map from typed variables to terms). Variables in the domain of r are called rebinders. When
the rebind operator is applied to a term h Γ | t i, a dynamic check is performed: if all unbinders are
rebound with values of the required types, then the substitution is performed, otherwise a dynamic
error is raised.
For instance, the term1 h x, y | x + y i[x 7→ 1, y 7→ 2] reduces to 1 + 2, whereas both h x, y | x + y i[x 7→ 1]
and h x:int | x + 1 i[x:int → int 7→ λ y.y + 1] reduce to error.
Unbinding and rebinding are hierarchical, that is, the term t can contain arbitrarily nested unbound
terms, whose inside code can only be executed after a sequence of rebinds has been applied2 . For
instance, two rebinds must be applied to the term h x | x + h x | x i i in order to get an integer:
h x | x + h x | x i i[x 7→ 1][x 7→ 2] −→ (1 + h x | x i)[x 7→ 2]
−→ (1[x 7→ 2]) + (h x | x i[x 7→ 2])
−→⋆ 1 + 2
∗ This work

has been partially supported by MIUR DISCO - Distribution, Interaction, Specification, Composition for Object
Systems, and IPODS - Interacting Processes in Open-ended Distributed Systems.
1 In the examples we omit type annotations when they are irrelevant.
2 See the Conclusion for more comments on this choice.
E. Pimentel, B. Venneri and J. Wells (Eds.): Workshop on
Intersection Types and Related Systems 2010 (ITRS 2010).
EPTCS 45, 2011, pp. 45–58, doi:10.4204/EPTCS.45.4

c Dezani, Giannini and Zucca
This work is licensed under the
Creative Commons Attribution License.

Intersection types for unbind and rebind

46

Correspondingly, types are decorated with levels, and a term has type τ k if it needs k rebinds in order
to reduce to a value of type τ . With intersection types we model the fact that a term can be used differently
in contexts which provide a different number k of unbinds. For instance, the term h x | x + h x | x i i above
has type int2 ∧ code0 , since it can be safely used in two ways: either in a context which provides two
rebinds, as shown above, or as a value of type code, as, e.g., in:
(λ y.y[x 7→ 1][x 7→ 2]) h x | x + h x | x i i
On the other side, the term h x | x + h x | x i i does not have type int1 , since by applying only one rebind
with [x 7→ 1] we get the term 1 + h x | x i which is stuck.
The use of intersection types allows us to get soundness w.r.t. the call-by-value strategy. This issue
was not resolved by previous type systems [12, 13] where, for this reason, we only considered the callby-name reduction strategy. To see the problem, consider the following example.
The term
(λ y.y[x 7→ 2]) (1 + h x | x i)
is stuck in the call-by-value strategy, since the argument is not a value, hence should be ill typed, even
though the argument has type int1 , which is a correct type for the argument of the function. By using
intersection types, this can be enforced by requiring arguments of functions to have value types, that is,
intersections where (at least) one of the conjuncts is a type of level 0. In this way, the above term is ill
typed. Note that a call-by-name evaluation of the above term gives
(λ y.y[x 7→ 2]) (1 + h x | x i)

−→ (1 + h x | x i)[x 7→ 2]
−→ (1[x →
7 2]) + (h x | x i[x 7→ 2])
−→⋆ 1 + 2.

Instead, the term (λ y.y[x 7→ 2]) h x | 1 + x i is well typed, and it reduces as follows in both call-by-value
and call-by-name strategies:
(λ y.y[x 7→ 2]) h x | 1 + x i −→ h x | 1 + x i[x 7→ 2]
−→ 1 + 2.
It is interesting to note that this phenomenon is due to the possibility for operators (in our case for
+) of acting on arguments which are unbound terms. This design choice is quite natural in view of discussing open code, as in MetaML [23]. In pure λ -calculus there is no closed term which converges when
evaluated by the lazy call-by-name strategy and is stuck when evaluated by the call-by-value strategy.
Instead there are closed terms, like (λ x.λ y.y)((λ z.z z)(λ z.z z)), which converge when evaluated by the
lazy call-by-name strategy and diverge when evaluated by the call-by-value strategy, and open terms,
like (λ x.λ y.y)z, which converge when evaluated by the lazy call-by-name strategy and are stuck when
evaluated by the call-by-value strategy.3
In summary, the contribution of this paper is the following. We define a type system for the calculus
of Dezani et al. [12, 13], where, differently from those papers, we omit types on the lambda-binders in
order to get the whole expressivity of the intersection type constructor [25]. The type system shows, in
our opinion, an interesting and novel application of intersection types. Indeed, they handle in a uniform
way the three following issues.
• Functions may be applied to arguments of (a finite set of) different types.
• A term can be used differently in contexts providing different numbers of unbinds. Indeed, an
intersection type for a term includes a type of form τ k if the term needs k rebinds in order to
reduce to a value of type τ .
3 Note

that following Pierce [18] we consider only λ -abstractions as values, while for Plotkin [19] also variables are values.

Dezani, Giannini and Zucca

47

• Most notably, the type system guarantees soundness for the call-by-value strategy, by requiring
that top-level terms, that is, terms which do not require unbinds to reduce to values, should have
value types.
Paper Structure. In Section 1 we introduce the syntax and the operational semantics of the language.
In Section 2 we define the type system and prove its soundness in Section 3. In Section 4 we discuss
related and further work.

1

Calculus

The syntax and reduction rules of the calculus are given in Figure 1.
t
Γ
r

:: = x | n | t1 + t2 | λ x.t | t1 t2 | h Γ | t i | t[r] | error term
:: = x1 :T1 , . . . , xm :Tm
type context
:: = x1 :T1 →
7 t1 , . . . , xm :Tm 7→ tm
(typed) substitution

v :: = λ x.t | h Γ | t i | n
rv :: = x1 :T1 7→ v1 , . . . , xm :Tm 7→ vm
E
σ

value
value substitution

:: = [ ] | E + t | n + E | E t | v E | t[r, x:T 7→ E ]
:: = x1 →
7 v1 , . . . , xm 7→ vm
n1 + n2 −→ n
(λ x.t) v −→ t{x 7→ v}
h Γ | t i[rv ] −→ t{subst(rv )|dom(Γ) }
h Γ | t i[rv ] −→ error
n[rv ] −→ n
(t1 + t2 )[rv ] −→ t1 [rv ] + t2 [rv ]
(λ x.t)[rv ] −→ λ x.t[rv ]
(t1 t2 )[rv ] −→ t1 [rv ] t2 [rv ]
t[r][rv ] −→ t′ [rv ]
error[rv ] −→ error
t −→ t′

ñ = ñ1 +Z ñ2

(C TX )

(S UM )
(A PP )

if
if

Γ ⊆ tenv(rv )
Γ 6⊆ tenv(rv )

(R EBIND U NBINDY ES )
(R EBIND U NBIND N O )
(R EBIND N UM )
(R EBIND S UM )
(R EBINDA BS )
(R EBINDA PP )

if

t[r] −→ t′

(R EBIND R EBIND )
(R EBIND E RROR )

t −→ error

E 6= [ ]

E [t] −→ E [t′ ]

if

evaluation context
(untyped) substitution

E 6= [ ]

E [t] −→ error

(C TX E RROR )

Figure 1: Syntax and reduction rules
Terms of the calculus are the λ -calculus terms, the unbind and rebind constructs, and the dynamic
error. Moreover, we include integers with addition to show how unbind and rebind behave on primitive
data types. Unbinders and rebinders are annotated with types T, which will be described in the following
section. Here it is enough to assume that they include standard int and functional types. Type contexts
and substitutions are assumed to be maps, that is, order is immaterial and variables cannot appear twice.

Intersection types for unbind and rebind

48

Free variables and application of a substitution to a term are defined in Figure 2. Note that an
unbinder behaves like a λ -binder: for instance, in a term of shape h x | t i, the unbinder x introduces a
local scope, that is, binds free occurrences of x in t. Hence, a substitution for x is not propagated inside
t. Moreover, a condition, which prevents capture of free variables similar to the λ -abstraction case is
needed. For instance, the term (λ y.h x | y i) (λ z.x) reduces to h x | y i{y 7→ λ z.x} which is stuck, i.e., it
does not reduce to h x | λ z.x i, which would be wrong.
However, λ -binders and unbinders behave differently w.r.t. α -equivalence. A λ -binder can be renamed, as usual, together with all its bound variable occurrences, whereas this is not safe for an unbinder:
for instance, h x | x + 1 i[x 7→ 2] is not equivalent to h y | y + 1 i[x 7→ 2]. Only a global renaming, e.g.,
leading to h y | y + 1 i[y 7→ 2], would be safe.4

FV(x) = {x}
FV(n) = 0/
FV(t1 + t2 ) = FV(t1 ) ∪ FV(t2 )
FV(λ x.t) = FV(t) \ {x}
FV(t1 t2 ) = FV(t1 ) ∪ FV(t1 )
FV(h Γ | t i) = FV(t) \ dom(Γ)
FV(t[r]) = FV(t) ∪ FV(subst(r))
S
FV(x1 7→ t1 , . . . , xm 7→ tm ) = i∈1..m FV(ti )
x{σ } = v if σ (x) = v
x{σ } = x if x 6∈ dom(σ )
n{σ } = n
(t1 + t2 ){σ } = t1 {σ } + t2 {σ }
(λ x.t){σ } = λ x.t{σ\{x} } if x 6∈ FV(σ )
(t1 t2 ){σ } = t1 {σ } t2 {σ }
h Γ | t i{σ } = h Γ | t{σ\dom(Γ) } i if dom(Γ) ∩ FV(σ ) = 0/
t[x1 :T1 7→ t1 , . . . , xm :Tm 7→ tm ]{σ } = t{σ }[x1 :T1 7→ t1 {σ }, . . . , xm :Tm 7→ tm {σ }]
Figure 2: Free variables and application of substitution
The call-by-value operational semantics is described by the reduction rules and the definition of the
evaluation contexts E . We denote by ñ the integer represented by the constant n, by tenv(r) and subst(r)
the type context and the untyped substitution, respectively, extracted from a typed substitution r, by dom
the domain of a map, by σ|{x1 ,...,xn } and σ\{x1 ,...,xn } the substitutions obtained from σ by restricting to or
removing variables in set {x1 , . . . , xn }, respectively.
Rules for sum and application (of a lambda to a value) are standard. The (R EBIND ) rules determine
what happens when a rebind is applied to a term. There are two rules for the rebinding of an unbound
term. Rule (R EBIND U NBINDY ES ) is applied when the unbound variables are all present (and of the required
types), in which case the associated values are substituted, otherwise rule (R EBIND U NBIND N O) produces a
4 A more sophisticated solution [5] allows local renaming of unbinders by a “precompilation” step annotating variables with
indexes, which can be α -renamed, but are not taken into account by the rebinding mechanism. Indeed, variable occurrences
which are unbinders, rebinders, or bound to an unbinder, actually play the role of names rather than standard variables. Note
that variables in a rebinder, e.g., x in [x 7→ 2], are not bindings, and x is neither a free, nor a bound variable. See the Conclusion
for more comments on this difference.

Dezani, Giannini and Zucca

49

dynamic error. This is formally expressed by the side condition Γ ⊆ tenv(r). Note that a rebind applied to
a term may be stuck even though the variables are all present and of the right type, when the substitution
is not defined. This may be caused by the fact that when applied to an unbound term, a substitution
could cause capture of free variables (see the example earlier in this section). Rebinding a term which
is a number or error does not affect the term. On sum, abstraction and application, the rebind is simply
propagated to subterms, and if a rebind is applied to a rebound term, (R EBIND R EBIND ), the inner rebind is
applied first. The evaluation order is specified by rule (C TX ) and the definition of contexts, E , that gives
the call-by-value strategy. Finally rule (C TX E RROR ) propagates errors. To make rule selection deterministic,
rules (C TX ) and (C TX E RROR ) are applicable only when E 6= [ ]. As usual −→⋆ is the reflexive and transitive
closure of −→.
When a rebind is applied, only variables which were explicitly specified as unbinders are replaced.
For instance, the term h x | x + y i[x 7→ 1, y 7→ 2] reduces to 1 + y rather than to 1 + 2. In other words, the
unbinding/rebinding mechanism is explicitly controlled by the programmer.
Looking at the rules we can see that there is no rule for the rebinding of a variable. Indeed, it will be
resolved only when the variable is substituted as effect of a standard application. For instance, the term
(λ y.y[x 7→ 2]) h x | x + 1 i reduces to h x | x + 1 i[x 7→ 2].
Note that in rule (R EBINDA BS ), the binder x of the λ -abstraction does not interfere with the rebind,
even in case x ∈ dom(r). Indeed, rebind has no effect on the free occurrences of x in the body of the λ abstraction. For instance, (λ x.x + h x | x i)[x 7→ 1] 2, which is α -equivalent to (λ y.y + h x | x i)[x 7→ 1] 2,
reduces in some steps to 2 + 1. On the other hand, both λ -binders and unbinders prevent a substitution
for the corresponding variable from being propagated in their scope, for instance:
h x, y | x + λ x.(x + y) + h x | x + y i i[x 7→ 2, y 7→ 3] −→ 2 + (λ x.x + 3) + h x | x + 3 i
A standard (static) binder can also affect code to be dynamically rebound, when it binds free variables
in a substitution r, as shown by the following example:
(λ x.λ y.y[x 7→ x] + x) 1 h x | x + 2 i −→ (λ y.y[x 7→ 1] + 1) h x | x + 2 i
−→ h x | x + 2 i[x 7→ 1] + 1 −→ 1 + 2 + 1.
Note that in [x 7→ x] the two occurrences of x refer to different variables. Indeed, the second is bound by
the external lambda whereas the first one is a rebinder.

2

Type system

We have three kinds of types: primitive types τ , value types V, and term types T; see Figure 3.
T :: = τ k | T1 ∧ T2
(k ∈ N) term type
0
value type
V :: = τ | V ∧ T
τ :: = int | code | T → T ′
primitive type
Figure 3: Types
Primitive types characterise the shape of values. In our case we have integers (int), functions (T →
T ′ ), and code, which is the type of a term h Γ | t i, that is, (possibly) open code.
Term types are primitive types decorated with a level k or intersection of types. If a term has type τ k ,
then by applying k rebind operators to the term we get a value of primitive type τ . We abbreviate a type
τ 0 by τ . Terms have the intersection type T1 ∧ T2 when they have both types T1 and T2 . On intersection

Intersection types for unbind and rebind

50

we have the usual congruence due to idempotence, commutativity, associativity, and distributivity over
arrow type, defined in the first four clauses of Figure 4.
Value types characterise terms that reduce to values, so they are intersections in which (at least) one
of the conjuncts must be a primitive type of level 0. For instance, the term h x : int | h y : int | x + y i i
has type code0 ∧ code1 ∧ int2 , since it is code that applying one rebinding produces code that, in turn,
applying another rebinding produces an integer. The term h x : int | x + h y : int | y + 1 i i has type
code0 ∧ int2 since it is code that applying one rebinding produces the term n + h y : int | y + 1 i, for
some n. Both code0 ∧ code1 ∧ int2 and code0 ∧ int2 are value types, whereas int1 , which is the
type of term n + h y : int | y + 1 i, is not a value type. Indeed, in order to produce an integer value the
term must be rebound (at least) once. The typing rule for application enforces the restriction that a term
may be applied only to terms reducing to values, that is the call-by-value strategy. Similar for the terms
associated with variables in a substitution.
V
V
Let I = {1, . . . , m}. We write i∈I τiki and i∈1..m τiki to denote τ1k1 ∧ · · · ∧ τmkm . Note that any type T
V
V
is such that T = i∈1..m τiki , for some τi and ki (i ∈ 1..m). Given a type T = i∈1..m τiki , with (T)⊕h we
V
denote the type i∈1..m τiki +h .
T ≡ T ∧T

T1 ∧ T2 ≡ T2 ∧ T1

(T → T1 )k ∧ (T → T2 )k ≡ (T → T1 ∧ T2 )k

T1 ∧ (T2 ∧ T3 ) ≡ (T1 ∧ T2 ) ∧ T3
(T ′ → (T)⊕h )k+1 ≡ (T ′ → (T)⊕(h+1) )k

Figure 4: Congruence on types
Figure 4 defines congruence on types. In addition to the standard properties of intersection, the
last clause says that the level of function types can be switched with the one of their results. That is,
unbinding and lambda-abstraction commute. So rebinding may be applied to lambda-abstractions, since
reduction rule (R EBINDA BS ) pushes rebinding inside. For instance, the terms h Γ | λ x.t i and λ x.h Γ | t i
may be used interchangeably.
intk ≤ intk+1
T2 ≤ T1

T1′ ≤ T2′

(T1 → T1′ )k ≤ (T2 → T2′ )k
T1 ≤ T2

T2 ≤ T3

T1 ≤ T3

T1 ∧ T2 ≤ T1
T1 ≤ T1′

T2 ≤ T2′

T1 ∧ T2 ≤ T1′ ∧ T2′
T1 ≡ T2
T1 ≤ T2

Figure 5: Subtyping on types
Subtyping, defined in Figure 5, expresses subsumption, that is, if a term has type T1 , then it can be
used also in a context requiring a type T2 with T1 ≤ T2 . For integer types it is justified by the reduction
rule (R EBIND N UM ), since once we obtain an integer value any number of rebindings may be applied.5
For intersections, it is intersection elimination. The other rules are the standard extension of subtyping
5 Note

that the generalisation of intk ≤ intk+1 to T k ≤ T k+1 is sound but useless.

Dezani, Giannini and Zucca

51

to function and intersection types, transitivity, and the fact that congruent types are in the subtyping
relation.
(T-I NTER )

(T-N UM )

(T-A BS )

Γ ⊢ t : T1 Γ ⊢ t : T2
Γ ⊢ t : T1 ∧ T2

Γ ⊢ n : int0

(T-S UM )

Γ, x:T ⊢ t : T ′
Γ ⊢ λ x.t : (T → T ′ )0

(T-U NBIND -0)

(T-R EBIND )

(T-S UB )

Γ ⊢ t : T T ≤ T′
Γ ⊢ t : T′

Γ ⊢ t1 : intk Γ ⊢ t2 : intk
Γ ⊢ t1 + t2 : intk
(T-A PP )

Γ, Γ′ ⊢ t : T
Γ ⊢ h Γ′ | t i : code0

Γ(x) = T
Γ⊢x:T

(T-E RROR )

Γ ⊢ error : T

Γ ⊢ t1 : (V → T)0 Γ ⊢ t2 : V
Γ ⊢ t1 t2 : T

(T-U NBIND )

Γ ⊢ t : (T)⊕1 Γ ⊢ r : ok
Γ ⊢ t[r] : T

(T-VAR )

Γ, Γ′ ⊢ t : T
Γ ⊢ h Γ′ | t i : (T)⊕1

(T-R EBINDING )

Γ ⊢ ti : Vi Vi ≤ Ti (i ∈ 1..m)
Γ ⊢ x1 :T1 7→ t1 , . . . , xm :Tm 7→ tm : ok

Figure 6: Typing rules
Typing rules are defined in Figure 6. We denote by Γ, Γ′ the concatenation of the two type contexts
Γ and Γ′ with disjoint domains, which turns out to be a type context (map) as well.
A number has the value type int0 . With rule (T-S UB ), however, it can be given the type intk for any
k. Rule (T-S UM ) requires that both operands of a sum have the same type, with rule (T-S UB ) the term can be
given as level the biggest level of the operands. Rule (T-E RROR ) permits the use of error in any context.
In rule (T-A BS ) the initial level of a lambda abstraction is 0 since the term is a value. With rule (T-S UB ) we
may decrease the level of the return type by increasing, by the same amount, the level of the whole arrow
type. This is useful since, for example, we can derive
⊢ λ x.x + h y:int | y + h z:int | z i i : (int → int1 )1
by first deriving the type (int → int2 )0 for the term, and then applying (T-S UB ). Therefore, we can give
type to the rebinding of the term, by applying rule (T-R EBINDING ) that requires that the term to be rebound
has level bigger than 0, and whose resulting type is decreased by one. For example,
⊢ (λ x.x + h y:int | y + h z:int | z i i)[y:int 7→ 5] : (int → int1 )0
which means that the term reduces to a lambda abstraction, i.e., to a value, which applied to an integer
needs one rebind in order to produce an integer or error. The rule (T-A PP ) assumes that the type of the
function be a level 0 type. This is not a restriction, since using rule (T-S UB ), if the term has any function
type it is possible to assign it a level 0 type. The type of the argument must be a value type. This
condition is justified by the example given in the introduction.
The two rules for unbinds reflect the fact that code is both a value, and as such has type code0 ,
and also a term that needs one more rebinding than its body in order to produce a value. Taking the
intersection of the types derived for the same unbind with these two rules we can derive a value type for
the unbind and use it as argument of an application. For example typing h y : int | y i by code0 ∧ int1
we can derive type int0 for the term

Intersection types for unbind and rebind

52

(λ x.2 + x[y: int 7→ 3])h y : int | y i.
The present type system only takes into account the number of rebindings which are applied to a
term, whereas no check is performed on the name and the type of the variables to be rebound. This
check is performed at runtime by rules (R EBIND U NBINDY ES ) and (R EBIND U NBIND N O ). In papers introducing the
calculus [12, 13] we have also provided an alternative type system (for the call-by-name calculus) such
that this check is statically perfomed, see the Conclusion for more comments.
Note that terms which are stuck since application of substitution is undefined, such as the previous
example (λ y.h x | y i) (λ z.x), are ill typed. Indeed, in the typing rules for unbinding, unbinders are
required to be disjoint from outer binders, and there is no weakening rule. Hence, a type context for the
example should simultaneously include a type for x and not include a type for x in order to type λ z.x and
λ y.h x | y i, respectively. For the same reason, a peculiarity of the given type system is that weakening
does not hold, in spite of the fact that no notion of linearity is enforced.

3

Soundness of the type system

The type system is safe since types are preserved by reduction and a closed term with value type is
a value or error or can be reduced. In other words the system has both the subject reduction and the
progress properties. Note that a term that may not be assigned a value type can be stuck, as for example
1 + h x:int | x i, which has type int1 .
The proof of subject reduction (Theorem 5) is standard. We start with a lemma (Lemma 1) on the
properties of the equivalence and pre-order relation on types, which can be easily shown by induction on
their definitions. Then we give an Inversion Lemma (Lemma 2), a Substitution Lemma (Lemma 3) and
a Context Lemma (Lemma 4). Lemmas 2 and 3 can be easily shown by induction on type derivations.
The proof of Lemma 4 is by structural induction on contexts.
Lemma 1
1. If

V

i∈I (Ti

V

→ Ti′ )0 ≡ (T → T ′ )0 , then Ti ≡ T for all i ∈ I and

V

′
i∈I Ti

≡ T ′.

2. If i∈I (Ti → Ti′ )0 ≤ T, then there are L, T̂l , T̂l′ , (l ∈ L), such that T ≡
l ∈ L there is Jl ⊆ I with

V

l∈L (T̂l

→ T̂l′ )0 , and for all

• T̂l ≤ T j for all j ∈ Jl , and
V
• j∈Jl T̂ ′j ≤ Tl′ .
Lemma 2 (Inversion Lemma)
1. If Γ ⊢ x : T, then Γ(x) ≤ T.
2. If Γ ⊢ n : T, then int0 ≤ T.
3. If Γ ⊢ t1 + t2 : T, then int0 ≤ T and Γ ⊢ t1 : T and Γ ⊢ t2 : T.
4. If Γ ⊢ λ x.t : T, then there are m, Ti , Ti′ (i ∈ 1..m) such that T ≡
(i ∈ 1..m).

V

i∈1..m (Ti

→ Ti′ )0 , and Γ, x:Ti ⊢ t : Ti′

5. If Γ ⊢ t1 t2 : T, then there is V such that Γ ⊢ t1 : (V → T)0 and Γ ⊢ t2 : V.
V

ki
i∈1..m τi , then
: τiki −1 for all ki >

6. If Γ ⊢ h Γ′ | t i :

• Γ, Γ′ ⊢ t
• τi = code for all ki = 0.

0, and

Dezani, Giannini and Zucca

53

When m = 1 and k1 = 0 we also have Γ, Γ′ ⊢ t : T ′ , for some T ′ .
7. If Γ ⊢ t[r] :

V

ki
i∈1..m τi ,

then Γ ⊢ t :

V

ki +1
i∈1..m τi

and Γ ⊢ r : ok.

8. If Γ ⊢ x1 :T1 7→ t1 , . . . , xm :Tm 7→ tm : ok, then there are Vi ≤ Ti for i ∈ 1..m such that Γ ⊢ ti : Vi .
Proof By induction on typing derivations. We only consider some interesting cases.
For Point (4), if the last applied rule is (T-S UB ), then the result follows by induction from Lemma 1(2).
For the same Point if the last applied rule is (T-I NTER ), then let Γ ⊢ λ x.t : T ∧ T ′ . By induction hypothesis
there are m, m′ , Ti , T ′j , T̂i , T̂ ′j (i ∈ 1..m, j ∈ 1..m′ ) such that:
• T≡

V

i∈1..m (Ti

→ T̂i )0 ,

• Γ, x:Ti ⊢ t : T̂i (i ∈ 1..m),
• T′ ≡

V

′
j∈1..m′ (T j

→ T̂ ′j )0 , and

• Γ, x:T ′j ⊢ t : T̂ ′j ( j ∈ 1..m′ ).
V

V

Therefore T ∧ T ′ ≡ i∈1..m (Ti → T̂i )0 ∧ j∈1..m′ (T ′j → T̂ ′j )0 .
For Point (5) if the last applied rule is (T-I NTER ), then let Γ ⊢ t1 t2 : T1 ∧ T2 . By induction hypothesis
we have Γ ⊢ t1 : Vi → Ti and Γ ⊢ t2 : Vi , for some Vi , i = 1, 2. We derive Γ ⊢ t1 : (V1 → T1 ) ∧ (V2 → T2 )
and Γ ⊢ t2 : V1 ∧ V2 by rule (T-I NTER ). Since (V1 → T1 ) ∧ (V2 → T2 ) ≤ V1 ∧ V2 → T1 ∧ T2 , applying rule
(T-S UB ) we get Γ ⊢ t1 : V1 ∧ V2 → T1 ∧ T2 .
Lemma 3 (Substitution Lemma) If Γ, x:T ⊢ t : T ′ , and Γ ⊢ v : T, then Γ ⊢ t{x 7→ v} : T ′ .
Lemma 4 (Context Lemma) Let Γ ⊢ E [t] : T, then
• Γ ⊢ t : T ′ for some T ′ , and
• if Γ ⊢ t′ : T ′ , then Γ ⊢ E [t′ ] : T, for all t′ .
Theorem 5 (Subject Reduction) If Γ ⊢ t : T and t −→ t′ , then Γ ⊢ t′ : T.
Proof By induction on reduction derivations. We only consider some interesting cases.
If the applied rule is (A PP ), then
(λ x.t) v −→ t{x 7→ v}
From Γ ⊢ (λ x.t) v : T by Lemma 2, case (5) we have that: there is V such that Γ ⊢ λ x.t : (V → T)0
and Γ ⊢ v : V. By Lemma 2, case (4) we have that there are m, Ti , Ti′ (i ∈ 1..m) such that (V → T)0 ≡
V
(T → Ti′ )0 , and Γ, x:Ti ⊢ t : Ti′ (i ∈ 1..m). From Lemma 1(1) we get Ti ≡ V for all i ∈ 1..m and
Vi∈1..m ′i
i∈1..m Ti ≡ T. Then we can derive Γ, x:V ⊢ t : T using rules (T-S UB ) and (T-I NTER ). By Lemma 3 we conclude that Γ ⊢ t{x 7→ v} : T.
If the applied rule is (R EBIND U NBINDY ES ), then
h Γ′ | t i[rv ] −→ t{subst(rv )|dom(Γ′ ) }

Γ′ ⊆ tenv(rv )

v
′
v
′
Let r|dom(Γ
′ ) = x1 :T1 7→ v1 , . . . , xm :Tm 7→ vm . Since Γ ⊆ tenv(r ) we have that Γ = x1 :T1 , . . . , xm :Tm .

V

V

From Γ ⊢ h Γ′ | t i[rv ] : T by Lemma 2, case (7), we get T = i∈1..n τiki and Γ ⊢ h Γ′ | t i : i∈1..n τiki +1 and
V
Γ ⊢ rv : ok. From Lemma 2, case (6), we have that Γ, Γ′ ⊢ t : i∈1..n τiki . Moreover, by Lemma 2, case (8),
and rule (T-S UB ) we have that Γ ⊢ rv : ok implies that Γ ⊢ vi : Ti for i ∈ 1..m. Applying m times Lemma 3,
we derive Γ ⊢ t{subst(rv )|dom(Γ′ ) } : T.

Intersection types for unbind and rebind

54

In order to show the Progress Theorem (Theorem 9), we start as usual with a Canonical Forms
Lemma (Lemma 6). Then we state the standard relation between type contexts and free variables (Lemma
7), and lastly we prove that all closed terms which are rebound terms always reduce (Lemma 8).
Lemma 6 (Canonical Forms)
1. If ⊢ v : int0 , then v = n.
2. If ⊢ v : code0 , then v = h Γ | t i.
3. If ⊢ v : (T → T ′ )0 , then v = λ x.t.
Proof By case analysis on the shape of values.
Lemma 7 If Γ ⊢ t : T, then FV(t) ⊆ dom(Γ).
Proof By induction on type derivations.
Lemma 8 If t = t′ [rv ] for some t′ and rv , and FV(t) = 0,
/ then t −→ t′′ for some t′′ .
Proof Let t = t′ [r1v ] · · · [rnv ] for some t′ , r1v , . . . , rnv (n ≥ 1), where t′ is not a rebind. The proof is by
mathematical induction on n.
If n = 1, then one of the reduction rules is applicable to t′ [r1v ]. Note that, if t′ = h Γ | t1 i, then rule
(R EBIND U NBINDY ES ) is applicable in case Γ is a subset of the type environment associated with r1v , otherwise
rule (R EBIND U NBIND N O ) is applicable.
v ]. If FV(t′ [rv ] · · · [rv ]) = 0,
Let t = t′ [r1v ] · · · [rn+1
/ then also FV(t′ [r1v ] · · · [rnv ]) = 0.
/ By induction hypothesis
1
n+1
′
v
v
′′
′
v
v
′′
v
t [r1 ] · · · [rn ] −→ t , therefore t [r1 ] · · · [rn+1 ] −→ t [rn+1 ] with rule (R EBIND R EBIND ).
Theorem 9 (Progress) If ⊢ t : V, then either t is a value, or t = error, or t −→ t′ for some t′ .
Proof By induction on the derivation of ⊢ t : V with case analysis on the last typing rule used.
If t is not a value or error, then the last applied rule in the type derivation cannot be (T-N UM ), (T-E RROR ),
or (T-U NBIND ). Moreover the typing environment for the expression is empty, hence
by Lemma 7 the last applied rule cannot be (T-VAR ).
(T-A BS ), (T-U NBIND -0),

If the last applied rule is
theorem holds by induction.

(T-S UB ),

note that T ≤ V implies that T is a value type, and therefore the

If the last applied rule is (T-A PP ), then t = t1 t2 , and taking into account that the resulting type must be
a value type:
⊢ t1 : V ′ → V ⊢ t2 : V ′
⊢ t1 t2 : V
If t1 is not a value or error, then, by induction hypothesis, t1 −→ t1′ . So t1 t2 = E [t1 ] with E = [ ] t2 , and by
rule (C TX ), t1 t2 −→ t1′ t2 . If t1 is error, we can apply rule (C ONT E RROR ) with the same context. It t1 is a value
v, and t2 is not a value or error, then, by induction hypothesis, t2 −→ t2′ . So t1 t2 = E [t2 ] with E = v [ ],
and by rule (C TX ), v t2 −→ v t2′ . If t2 is error, we can apply rule (C ONT E RROR ) with the same context. If both
t1 and t2 are values, then by Lemma 6, case (3), t1 = λ x.t′ and, therefore, we can apply rule (A PP ).
If the last applied rule is (T-S UM ), then t = t1 + t2 and taking into account that the resulting type must
be a value type:
⊢ t1 : int0 ⊢ t2 : int0
⊢ t1 + t2 : int0

Dezani, Giannini and Zucca

55

If t1 is not a value or error, then, by induction hypothesis, t1 −→ t1′ . So by rule (C TX ), with context
E = [ ] + t2 , we have t1 + t2 −→ t1′ + t2 . If t1 is error, we can apply rule (C ONT E RROR ) with the same context.
If t1 is a value, then, by Lemma 6, case (1), t1 = n1 . Now, if t2 is not a value or error, then, by induction
hypothesis, t2 −→ t2′ . So by rule (C TX ), with context E = n1 + [ ], we get t1 + t2 −→ t1 + t2′ . If t2 is error,
we can apply rule (C ONT E RROR ) with the same context. Finally, if t2 is a value, then by Lemma 6, case (1),
t2 = n2 . Therefore rule (S UM ) is applicable.
If the last applied rule is (T-R EBIND ), then t = t′ [r]. If some term ti in r is not a value, then by Lemma
2(7) and (8) ti is typed with a value type, and therefore ti −→ ti′ by induction, so t reduces using rule
(C TX ). Otherwise t = t′ [rv ]. Since ⊢ t′ [rv ] : V, we have that FV(t′ [rv ]) = 0
/ by Lemma 7. From Lemma 8
we get that t′ [rv ] −→ t′′ for some t′′ .

4

Conclusion

We have defined a type system with intersection types for an extension of lambda-calculus with unbind
and rebind operators introduced in previous work [12, 13]. Besides the traditional use of intersection
types for typing (finitely) polymorphic functions, this type system shows two novel applications:
• An intersection type expresses that a term can be used in contexts which provide a different number
of unbinds.
• In particular, an unbound term can be used both as a value of type code and in a context providing
an unbind.
This type system could be used for call-by-name with minor modifications. However, the call-byvalue case is more significant since the condition that the argument of an application must reduce to a
value can be nicely expressed by the notion of value type.
Moreover, only the number of rebindings which are applied to a term is taken into account, whereas
no check is performed on the name and the type of the variables to be rebound; this check is performed
at runtime. This solution is convenient, e.g., in distributed scenarios where code is not all available at
compile time, or in combination with delegation mechanisms where, in case of dynamic error due to an
absent/wrong binding, an alternative action is taken. In papers introducing the calculus [12, 13] we have
also provided an alternative type system (for the call-by-name calculus) which ensures a stronger form
of safety, that is, that rebinding always succeeds. The key idea is to decorate types with the names of the
variables which need to be rebound, as done also by Nanevski and Pfenning [17]. In this way run-time
errors arising from absence (or mismatch) in rebind are prevented by a purely static type system, at the
price of quite sophisticated types. A similar system could be developed for the present calculus. Also the
type system of Dezani et al. [12, 13] could be enriched with intersection types to get the stronger safety
for the call-by-value calculus.
Intersection types have been originally introduced [6] as a language for describing and capturing
properties of λ -terms, which had escaped all previous typing disciplines. For instance, they were used
in order to give the first type theoretic characterisation of strongly normalising terms [20], and later in
order to capture (persistently) normalising terms [8].
Very early it was realised that intersection types had also a distinctive semantical flavour. Namely,
they expressed at a syntactical level the fact that a term belonged to suitable compact open sets in a
Scott domain [4]. Since then, intersection types have been used as a powerful tool both for the analysis
and the synthesis of λ -models. On the one hand, intersection type disciplines provide finitary inductive

56

Intersection types for unbind and rebind

definitions of interpretation of λ -terms in models [7], and they are suggestive for the shape the domain
model has to have in order to exhibit specific properties [10].
More recently, systems with both intersection and union types have been proposed for various aims
[3, 14], but we do not see any gain in adding union types in the present setting.
Ever since the accidental discovery of dynamic scoping in McCarthy’s Lisp 1.0, there has been
extensive work in explaining and integrating mechanisms for dynamic and static binding. The classical
reference for dynamic scoping is Moreau’s paper [16], which introduces a λ -calculus with two distinct
kinds of variables: static and dynamic. The semantics can be (equivalently) given either by translation
in the standard λ -calculus or directly. In the translation semantics, λ -abstractions have an additional
parameter corresponding to the application-time context. In the direct semantics, roughly, an application
(λ x.t) v, where x is a dynamic variable, reduces to a dynamic let dlet x = v in t. In this construct, free
occurrences of x in t are not immediately replaced by v, as in the standard static let, but rather reduction
of t is started. When, during this reduction, an occurrence of x is found in redex position, it is replaced
by the value of x in the innermost enclosing dlet, so that dynamic scoping is obtained.
In our calculus, the behaviour of the dynamic let is obtained by the unbind and rebind constructs.
However, there are at least two important differences. Firstly, the unbind construct allows the programmer to explicitly control the program portions where a variable should be dynamically bound. In particular, occurrences of the same variable can be bound either statically or dynamically, whereas Moreau [16]
assumes two distinct sets. Secondly, our rebind behaves in a hierarchical way, whereas, taking Moreau’s
approach [16] where the innermost binding is selected, a new rebind for the same variable would rewrite
the previous one, as also in work by Dezani et al. [11]. For instance, h x | x i[x 7→ 1][x 7→ 2] would reduce
to 2 rather than to 1. The advantage of our semantics, at the price of a more complicated type system, is
again more control. In other words, when the programmers want to use “open code”, they must explicitly specify the desired binding, whereas in Moreau’s paper [16] code containing dynamic variables is
automatically rebound with the binding which accidentally exists when it is used. This semantics, when
desired, can be recovered in our calculi by using rebinds of the shape t[x1 7→ x1 , . . . , xn 7→ xn ], where
x1 , . . . , xn are all the dynamic variables which occur in t.
Other calculi for dynamic binding and/or rebinding have been proposed [9, 15, 5]. We refer to our
previous papers introducing the calculus [12, 13] for a discussion and comparison.
As already mentioned, an interesting feature of our calculus is that elements of the same set can
play the double role of standard variables, which can be α -renamed, and names, which cannot be α renamed (if not globally in a program) [2, 17]. The crucial difference is that in the case of standard
variables the matching betweeen parameter and argument is done on a positional basis, as demonstrated
by the de Bruijn notation, whereas in the case of names it is done on a nominal basis. An analogous
difference holds between tuples and records, and between positional and name-based parameter passing
in languages, as recently discussed by Rytz and Odersky [21].
Distributed process calculi provide rebinding of names, see for instance the work of Sewell [22].
Moreover, rebinding for distributed calculi has been studied [1], where, however, the problem of integrating rebinding with standard computation is not addressed, so there is no interaction between static
and dynamic binding.
Finally, an important source of inspiration has been multi-stage programming as, e.g., in MetaML
[23], notably for the idea of allowing (open) code as a special value, the hierarchical nature of the
unbind/rebind mechanism and, correspondingly, of the type system. The type system of Taha and Sheard
[23] is more expressive than the present one, since both the turn-style and the types are decorated with
integers. A deeper comparison will be subject of further work.

Dezani, Giannini and Zucca

57

In order to model different behaviours according to the presence (and type concordance) of variables
in the rebinding environment, we plan to add a construct for conditional execution of rebind [11]. With
this construct we could model a variety of object models, paradigms and language features.
Future investigation will also deal with the general form of binding discussed by Tanter [24], which
subsumes both static and dynamic binding and also allows fine-grained bindings which can depend on
contexts and environments.
Acknowledgments. We warmly thank the anonymous referees for their useful comments. In particular, one referee warned us about the problem of avoiding variable capture when applying substitution
to an unbound term. We also thank Davide Ancona for pointing out the work by Rytz and Odersky [21]
and the analogy among the pairs variable/name, tuple/record, positional/nominal, any misinterpretation
is, of course, our responsibility.

References
[1] Davide Ancona, Sonia Fagorzi & Elena Zucca (2008): A Parametric Calculus for Mobile Open Code. In:
DCM’07. ENTCS 192(3), Elsevier, pp. 3–22, doi:10.1016/j.entcs.2008.10.024.
[2] Davide Ancona & Eugenio Moggi (2004): A Fresh Calculus for Name Management. In: GPCE’04. LNCS
3286, Springer, pp. 206–224, doi:10.1007/978-3-540-30175-2 11.
[3] Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ugo de’ Liguoro (1995): Intersection and Union
Types: Syntax and Semantics. Information and Computation 119, pp. 202–230, doi:10.1006/inco.1995.1086.
[4] Henk P. Barendregt, Mario Coppo & Maraingiola Dezani-Ciancaglini (1983): A filter lambda model and the
completeness of type assignment. The Journal of Symbolic Logic 48(4), pp. 931–940, doi:10.2307/2273659.
[5] Gavin Bierman, Michael W. Hicks, Peter Sewell, Gareth Stoyle & Keith Wansbrough (2003): Dynamic
Rebinding for Marshalling and Update, with Destruct-Time λ . In: ICFP’03. ACM Press, pp. 99–110,
doi:10.1145/944705.944715.
[6] Mario Coppo & Mariangiola Dezani-Ciancaglini (1980): An extension of the basic functionality theory for
the λ -calculus. Notre Dame Journal of Formal Logic 21(4), pp. 685–693, doi:10.1305/ndjfl/1093883253.
[7] Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell & Giuseppe Longo (1984): Extended
type structures and filter lambda models. In: Logic colloquium ’82. North-Holland, pp. 241–262,
doi:10.1016/S0049-237X(08)71819-6.
[8] Mario Coppo, Mariangiola Dezani-Ciancaglini & Maddalena Zacchi (1987):
Type theories,
Information and Computation 72(2), pp. 85–116,
normal forms, and D∞ -lambda-models.
doi:10.1016/0890-5401(87)90042-3.
[9] Laurent Dami (1997): A Lambda-Calculus for Dynamic Binding. Theoretical Computer Science 192(2), pp.
201–231, doi:10.1016/S0304-3975(97)00150-3.
[10] Mariangiola Dezani-Ciancaglini, Silvia Ghilezan & Silvia Likavec (2004): Behavioural Inverse Limit
lambda-models. Theoretical Computer Science 316(1–3), pp. 49–74, doi:10.1016/j.tcs.2004.01.023.
[11] Mariangiola Dezani-Ciancaglini, Paola Giannini & Oscar Nierstrasz (2008): A Calculus of Evolving Objects.
Scientific Annals of Computer Science 18, pp. 63–98.
[12] Mariangiola Dezani-Ciancaglini, Paola Giannini & Elena Zucca (2009): The essence of static and dynamic
bindings. In: ICTCS’09.
http://www.disi.unige.it/person/ZuccaE/Research/papers/ICTCS09-DGZ.pdf.
[13] Mariangiola Dezani-Ciancaglini, Paola Giannini & Elena Zucca (2010):
Extending lambdacalculus with unbind and rebind. RAIRO - Theoretical Informatics and Applications To appear.
http://www.disi.unige.it/person/ZuccaE/Research/papers/ITA10.pdf.

58

Intersection types for unbind and rebind

[14] Alain Frisch, Giuseppe Castagna & Veronique Benzaken (2008): Semantic Subtyping: dealing settheoretically with function, union, intersection, and negation types. Journal of the ACM 55(4), pp. 1–64,
doi:10.1145/1391289.1391293. Extends and supersedes LICS’02 and ICALP/PPDP’05 articles.
[15] Oleg Kiselyov, Chung-chieh Shan & Amr Sabry (2006): Delimited dynamic binding. In: ICFP’06. ACM
Press, pp. 26–37, doi:10.1145/1159803.1159808.
[16] Luc Moreau (1998): A Syntactic Theory of Dynamic Binding. Higher Order and Symbolic Computation
11(3), pp. 233–279, doi:10.1023/A:1010087314987.
[17] Aleksandar Nanevski & Frank Pfenning (2005): Staged computation with names and necessity. Journal of
Functional Programming 15(5), pp. 893–939, doi:10.1017/S095679680500568X.
[18] Benjamin C. Pierce (2002): Types and Programming Languages. MIT Press.
[19] Gordon Plotkin (1977): LCF considered as a programming language. Theoretical Computer Science 5, pp.
225–255, doi:10.1016/0304-3975(77)90044-5.
[20] Garrel Pottinger (1980): A type assignment for the strongly normalizable λ -terms. In: To H. B. Curry: essays
on combinatory logic, lambda calculus and formalism. Academic Press, pp. 561–577.
[21] Lukas Rytz & Martin Odersky (2010): Named and default arguments for polymorphic object-oriented languages. In: OOPS’10. ACM Press, pp. 2090–2095, doi:10.1145/1774088.1774529.
[22] Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre
Habouzit & Viktor Vafeiadis (2007): Acute: High-level programming language design for distributed computation: Design rationale and language definition. Journal of Functional Programming 17(4-5), pp. 547–612,
doi:10.1017/S0956796807006442.
[23] Walid Taha & Tim Sheard (2000): MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science 248(1-2), pp. 211–242, doi:10.1016/S0304-3975(00)00053-0.
[24] Èric Tanter (2009): Beyond Static and Dynamic Scope. In: Dynamic Languages Symposium’09. ACM Press,
pp. 3–14, doi:10.1145/1640134.1640137.
[25] Betti Venneri (1994): Intersection Types as Logical Formulae. Journal of Logic and Computation 4(2), pp.
109–124, doi:10.1093/logcom/4.2.109.

