1–LABEL:LastPageApr. 29, 2016Feb. 27, 2018

This article is based on the submission to the 13th International Conference
on Typed Lambda Calculi and Applications, TLCA 2015

# Mixin Composition Synthesis based on Intersection Types

Jan Bessaia  aTechnical University of Dortmund, Dortmund, Germany
<EMAIL_ADDRESS><EMAIL_ADDRESS>boris.duedder@tu-
dortmund.de<EMAIL_ADDRESS>,  Tzu-Chun Chenb  bTechnical
University of Darmstadt, Darmstadt, Germany<EMAIL_ADDRESS>darmstadt.de ,  Andrej Dudenhefnera  ,  Boris Düddera  ,  Ugo de’Liguoroc
cUniversity of Torino, Torino, Italy<EMAIL_ADDRESS>and  Jakob Rehofa

###### Abstract.

We present a method for synthesizing compositions of mixins using type
inhabitation in intersection types. First, recursively defined classes and
mixins, which are functions over classes, are expressed as terms in a lambda
calculus with records. Intersection types with records and record-merge are
used to assign meaningful types to these terms without resorting to recursive
types. Second, typed terms are translated to a repository of typed
combinators. We show a relation between record types with record-merge and
intersection types with constructors. This relation is used to prove soundness
and partial completeness of the translation with respect to mixin composition
synthesis. Furthermore, we demonstrate how a translated repository and goal
type can be used as input to an existing framework for composition synthesis
in bounded combinatory logic via type inhabitation. The computed result is a
class typed by the goal type and generated by a mixin composition applied to
an existing class.

###### Key words and phrases:

Record Calculus, Combinatory Logic, Type Inhabitation, Mixin, Intersection
Type

###### 1991 Mathematics Subject Classification:

F.4.1 Mathematical Logic – $\lambda$ Calculus and Related Systems

This work was partially supported by EU COST Action IC1201: BETTY and MIUR
PRIN CINA Prot. 2010LHT4KM, San Paolo Project SALT. Tzu-chun Chen is also
partially supported by the ERC grant FP7-617805 _LiVeSoft – Lightweight
Verification of Software_.

##  1\. Introduction

Starting with Cardelli’s pioneering work [Car84], various typed
$\lambda$-calculi extended with records have been thoroughly studied to model
sophisticated features of object-oriented programming languages, like
recursive objects and classes, object extension, method overriding and
inheritance (see e.g. [AC96, Bru02, KL05]).

Here, we focus on the synthesis of mixin application chains. In the object-
oriented paradigm, mixins [Moo86, Can79] have been introduced as an
alternative construct for code reuse that improves over the limitations of
multiple inheritance, e.g. connecting incompatible base classes and semantic
ambiguities caused by the diamond problem [HTT87]. Together with abstract
classes and traits, mixins (functions over classes) can be considered as an
advanced construct to obtain flexible implementations of module libraries and
to enhance code reusability; many popular programming languages miss native
support for mixins, but they are an object of intensive study and research
(e.g. [BPS99, OZ05]). In this setting we aim at synthesizing classes from a
library of mixins. Our particular modeling approach is inspired by modern
language features (e.g. ECMAScript “bind”) to preserve contexts in order to
prevent programming errors [Ecm11].

We formalize synthesis of classes from a library of mixins as an instance of
the relativized type inhabitation problem in combinatory logic. Relativized
type inhabitation is the following decision problem: given a combinatory type
context $\Delta$ and a type $\tau$ does there exist an applicative term $e$
such that $e$ has type $\tau$ under the type assumptions in $\Delta$? We
implicitly include the problem of constructing such a term as the synthesized
result.

Although relativized type inhabitation is undecidable even in simple types, it
is decidable in $k$-bounded combinatory logic $\textsf{BCL}_{k}(\to,\cap)$
[DMRU12]. $\textsf{BCL}_{k}(\to,\cap)$ is the combinatory logic typed with
arrow and intersection types, where $k$ bounds the depth of types wrt. $\to$
used to instantiate schematic combinator types. Hence, an algorithm for semi-
deciding type inhabitation for
$\mbox{$\textsf{BCL}(\to,\cap)$}=\bigcup_{k}\mbox{$\textsf{BCL}_{k}(\to,\cap)$}$
can be obtained by iterative deepening over $k$ and solving the corresponding
decision problem in $\textsf{BCL}_{k}(\to,\cap)$ [DMRU12]. In the present
paper, we enable combinatory synthesis of classes via intersection typed mixin
combinators. Intersection types [BCDC83] play an important rôle in combinatory
synthesis, because they allow for semantic specification of components and
synthesis goals [DMRU12, BDDM14]. They also allow a natural way to type
records.

Now, looking at
$\\{C_{1}:\sigma_{1},\ldots,C_{p}:\sigma_{p},M_{1}:\tau_{1},\ldots,M_{q}:\tau_{q}\\}\subseteq\Delta$
as the abstract specification of a library including classes $C_{i}$ and
mixins $M_{j}$ with interfaces $\sigma_{i}$ and $\tau_{j}$ respectively, and
given a type $\tau$ specifying a desired class, we may identify the class
synthesis problem with the relativized type inhabitation problem of
constructing a term $e$, i.e. an applicative composition of classes and
mixins, typed by $\tau$ in $\Delta$. To make this feasible, we have to bridge
the gap between the expressivity of highly sophisticated type systems used for
typing classes and mixins, for instance $F$-bounded polymorphism used in
[CCH+89, CHC90], and the system of intersection types from [BCDC83]. In doing
so, we move from the system originally presented in [Lig01], consisting of a
type assignment system of intersection and record types, to a
$\lambda$-calculus which we enrich here with record merge operation (called
“with” in [CHC90]), to allow for expressive mixin combinators. The type system
is modified by reconstructing record types ${\langle l_{i}:\sigma_{i}\mid i\in
I\rangle}$ as intersection of unary record types ${\langle
l_{i}:\sigma_{i}\rangle}$, and considering a subtype relation extending the
one in [BCDC83]. This is however not enough for typing record merge, for which
we consider a type-merge operator $+$. The problem of typing extensible
records and merge, faced for the first time in [Wan91, Rém92], is notoriously
hard; to circumvent difficulties the theory of record subtyping in [CHC90]
(where a similar type-merge operator is considered) allows just for “exact”
record typing, which involves subtyping in depth, but not in width. Such a
restriction, that has limited effects wrt. a rich and expressive type system
like $F$-bounded polymorphism, would be too severe in our setting. Therefore,
we undertake a study of the type algebra of record types with intersection and
type-merge, leading to a type assignment system where exact record typing is
required only for the right-hand side operand of the term merge operator,
which is enough to ensure soundness of typing.

The next challenge is to show that in our system we can type classes and
mixins in a meaningful way. Classes are essentially recursive records. Mixins
are made of a combination of fixed point combinators and record merge. Such
combinators, which usually require recursive types, can be typed in our system
by means of an iterative method exploiting the ability of intersection types
to represent approximations of the potentially infinite unfolding of recursive
definitions.

The final problem we face is the encoding of intersection types with record
types and type-merge into the language of $\textsf{BCL}_{k}(\to,\cap)$. For
this purpose, we consider a conservative extension of bounded combinatory
logic, called $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$, where we allow
unary type constructors that are monotonic and distribute over intersection.
We show that the (semi) algorithm solving inhabitation for
$\textsf{BCL}_{k}(\to,\cap)$ can be adapted to
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$, by proving that the key
properties necessary to solve the inhabitation problem in
$\textsf{BCL}_{k}(\to,\cap)$ are preserved in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ and showing how the type-merge
operator can be simulated in $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$. In
fact, type-merge is not monotonic in its second argument, due to the lack of
negative information caused by the combination of $+$ and $\cap$. Our work
culminates in two theorems that ensure soundness and completeness of the so
obtained method wrt. synthesis of classes by mixin application.

###  1.1. Contributions

The contributions of this article can be summarized as follows:

  * •

A type system with intersection types and records
($\mathbb{T}_{{\langle\rangle}}$) for a $\lambda$-calculus with records
($\Lambda_{R}$) is designed and its key properties are proven.

  * •

$\mathbb{T}_{{\langle\rangle}}$ is used as a typed calculus for classes and
mixins.

  * •

Bounded combinatory logic and a decision algorithm for relativized type
inhabitation are extended with constructors
($\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$) retaining complexity results.

  * •

A sound and (partially) complete encoding of mixins and classes in
$\mathbb{T}_{{\langle\rangle}}$ as combinators in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ for synthesis is proven and
exemplified.

  * •

Negative information, i.e. the information on which labels are absent, is
encoded with polynomial overhead.

###  1.2. Organization

The article is organized as follows: Section 2 discusses the development of
traits and mixins as well as program synthesis. In Section 3, intersection and
record types for a $\lambda$-calculus with records are introduced as a domain
specific language for representing mixins and classes. Section 4 adapts
bounded combinatory logic to include constructors
($\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$) as a foundation for mixin
synthesis. Section 5 presents the encoding of record types in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$, mixin composition synthesis by
type inhabitation and provides detailed examples including the use of semantic
types. A conclusion in Section 6 hints at future work.

##  2\. Related Work

This work evolves from the contributions [BDDM14, LC14, BDD+15a] to the
workshop ITRS’14 and the original submission to TLCA15 [BDD+15b]. It combines
two research areas, type systems for traits and mixins and program synthesis
using type inhabitation.

###  2.1. Type Systems for Traits and Mixins

The concept of mixins goes back to research on Lisp dialects in the late 70’s
and early 80’s [Can79, WM80, Moo86]. The motivation was to extend code
organization in object-oriented languages, which was traditionally defined by
hierarchical inheritance. To this end Cannon introduced base flavors serving
as a starting point later to be extended by mixin flavors [Can79]. Mixin
flavors implement particular features and can only be instantiated by
application to existing flavors. They can define requirements to be met prior
to application. If they use internal state, this state cannot be shared with
other flavors.

Type theories for objects and classes were developed shortly after. Languages
like Simula [DN66] and Smalltalk-80 [DS84] are object-oriented typed
languages, but their type system is geared toward memory management rather
than safe reuse. Various techniques have been deployed to enable type safe
reuse of implementations. Cardelli’s seminal paper “A Semantics of Multiple
Inheritance” [Car84] filled this gap. Type inference for products with
subtyping was shown to be decidable in [Mit84]. Cardelli improved upon the
cumbersome encoding of entities using records with named projections instead
of products. Subtyping addresses permutation of record entries as well as
multiple inheritance. It ensures compatibility of horizontally extended and
vertically specialized records.

A series of later developments dealt with issues introduced by recursion and
obtained type inference. To this end Wand designed an ML-inspired system
[Wan87] that later inspired the development of System $F_{\leq}$ [CCH+89]. A
fine grained analysis of the connection between inheritance and subtyping was
now possible [CHC90] and came to the surprising negative conclusion, that
“inheritance is not subtyping”. This analysis by Cook, Hill and Canning is
also the first to discuss the difference between early and late binding of the
recursion inherently present in objects: delegating recursion to methods using
a self parameter (late binding) as done previously by Mitchell [Mit90] unifies
classes and objects, whereas early fixpoint computation at the class level is
open for later modifications by inheritance and mixins. Subsequently, Bracha
and Cook reinterpreted mixins in the light of classes and inheritance, where
they can act as abstract subclasses [BC90]. Their main contribution was to
shed light on the abstract operation of mixin application in contrast to prior
work, which focused on implementation details like class hierarchy
linearization. This operation turns out to be powerful enough to encode
(multiple) inheritance. From there on, development took two main routes. One
direction was the development of advanced object calculi, which is covered in
great detail in [AC96]. The other direction was to model the type systems of
mainstream programming languages. Featherweight Java by Igarashi, Pierce and
Wadler is a prominent example [IPW01] for the latter direction. It inspired a
mixin based treatment of virtual classes in [EOC06]. A parallel development
focused on traits, which are a restriction of mixins to subtype compatible
overwriting [LS08, LSZ12]. Bono et al. suggested a formal type system for a
calculus with traits [BDG07, BDG08]. The most recent studies follow this trend
to bring together the two directions. Java has been partially formalized by
Rowe and van Bakel [BR13, RB14], and completely in K-Java [BR15]. Recently,
the Scala compiler is being reworked to match DOT [AMO12, ARO14, AGO+16], a
formal dependently typed core specification.

###  2.2. Synthesis by Type Inhabitation

Synthesis is by now a vast area of computer science, and we can only attempt
here to place our approach broadly in relation to major points of comparison.

The synthesis problem can be traced back to Alonzo Church [Chu57, Tho09]. It
was first considered for the problem of automatically constructing a finite-
state procedure implementing a given input/output relation over infinite
bitstreams specified as a logical formula. The automata-theoretic approach was
notably advanced by Pnueli and Rosner in the context of linear temporal logic
(LTL) [PR89] and by many others since then. Another major branch of work in
synthesis is deductive synthesis, as studied by Manna and Waldinger, who rely
on proof systems for program properties [MW80], with many more works following
in this tradition.

The presented approach to the synthesis problem is proof-theoretic and can
best be characterized more specifically as type-based and component-oriented.
This approach was initiated by Rehof et al. [RU11, DMRU12, Reh13] around the
idea of using the inhabitation problem in bounded combinatory logics with
intersection types [BCDC83] as a foundation for synthesis. In contrast to
standard combinatory logic [HS08, DCH92] invented by Schönfinkel in 1924
[Sch24], $k$-bounded combinatory logic $\textsf{BCL}_{k}(\to,\cap)$ [DMRU12]
introduces a bound $k$ on the level of types, i.e. depth wrt. $\to$, used to
instantiate schematic combinator types. Additionally, rather than considering
a fixed base of combinators (for example, the base $\mathbf{S},\mathbf{K}$),
the inhabitation problem is relativized to an arbitrary set $\Delta$ of typed
combinators, given as part of the input to the relativized inhabitation
problem:

Given $\Delta$ and $\tau$, is there an applicative term $e$ such that
$\Delta\vdash_{\textsf{BCL}_{k}(\to,\cap)}e:\tau$?

In many instances the inhabitation problem with a fixed-base is much easier
than in the relativized case, where the base is part of the input. For
example, Pspace-completeness of inhabitation in the simple-typed
$\lambda$-calculus [Sta79] implies Pspace-completeness of the equivalent
simple-typed $\mathbf{S}\mathbf{K}$-calculus. The related problem of term
enumeration for simple-typed $\lambda$-calculus has been studied by Ben-Yelles
[BY79] and, more recently, by Hindley [Hin08].

Linial and Post [LP49] initiated the study of decision problems for arbitrary
propositional axiom systems (partial propositional calculi, abbreviated PPC),
in reaction to a question posed by Tarski in 1946. In the Linial-Post theorem
they show existence of a PPC with an unsolvable decision problem. Later,
Singletary showed that every recursively enumerable many-one degree can be
represented by the implicational fragment of PPC [Sin74]. This implies that
the relativized inhabitation problem is undecidable for combinatory logic with
schematism even in simple types. Recent developments [Bok15] show that it is
undecidable, whether a given finite set of propositional formulas constitutes
an adequate axiom system for a fixed intuitionistic implicational
propositional calculus.

In contrast, the main result of [DMRU12] is that the relativized inhabitation
problems for $\textsf{BCL}_{k}(\to,\cap)$ with intersection types form an
infinite hierarchy, being $(k+2)$-Exptime-complete for each fixed bound $k$.

In [Reh13], unbounded relativized inhabitation is seen, already at the level
of simple types, to constitute a Turing-complete logic programming language
for program composition, in a way that is related to work on proof-theoretic
generalizations of logic programming languages [MNPS91].

Perhaps surprisingly, component-oriented synthesis is a relatively recent
development. The approach of combinatory logic synthesis is basically
motivated by the idea that type structure provides a natural and code-oriented
vehicle for synthesis specifications together with the idea that combinatory
logic provides a natural type-theoretic model of components, component
interfaces, and component composition. Vardi and Lustig initiated the
component-oriented approach within the automata-theoretic tradition,
explicitly developing the idea of synthesizing systems from preexisting
components [LV09] with the idea of leveraging design intelligence and
efficiency from components as building blocks for synthesis. A recent Dagstuhl
meeting explored these ideas of design and synthesis from components across
different communities [RV14].

Realizing the component-based idea within type-based synthesis requires ways
to deal with semantic specification as well as the combinatorial explosion of
search spaces inherent in synthesis problems. Rehof et al. [RU12] introduced
the idea of using intersection types [BCDC83] to type-based synthesis as a
means of addressing the problem of search control and semantic specification
at the type level. We refer to types enriched with semantic specifications
through intersection types as semantic types. In addition to semantic types,
Rehof et al. have introduced the idea of staging into synthesis via modal
types [DMR14]. Simple types were used by Steffen et al. [SMvdB97] in the
context of temporal logic synthesis to semantically enrich temporal
specifications with taxonomic information.

The notion of composition synthesis using semantic types is related to
adaptation synthesis via proof counting [HHSW02, WY05]. In particular, in
[HHSW02] typed predicate logic is used for semantic specification at the
interface level. We follow this idea, however the type system, underlying
logic and algorithmic methods are different.

Refinement types [FP91] externally relate specifications to implementation
types. The refinement type scheme structurally constraints how refinement
types are formed: this prevents semantic specifications like
$(\text{Int}\to\text{Int})\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Injective}}$,
which are possible in our system. Recently, refinement types have been used
for example guided synthesis in [FOWZ16]. Types have also been used in order
to synthesize code completions [GKKP13]. Intersection types are not only
useful for semantic specification, but also to encode objects. To this end
they can be combined with records as proposed in [Pie91]. Their relation to
object-oriented inheritance has been studied in [CP96] and serves as an
inspiration for our work.

Combinatory logic synthesis has been implemented in a framework, Combinatory
Logic Synthesizer (CL)S, which is still being further developed [BDD+14].

##  3\. Intersection Types for Mixins and Classes

###  3.1. Intersection and record types

We consider a type-free $\lambda$-calculus of extensible records, equipped
with a merge operator. The term syntax is defined by the following grammar:

$\begin{array}[]{rlll}\Lambda_{R}\ni M,N,M_{i}&::=&x\mid(\lambda
x.M)\mid(MN)\mid(M.l)\mid R\mid(M\oplus R)&\text{terms}\\\\[2.84526pt]
R&::=&{\langle l_{i}=M_{i}\mid i\in I\rangle}&\text{records}\end{array}$

where $x\in\mbox{\bf Var}$ and $l\in\mbox{\bf Label}$ range over denumerably
many term variables and labels respectively, and the sets of indexes $I$ are
finite. Free and bound variables are defined as for the ordinary
$\lambda$-calculus, and we name $\Lambda_{R}^{0}$ the set of all closed terms
in $\Lambda_{R}$; terms are identified up to renaming of bound variables and
$M\\{N/x\\}$ denotes capture avoiding substitution of $N$ for $x$ in $M$. We
adopt notational conventions from [Bar84]; in particular, application
associates to the left and external parentheses are omitted when unnecessary;
also the dot notation for record selection takes precedence over $\lambda$, so
that $\lambda x.\;M.l$ reads as $\lambda x.(M.l)$. If not stated otherwise
$\,\oplus\,$ also associates to the left, and we avoid external parentheses
when unnecessary.

Terms $R\equiv{\langle l_{i}=M_{i}\ |\ i\in I\rangle}$ (writing $\equiv$ for
syntactic identity) represent records, with fields $l_{i}$ and $M_{i}$ as the
respective values; we set $\mbox{\it lbl}({\langle l_{i}=M_{i}\mid i\in
I\rangle})=\\{l_{i}\mid i\in I\\}$. For records we adopt the usual notation to
combine sets, i.e. $\\{l_{i},l_{j}\mid i\in I,j\in J\\}=\\{l_{i}\mid i\in
I\cup J\\}$. The term $M.l$ is field selection and $M\oplus R$ is record
merge. In particular, if $R_{1}$ and $R_{2}$ are records then
$R_{1}\,\oplus\,R_{2}$ is the record having as fields the union of the fields
of $R_{1}$ and $R_{2}$ and as values those of the original records but in case
of ambiguity, where the values in $R_{2}$ prevail. The syntactic constraint
that $R$ is a record in $M\oplus R$ is justified after Definition 6. Note that
a variable $x$ is not a record, hence $\lambda x.x\,\oplus\,R$ is well-formed
for any record $R$ while $\lambda x.R\,\oplus\,x$ is not.

The actual meaning of these operations is formalized by the following
reduction relation:

[$\Lambda_{R}$ reduction] Reduction
$\longrightarrow\,\subseteq\Lambda_{R}^{2}$ is the least compatible relation
such that:

$\begin{array}[]{lrcl}(\beta)&\ (\lambda
x.M)N&\longrightarrow&M\\{N/x\\}\\\\[2.84526pt] (\mbox{\it sel})&\langle
l_{i}=M_{i}\mid i\in I\rangle.l_{j}&\longrightarrow&M_{j}\hskip
113.81102pt\mbox{if $j\in I$}\\\\[2.84526pt] (\mbox{\it$\oplus$})&\langle
l_{i}=M_{i}\mid i\in I\rangle\,\oplus\,\langle l_{j}=N_{j}\mid\ j\in
J\rangle&\longrightarrow&\langle l_{i}=M_{i},\ l_{j}=N_{j}\mid i\in I\setminus
J,\ j\in J\rangle\end{array}$

Record merge subsumes field update as considered in [Lig01]: $(M.l:=N)$ is
exactly $(M\,\oplus\,{\langle l=N\rangle})$, but merge is not uniformly
definable in terms of update as long as labels are not expressions in the
calculus, therefore we take merge as primitive operator. The reduction
relation $\longrightarrow$ is Church-Rosser namely its transitive closure
$\longrightarrow^{*}$ is confluent.

######  Theorem 1 (Church-Rosser property).

For all $M$ if $M\longrightarrow^{*}M_{1}$ and $M\longrightarrow^{*}M_{2}$
then there is $M_{3}$ such that $M_{1}\longrightarrow^{*}M_{3}$ and
$M_{2}\longrightarrow^{*}M_{3}$.

######  Proof 3.1.

By adapting Tait and Martin-Löf’s proof of Church-Rosser property of
$\beta$-reduction of $\lambda$-calculus, which is based on the so called
$1$-reduction $\twoheadrightarrow_{1}$. To the clauses for ordinary
$\lambda$-calculus (see e.g. [Bar84] Definition 3.2.3) we add:

  1. i)

$\forall i\in I.\ M_{i}\twoheadrightarrow_{1}M^{\prime}_{i}\Rightarrow{\langle
l_{i}=M_{i}\mid i\in I\rangle}\twoheadrightarrow_{1}{\langle
l_{i}=M^{\prime}_{i}\mid i\in I\rangle}$

  2. ii)

$M\twoheadrightarrow_{1}M^{\prime}\Rightarrow
M.l\twoheadrightarrow_{1}M^{\prime}.l$

  3. iii)

$M\twoheadrightarrow_{1}M^{\prime}\And
R\twoheadrightarrow_{1}R^{\prime}\Rightarrow
M\,\oplus\,R\twoheadrightarrow_{1}M^{\prime}\,\oplus\,R^{\prime}$

  4. iv)

$\forall i\in I.\ M_{i}\twoheadrightarrow_{1}M^{\prime}_{i}\And j\in
I\Rightarrow{\langle l_{i}=M_{i}\mid i\in
I\rangle}.l_{j}\twoheadrightarrow_{1}M^{\prime}_{j}$

  5. v)

$\forall i\in I.\ M_{i}\twoheadrightarrow_{1}M^{\prime}_{i}\And\forall j\in
J.\ N_{j}\twoheadrightarrow_{1}N^{\prime}_{j}\Rightarrow$
$\langle l_{i}=M_{i}\mid i\in I\rangle\,\oplus\,\langle l_{j}=N_{j}\mid\ j\in
J\rangle\twoheadrightarrow_{1}\langle l_{i}=M^{\prime}_{i},\
l_{j}=N^{\prime}_{j}\mid i\in I\setminus J,\ j\in J\rangle$

Now it is easy to check that $\twoheadrightarrow_{1}^{*}\ =\
\longrightarrow^{*}$ so that by Lemma 3.2.2 of [Bar84] it suffices to show
that $\twoheadrightarrow_{1}$ satisfies the diamond property:

$M\twoheadrightarrow_{1}M_{1}\And
M\twoheadrightarrow_{1}M_{2}\Rightarrow\exists M_{3}.\
M_{1}\twoheadrightarrow_{1}M_{3}\And M_{2}\twoheadrightarrow_{1}M_{3}.$

The latter is easily established by induction over the definition of
$M\twoheadrightarrow_{1}M_{1}$ and by cases of $M\twoheadrightarrow_{1}M_{2}$.

In the spirit of Curry’s assignment of polymorphic types and of intersection
types in particular, types are introduced as a syntactical tool to capture
semantic properties of terms, rather than as constraints to term formation.

[Intersection types for $\Lambda_{R}$]

$\begin{array}[]{rlll}\mathbb{T}\ni\sigma,\sigma_{i}&::=&a\mid\omega\mid\sigma_{1}\to\sigma_{2}\mid\sigma_{1}\cap\sigma_{2}\mid\rho&\text{types}\\\\[2.84526pt]
\mathbb{T}_{{\langle\rangle}}\ni\rho,\rho_{i}&::=&{\langle\rangle}\mid{\langle
l:\sigma\rangle}\mid\rho_{1}+\rho_{2}\mid\rho_{1}\cap\rho_{2}&\text{record
types}\end{array}$

where $a$ ranges over type constants and $l$ ranges over the denumerable set
Label. We use $\sigma,\tau$, possibly with sub and superscripts, for types in
$\mathbb{T}$ and $\rho,\rho_{i}$, possibly with superscripts, for record types
in $\mathbb{T}_{{\langle\rangle}}$ only. Note that $\to$ associates to the
right, and $\cap$ binds stronger than $\to$. As with intersection type systems
for the $\lambda$-calculus, the intended meaning of types are sets, provided a
set theoretic interpretation of type constants $a$.

Following [BCDC83], type semantics is given axiomatically by means of the
subtyping relation $\leq$, that can be interpreted as subset inclusion: see
e.g. [Mit96] §10.4 for extending such interpretation to record types. It is
the least pre-order over $\mathbb{T}$ satisfying Definition 3.1 and Definition
3.1.

[Type inclusion: arrow and intersection types]

  1. (1)

$\sigma\leq\omega$ and $\omega\leq\omega\to\omega$

  2. (2)

$\sigma\cap\tau\leq\sigma$ and $\sigma\cap\tau\leq\tau$

  3. (3)

$\sigma\leq\tau_{1}\And\sigma\leq\tau_{2}\Rightarrow\sigma\leq\tau_{1}\cap\tau_{2}$

  4. (4)

$(\sigma\to\tau_{1})\cap(\sigma\to\tau_{2})\leq\sigma\to\tau_{1}\cap\tau_{2}$

  5. (5)

$\sigma_{2}\leq\sigma_{1}\And\tau_{1}\leq\tau_{2}\Rightarrow\sigma_{1}\to\tau_{1}\leq\sigma_{2}\to\tau_{2}$

By 3.1.2 type $\omega$ is the top w.r.t. $\leq$; by 3.1.2 and 3.1.3
$\sigma\cap\tau$ is the meet. Writing $\sigma=\tau$ if $\sigma\leq\tau$ and
$\tau\leq\sigma$, from 3.1.1 and 3.1.5 we have
$\omega\leq\omega\to\omega\leq\sigma\to\omega\leq\omega$, which are all
equalities. Finally from 3.1.4 and 3.1.5 we also have
$(\sigma\to\tau_{1})\cap(\sigma\to\tau_{2})=\sigma\to\tau_{1}\cap\tau_{2}$.

If $\sigma_{1}\leq\tau_{1}$ and $\sigma_{2}\leq\tau_{2}$ then by transitivity
we have $\sigma_{1}\cap\sigma_{2}\leq\sigma_{1}\leq\tau_{1}$ and
$\sigma_{1}\cap\sigma_{2}\leq\sigma_{2}\leq\tau_{2}$ from which
$\sigma_{1}\cap\sigma_{2}\leq\tau_{1}\cap\tau_{2}$ follows by 3.1.3. Hence
$\leq$ is a precongruence w.r.t. $\cap$, and hence $=$ is a congruence.

[Type inclusion: record types]

  1. (1)

${\langle l:\sigma\rangle}\leq{\langle\rangle}$

  2. (2)

$\langle l:\sigma\rangle\cap\langle l:\tau\rangle\leq\langle
l:\sigma\cap\tau\rangle$

  3. (3)

$\sigma\leq\tau\Rightarrow\langle l:\sigma\rangle\leq\langle l:\tau\rangle$

  4. (4)

$\rho+{\langle\rangle}={\langle\rangle}+\rho=\rho$

  5. (5)

$(\rho_{1}+\rho_{2})+\rho_{3}=\rho_{1}+(\rho_{2}+\rho_{3})$

  6. (6)

$(\rho_{1}\cap\rho_{2})+\rho_{3}=(\rho_{1}+\rho_{3})\cap(\rho_{2}+\rho_{3})$

  7. (7)

$\langle l:\sigma\rangle+(\langle l:\tau\rangle\cap\rho)=\langle
l:\tau\rangle\cap\rho$

  8. (8)

$\langle l:\sigma\rangle+(\langle l^{\prime}:\tau\rangle\cap\rho)=\langle
l^{\prime}:\tau\rangle\cap(\langle l:\sigma\rangle+\rho)$ if $l\neq
l^{\prime}$

  9. (9)

$\rho_{1}\leq\rho_{2}\Rightarrow\rho_{1}+\rho\leq\rho_{2}+\rho$

  10. (10)

$\rho_{1}=\rho_{2}\Rightarrow\rho+\rho_{1}=\rho+\rho_{2}$

While Definition 3.1 is standard after [BCDC83], comments on Definition 3.1
are in order. First observe that from ${\langle
l:\sigma\rangle}\leq{\langle\rangle}$ we obtain that ${\langle
l:\sigma\rangle}\cap{\langle\rangle}={\langle l:\sigma\rangle}$, so that by
putting $\rho={\langle\rangle}$ in 3.1.7 and in 3.1.8 we obtain by 3.1.10:

$\langle l:\sigma\rangle+\langle l:\tau\rangle=\langle
l:\tau\rangle,\quad\quad\langle l:\sigma\rangle+\langle
l^{\prime}:\tau\rangle=\langle l:\sigma\rangle\cap\langle
l^{\prime}:\tau\rangle\qquad(l\neq l^{\prime}).$ (1)

Type ${\langle\rangle}$ is the type of all records. Type $\langle
l:\sigma\rangle$ is a unary record type, whose meaning is the set of records
having at least a field labeled by $l$, with value of type $\sigma$; therefore
${\langle l:\sigma\rangle}\cap{\langle l:\tau\rangle}$ is the type of records
having label $l$ with values both of type $\sigma$ and $\tau$, that is of type
$\sigma\cap\tau$. In fact the following equation is derivable:

${\langle l:\sigma\rangle}\cap{\langle l:\tau\rangle}=\langle
l:\sigma\cap\tau\rangle.$ (2)

On the other hand ${\langle l:\sigma\rangle}\cap{\langle
l^{\prime}:\tau\rangle}$, with $l\neq l^{\prime}$, is the type of records
having fields labeled by $l$ and $l^{\prime}$, with values of type $\sigma$
and $\tau$ respectively. It follows that intersection of record types can be
used to express properties of records with arbitrary (though finitely) many
fields, which justifies the abbreviations $\langle l_{i}:\sigma_{i}\mid i\in
I\neq\emptyset\rangle=\bigcap_{i\in I}\langle l_{i}:\sigma_{i}\rangle$ and
$\langle l_{i}:\sigma_{i}\mid i\in\emptyset\rangle={\langle\rangle}$, where we
assume that the $l_{i}$ are pairwise distinct. Finally, as it will be apparent
from Definition 6 below, $\rho_{1}+\rho_{2}$ is the type of all records
obtained by merging a record of type $\rho_{1}$ with a record of type
$\rho_{2}$, which is intended to type $\,\oplus\,$ that is at the same time a
record extension and field updating operation. Since this is the distinctive
feature of the system introduced here, we comment on this by means of a few
lemmas, illustrating its properties.

######  Lemma 2.

  1. (1)

$\langle l_{j_{0}}:\sigma\rangle+\langle l_{j}:\tau_{j}\mid j\in
J\rangle=\langle l_{j}:\tau_{j}\mid j\in J\rangle$ if $j_{0}\in J$,

  2. (2)

$\langle l_{j_{0}}:\sigma\rangle+\langle l_{j}:\tau_{j}\mid j\in
J\rangle=\langle l_{j_{0}}:\sigma\rangle\cap\langle l_{j}:\tau_{j}\mid j\in
J\rangle$ if $j_{0}\not\in J$

######  Proof 3.2.

  1. (1)

By commutativity and associativity of the meet operator $\cap$ and by 3.1.10,
when $j_{0}\in J$ we may freely assume that

$\langle l_{j_{0}}:\sigma\rangle+\langle l_{j}:\tau_{j}\mid j\in
J\rangle=\langle l_{j_{0}}:\sigma\rangle+(\langle
l_{j_{0}}:\tau_{j_{0}}\rangle\cap\langle l_{j}:\tau_{j}\mid j\in
J\setminus\\{j_{0}\\}\rangle)$

which is equal to $\langle l_{j_{0}}:\tau_{j_{0}}\rangle\cap\langle
l_{j}:\tau_{j}\mid j\in J\setminus\\{j_{0}\\}\rangle$ by 3.1.7, namely to
$\langle l_{j}:\tau_{j}\mid j\in J\rangle$.

  2. (2)

By induction over the cardinality of $J$. If it is $0$ then $\langle
l_{j}:\tau_{j}\mid j\in\emptyset\rangle={\langle\rangle}$ and:

$\langle l_{j_{0}}:\sigma\rangle+{\langle\rangle}=\langle
l_{j_{0}}:\sigma\rangle=\langle l_{j_{0}}:\sigma\rangle\cap{\langle\rangle}$

using 3.1.4, 3.1.1 and the fact that $\cap$ is the meet. If $|J|>0$ then, by
reasoning as before we have:

$\langle l_{j_{0}}:\sigma\rangle+\langle l_{j}:\tau_{j}\mid j\in
J\rangle=\langle l_{j_{0}}:\sigma\rangle+(\langle
l_{j_{1}}:\tau_{j_{1}}\rangle\cap\langle l_{j}:\tau_{j}\mid j\in
J\setminus\\{j_{1}\\}\rangle).$

for some $j_{1}\in J$. Now $j_{0}\not\in J$ implies $l_{j_{0}}\neq l_{j_{1}}$,
and the thesis follows by 3.1.8 and the induction hypothesis.

######  Lemma 3.

  1. (1)

$\langle l_{i}:\sigma_{i}\mid i\in I\rangle\leq\langle l_{j}:\tau_{j}\mid j\in
J\rangle\Leftrightarrow J\subseteq I\And\forall j\in
J.\;\sigma_{j}\leq\tau_{j}$,

  2. (2)

$\langle l_{i}:\sigma_{i}\ \mid\ i\in I\rangle\cap\langle l_{j}:\tau_{j}\mid
j\in J\rangle=\langle
l_{i}:\sigma_{i},l_{j}:\tau_{j},l_{k}:\sigma_{k}\cap\tau_{k}\mid i\in
I\setminus J,j\in J\setminus I,k\in I\cap J\rangle$,

  3. (3)

$\langle l_{i}:\sigma_{i}\ \mid\ i\in I\rangle+\langle l_{j}:\tau_{j}\mid j\in
J\rangle=\langle l_{i}:\sigma_{i},l_{j}:\tau_{j}\mid i\in I\setminus J,j\in
J\rangle$,

  4. (4)

$\forall\rho\in\mathbb{T}_{{\langle\rangle}}.\;\exists\ \langle
l_{i}:\sigma_{i}\mid i\in I\rangle.~{}\rho=\langle l_{i}:\sigma_{i}\mid i\in
I\rangle$.

######  Proof 3.3.

Through this proof let $\rho_{1}\equiv\langle l_{i}:\sigma_{i}\mid i\in
I\rangle$ and $\rho_{2}\equiv\langle l_{j}:\tau_{j}\mid j\in J\rangle$, where
$\equiv$ denotes syntactic identity up to commutativity and associativity of
$\cap$.

  1. (1)

The only if part is proved by induction over the derivation of
$\rho_{1}\leq\rho_{2}$. If this equation is an instance of axiom 3.1.1 then
$J=\emptyset\subseteq I$ and $\forall j\in J.\;\sigma_{j}\leq\tau_{j}$ is
vacuously true.

Axiom 3.1.2 doesn’t apply being the labels $l_{i}$ pairwise distinct.

In case the derivation ends by rule 3.1.3 we have $I=J=\\{l\\}$ and
$\sigma\leq\tau$ by the premise of the rule.

In case of the axiom instance ${\langle l_{1}:\sigma\rangle}\cap{\langle
l_{2}:\tau\rangle}\leq{\langle l_{1}:\sigma\rangle}$ of 3.1.2 we have
$J=\\{l_{1}\\}\subseteq\\{l_{1},l_{2}\\}=I$ and obviously $\sigma\leq\sigma$.

Finally in case of deriving $\rho_{1}\leq(\rho_{3}\cap\rho_{4})$ from
$\rho_{1}\leq\rho_{3}$ and $\rho_{1}\leq\rho_{4}$, where
$\rho_{2}\equiv\rho_{3}\cap\rho_{4}$, we have that for some
$J^{\prime},J^{\prime\prime}$ such that $J=J^{\prime}\cup J^{\prime\prime}$ it
is $\rho_{3}\equiv\langle l_{h}:\tau_{h}\mid h\in J^{\prime}\rangle$ and
$\rho_{4}\equiv\langle l_{k}:\tau_{k}\mid k\in J^{\prime\prime}\rangle$. By
induction we know that $J^{\prime}\subseteq I$ and $\sigma_{h}\leq\tau_{h}$
for all $h\in J^{\prime}$ and $J^{\prime\prime}\subseteq I$ and
$\sigma_{k}\leq\tau_{k}$ for all $k\in J^{\prime\prime}$. Therefore
$J=J^{\prime}\cup J^{\prime\prime}\subseteq I$ and $\sigma_{j}\leq\tau_{j}$
for all $j\in J$.

For the if part we reason by induction over the cardinality of $J$. If $|J|=0$
then $\rho_{2}\equiv{\langle\rangle}$, hence either $I=\emptyset$, but then
$\rho_{1}\equiv{\langle\rangle}$; or $I\neq\emptyset$ so that
$\rho_{1}\leq\langle l_{i}:\sigma_{i}\rangle\leq{\langle\rangle}$ for any
$i\in I$, using axiom 3.1.1. If $|J|>0$ then let $j_{0}\in J$ be any index:
then $\rho_{2}\equiv\langle l_{j}:\tau_{j}\mid j\in
J\setminus\\{j_{0}\\}\rangle\cap\langle l_{j_{0}}:\tau_{j_{0}}\rangle$. Now by
induction $\rho_{1}\leq\langle l_{j}:\tau_{j}\mid j\in
J\setminus\\{j_{0}\\}\rangle$; by hypothesis $\sigma_{j_{0}}\leq\tau_{j_{0}}$
so that $\rho_{1}\leq\langle l_{j_{0}}:\sigma_{j_{0}}\rangle\leq\langle
l_{j_{0}}:\tau_{j_{0}}\rangle$ and we conclude being $\cap$ the meet w.r.t.
$\leq$.

  2. (2)

This is an immediate consequence of commutativity, associativity, idempotency
of $\cap$ and equation (2).

  3. (3)

If $I=\emptyset$ then$\rho_{1}={\langle\rangle}$ and the thesis follows by
3.1.4. Otherwise we have:

$\begin{array}[]{llll}\rho_{1}+\rho_{2}&=&\bigcap_{i\in I}({\langle
l_{i}:\sigma_{i}\rangle}+\rho_{2})&\mbox{by repeated applications of
\ref{def:typeInclusionRec-new}.\ref{leq-ax-6}}\\\ &=&\bigcap_{i\in I}\langle
l_{i}:\sigma_{i},l_{j}:\tau_{j}\mid i\not\in J,j\in J\rangle&\mbox{by Lemma
\ref{lem:derivedLeq}.\ref{lem:derivedLeq-b} and
\ref{lem:derivedLeq}.\ref{lem:derivedLeq-c}}\\\ &\equiv&\langle
l_{i}:\sigma_{i},l_{j}:\tau_{j}\mid i\in I\setminus J,j\in
J\rangle.\end{array}$

  4. (4)

By induction over $\rho$. If $\rho={\langle\rangle}$ there is nothing to
prove.

If $\rho\equiv\rho_{1}\cap\rho_{2}$ then by induction $\rho_{1}=\langle
l_{i}^{1}:\sigma_{i}^{1}\mid i\in I_{1}\rangle$ and $\rho_{2}=\langle
l_{i}^{2}:\sigma_{i}^{2}\mid i\in I_{2}\rangle$ so that the thesis follows by
(2) above and the fact that $=$ is a congruence w.r.t. $\cap$.

Similarly if $\rho\equiv\rho_{1}+\rho_{2}$ the thesis follows by induction
using (3) and the fact that $=$ is a congruence w.r.t. $+$ by 3.1.9 and
3.1.10.

######  Remark 4.

By 3.1.6 the $+$ distributes to the left over $\cap$; however this doesn’t
hold to the right, namely
$\rho_{1}+(\rho_{2}\cap\rho_{3})\neq(\rho_{1}+\rho_{2})\cap(\rho_{1}+\rho_{3})$:
take $\rho_{1}\equiv{\langle l_{1}:\sigma_{1},l_{2}:\sigma_{2}\rangle}$,
$\rho_{2}\equiv{\langle l_{1}:\sigma^{\prime}_{1}\rangle}$ and
$\rho_{3}\equiv{\langle l_{2}:\sigma^{\prime}_{2}\rangle}$, with
$\sigma_{1}\neq\sigma^{\prime}_{1}$ and $\sigma_{2}\neq\sigma^{\prime}_{2}$.
Then by Lemma 3.3 we have: $\rho_{1}+(\rho_{2}\cap\rho_{3})=\rho_{1}+{\langle
l_{1}:\sigma^{\prime}_{1},l_{2}:\sigma^{\prime}_{2}\rangle}={\langle
l_{1}:\sigma^{\prime}_{1},l_{2}:\sigma^{\prime}_{2}\rangle}$, while
$(\rho_{1}+\rho_{3})\cap(\rho_{2}+\rho_{3})={\langle
l_{1}:\sigma_{1},l_{2}:\sigma^{\prime}_{2}\rangle}\cap{\langle
l_{1}:\sigma^{\prime}_{1},l_{2}:\sigma_{2}\rangle}={\langle
l_{1}:\sigma_{1}\cap\sigma^{\prime}_{1},l_{2}:\sigma_{2}\cap\sigma^{\prime}_{2}\rangle}.$
The last example suggests that
$(\rho_{1}+\rho_{2})\cap(\rho_{1}+\rho_{3})\leq\rho_{1}+(\rho_{2}\cap\rho_{3})$.

On the other hand by 3.1.9 $+$ is monotonic in its first argument. However we
have
$\rho_{2}\leq\rho_{3}\not\Rightarrow\rho_{1}+\rho_{2}\leq\rho_{1}+\rho_{3}$.
Indeed:

$\begin{array}[]{llll}{\langle
l_{0}:\sigma_{1},l_{1}:\sigma_{2}\rangle}+{\langle
l_{1}:\sigma_{3},l_{2}:\sigma_{4}\rangle}&=&{\langle
l_{0}:\sigma_{1},l_{1}:\sigma_{3},l_{2}:\sigma_{4}\rangle}\\\
&\not\leq&{\langle
l_{0}:\sigma_{0},l_{1}:\sigma_{1},l_{2}:\sigma_{4}\rangle}&\mbox{if
$\sigma_{3}\not\leq\sigma_{1}$}\\\ &=&{\langle
l_{0}:\sigma_{1},l_{1}:\sigma_{2}\rangle}+{\langle
l_{2}:\sigma_{4}\rangle}\end{array}$

even if ${\langle l_{1}:\sigma_{1},l_{2}:\sigma_{2}\rangle}\leq{\langle
l_{2}:\sigma_{2}\rangle}$. From this we conclude that $+$ is not monotonic in
its second argument. Comparing this with 3.1.10 we see that $\leq$ is not a
precongruence w.r.t. $+$, while $=$, namely the symmetric closure of $\leq$,
is a congruence.

Finally if one assumes (1)-(3) of Lemma 3 as axioms then (pre)-congruence
axioms in Definition 3.1 become derivable. The opposite is hardly provable and
possibly false111Remark of an anonymous referee about our former attempt to
derive 3.1.9 and 3.1.10 from the other axioms..

Lemma 3.1 states that subtyping among intersection of unary record types
subsumes subtyping in width and depth of ordinary record types from the
literature. Lemma 3.3 shows that the $+$ type constructor reflects at the
level of types the operational behavior of the merge operator $\oplus$. Lemma
3.4 says that any record type is equivalent to an intersection of unary record
types; this implies that types of the form $\rho_{1}+\rho_{2}$ are eliminable
in principle. However, they play a key role in typing mixins, motivating the
issue of control of negative information in the synthesis process: see Section
5. More properties of subtyping record types w.r.t. $+$ and $\cap$ are listed
in the next two lemmas.

######  Lemma 5.

$\rho_{1}+\rho_{2}=\rho_{1}\cap\rho_{2}\Leftrightarrow\rho_{1}+\rho_{2}\leq\rho_{1}$.

######  Proof 3.4.

W.l.o.g. by 3.4 let us assume that $\rho_{1}={\langle l_{i}:\sigma_{1,i}\mid
i\in I\rangle}$, $\rho_{2}={\langle l_{j}:\sigma_{2,j}\mid j\in J\rangle}$ and
$\rho_{3}={\langle l_{k}:\sigma_{3,k}\mid k\in K\rangle}$. If
$\rho_{1}+\rho_{2}=\rho_{1}\cap\rho_{2}$ then by 3.2 and 3.3:

$\displaystyle{\langle l_{i}:\sigma_{1,i},l_{j}:\sigma_{2,j}\mid i\in
I\setminus J,j\in J\rangle}$ $\displaystyle=\;$ $\displaystyle{\langle
l_{i}:\sigma_{1,i},l_{j}:\sigma_{2,j},l_{k}:\sigma_{1,k}\cap\sigma_{2,k}\mid
i\in I\setminus J,j\in J\setminus I,k\in I\cap I\rangle}$

Obviously $J=(J\setminus I)\cup(I\cap J)$ and from 3.1 we deduce that
$\sigma_{2,j}=\sigma_{1,j}\cap\sigma_{2,j}$ for all $j\in J$, hence
$\sigma_{2,j}\leq\sigma_{1,j}$ so we conclude that
$\rho_{1}+\rho_{2}\leq\rho_{1}$ again by 3.1. Since all these implications can
be reverted, we conclude.

Let us define the map $\mbox{\it
lbl}:\mathbb{T}_{{\langle\rangle}}\to\wp(\mbox{\bf Label})$ (where
$\wp(\mbox{\bf Label})$ is the powerset of Label) by:

$\begin{array}[]{llll}\mbox{\it lbl}({\langle
l:\sigma\rangle})=\\{l\\},&\mbox{\it lbl}(\rho_{1}\cap\rho_{2})=\mbox{\it
lbl}(\rho_{1}+\rho_{2})=\mbox{\it lbl}(\rho_{1})\cup\mbox{\it
lbl}(\rho_{2}).\end{array}$

######  Lemma 6.

  1. (1)

$\rho_{1}=\rho_{2}\Rightarrow\mbox{\it lbl}(\rho_{1})=\mbox{\it
lbl}(\rho_{2})$,

  2. (2)

$\mbox{\it lbl}(\rho_{1})\cap\mbox{\it
lbl}(\rho_{2})=\emptyset\Rightarrow\rho_{1}+\rho_{2}=\rho_{1}\cap\rho_{2}$,

  3. (3)

$\mbox{\it lbl}(\rho_{1})\subseteq\mbox{\it
lbl}(\rho_{2})\Rightarrow\rho_{1}+\rho_{2}=\rho_{2}$,

  4. (4)

$\mbox{\it lbl}(\rho_{2})=\mbox{\it
lbl}(\rho_{3})\Rightarrow(\rho_{1}+\rho_{2})\cap(\rho_{1}+\rho_{3})=\rho_{1}+(\rho_{2}\cap\rho_{3})$.

Part (1) follows by 3.1, and (2) is a consequence of the fact that if
$\mbox{\it lbl}(\rho_{1})\cap\mbox{\it lbl}(\rho_{2})=\emptyset$ then equation
(1) $\langle l:\sigma\rangle+\langle l^{\prime}:\tau\rangle=\langle
l:\sigma\rangle\cap\langle l^{\prime}:\tau\rangle$ repeatedly applies. Part
(3) follows by 3.3.

To see part (4) we can assume by 3.4 that $\rho_{1}={\langle
l_{i}:\sigma_{1,i}\mid i\in I\rangle}$, $\rho_{2}={\langle
l_{j}:\sigma_{2,j}\mid j\in J\rangle}$ and $\rho_{3}={\langle
l_{k}:\sigma_{3,k}\mid k\in K\rangle}$. Since $\mbox{\it
lbl}(\rho_{2})=\mbox{\it lbl}(\rho_{3})$ we have that $J=K$, so that:

$\begin{array}[]{llll}\rho_{1}+\rho_{2}&=&{\langle
l_{i}:\sigma_{1,i},l_{j}:\sigma_{2,j}\mid i\in I\setminus J,j\in
J\rangle}&\mbox{by \ref{lem:normal-recordTypes}.\ref{lem:normal-
recordTypes-b}}\\\\[2.84526pt] \rho_{1}+\rho_{3}&=&{\langle
l_{i}:\sigma_{1,i},l_{j}:\sigma_{3,j}\mid i\in I\setminus J,j\in
J\rangle}&\mbox{by \ref{lem:normal-recordTypes}.\ref{lem:normal-
recordTypes-b}}\\\\[2.84526pt] \rho_{2}\cap\rho_{3}&=&{\langle
l_{j}:\sigma_{2,j}\cap\sigma_{3,j}\mid j\in J\rangle}&\mbox{by
\ref{lem:normal-recordTypes}.\ref{lem:normal-recordTypes-ab}}\end{array}$

Again by 3.2, 3.3 and the fact that
$\sigma_{1,i}\cap\sigma_{1,i}=\sigma_{1,i}$ we conclude that
$(\rho_{1}+\rho_{2})\cap(\rho_{1}+\rho_{3})$ and
$\rho_{1}+(\rho_{2}\cap\rho_{3})$ are both equal to

${\langle l_{i}:\sigma_{1,i},l_{j}:\sigma_{2,j}\cap\sigma_{3,j}\mid i\in
I\setminus J,j\in J\rangle}.$

About Lemma 6.2 above note that condition $\mbox{\it
lbl}(\rho_{1})\cap\mbox{\it lbl}(\rho_{2})=\emptyset$ is essential, since
$\cap$ is commutative while $\rho_{1}+\rho_{2}\neq\rho_{2}+\rho_{1}$ in
general, as it immediately follows by Lemma 3.3.

We come now to the type assignment system. A basis (also called a context in
the literature) is a finite set
$\Gamma=\\{x_{1}:\sigma_{n},\ldots,x_{n}:\sigma_{n}\\}$, where the variables
$x_{i}$ are pairwise distinct; we set $\textrm{\it
dom}(\Gamma)=\\{x\mid\exists\,\sigma.~{}x:\sigma\in\Gamma\\}$ and we write
$\Gamma,x:\sigma$ for $\Gamma\cup\\{x:\sigma\\}$ where $x\not\in\textrm{\it
dom}(\Gamma)$. Then we consider the following extension of the system in
[BCDC83], also called BCD in the literature.

[Type Assignment] The rules of the assignment system are:

$\displaystyle{\begin{array}[]{ccc }{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1x:\sigma\in\Gamma$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.23473pt\hbox{\kern
3.00003pt$(\textrm{\it Ax})$}}}\hbox{\kern
0.27779pt\hbox{$\displaystyle\Gamma\vdash x:\sigma$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
4.58334pt\hbox{$\displaystyle\penalty 1\Gamma,x:\sigma\vdash M:\tau$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=73.67554pt\hbox{\kern
3.00003pt$(\rightarrow\mbox{\it I})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda
x.M:\sigma\to\tau$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\sigma\to\tau\quad\Gamma\vdash N:\sigma$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=105.99367pt\hbox{\kern
3.00003pt$(\rightarrow\mbox{\it E})$}}}\hbox{\kern
27.72787pt\hbox{$\displaystyle\Gamma\vdash MN:\tau$}}}\par}\\\\[17.07164pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash M:\sigma\quad\Gamma\vdash
M:\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=94.1685pt\hbox{\kern
3.00003pt$(\cap)$}}}\hbox{\kern 17.9652pt\hbox{$\displaystyle\Gamma\vdash
M:\sigma\cap\tau$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 21.63297pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=43.26593pt\hbox{\kern
3.00003pt$(\omega)$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Gamma\vdash
M:\omega$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\sigma\qquad\sigma\leq\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=86.17445pt\hbox{\kern
3.00003pt$(\leq)$}}}\hbox{\kern 23.7696pt\hbox{$\displaystyle\Gamma\vdash
M:\tau$}}}\par\par}\\\\[17.07164pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 49.9642pt\hbox{$\displaystyle\penalty 1$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=99.9284pt\hbox{\kern
3.00003pt$({\langle\rangle})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash{\langle l_{i}=M_{i}\ |\ i\in
I\rangle}:{\langle\rangle}$}}}\par}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 20.73865pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
M_{k}:\sigma\quad k\in I$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=117.47029pt\hbox{\kern
3.00003pt$(\mbox{\it rec})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash{\langle l_{i}=M_{i}\ |\ i\in
I\rangle}:\langle l_{k}:\sigma\rangle$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash M:\langle l:\sigma\rangle$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=59.26941pt\hbox{\kern
3.00003pt$(\mbox{\it sel})$}}}\hbox{\kern
4.72223pt\hbox{$\displaystyle\Gamma\vdash M.l:\sigma$}}}\par}\\\\[17.07164pt]
\lx@intercol\hfil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\rho_{1}\qquad\Gamma\vdash R:\rho_{2}\quad(*)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=129.67949pt\hbox{\kern
3.00003pt$(+)$}}}\hbox{\kern 23.40276pt\hbox{$\displaystyle\Gamma\vdash
M\oplus R:\rho_{1}+\rho_{2}$}}}}\hfil\lx@intercol\par\end{array}}$

where $(*)$ in rule $(+)$ is the side condition: $\mbox{\it lbl}(R)=\mbox{\it
lbl}(\rho_{2})$.

Using Lemma 3.1, the following rule is easily shown to be admissible:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
8.98372pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
M_{j}:\sigma_{j}\qquad\forall j\in J\subseteq I$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=134.02078pt\hbox{\kern
3.00003pt$(\mbox{\it rec}^{\prime})$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash{\langle l_{i}=M_{i}\mid i\in
I\rangle}:\langle l_{j}:\sigma_{i}\mid j\in J\rangle$}}}}$

Contrary to this, the side condition $(*)$ of rule $(+)$ is equivalent to
“exact” record typing in [BC90], disallowing record subtyping in width. Such a
condition is necessary for soundness of typing. Indeed, suppose that
$\Gamma\vdash M_{0}:\sigma$ and $\Gamma\vdash
M^{\prime}_{0}:\sigma^{\prime}_{0}$ but $\Gamma\not\vdash
M^{\prime}_{0}:\sigma_{0}$; then without $(*)$ we could derive:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash{\langle
l_{0}=M_{0}\rangle}:\langle l_{0}:\sigma_{0}\rangle\qquad\Gamma\vdash{\langle
l_{0}=M^{\prime}_{0},l_{1}:\sigma_{1}\rangle}:\langle
l_{1}:\sigma_{1}\rangle$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=210.53499pt\hbox{}}}\hbox{\kern
10.06958pt\hbox{$\displaystyle\Gamma\vdash{\langle
l_{0}=M_{0}\rangle}\,\oplus\,{\langle
l_{0}=M^{\prime}_{0},l:_{1}:\sigma_{1}\rangle}:{\langle
l_{0}:\sigma_{0},l_{1}:\sigma_{1}\rangle}$}}}}$

from which we obtain that $\Gamma\vdash({\langle
l_{0}=M_{0}\rangle}\,\oplus\,{\langle
l_{0}=M^{\prime}_{0},l:_{1}:\sigma_{1}\rangle}).l_{0}:\sigma_{0}$ breaking
subject reduction, since $({\langle l_{0}=M_{0}\rangle}\,\oplus\,{\langle
l_{0}=M^{\prime}_{0},l:_{1}:\sigma_{1}\rangle}).l_{0}\longrightarrow^{*}M^{\prime}_{0}$.
The essential point is that proving that $\Gamma\vdash N:{\langle
l:\sigma\rangle}$ doesn’t imply that $l^{\prime}\not\in\mbox{\it
lbl}(R^{\prime})$ for any $l^{\prime}\neq l$, which follows only by the
uncomputable (not even recursively enumerable) statement that
$\Gamma\not\vdash N:{\langle l^{\prime}:\omega\rangle}$, a negative
information.

This explains the restriction to record terms as the second argument of
$\,\oplus\,$: in fact, allowing $M\,\oplus\,N$ to be well formed for an
arbitrary $N$ we might have $N\equiv x$ in $\lambda x.\,(M\,\oplus\,x)$. But
extending lbl to all terms in $\Lambda_{R}$ is not possible without severely
limiting the expressiveness of the assignment system. In fact to say that
$\mbox{\it lbl}(N)=\mbox{\it lbl}(R)$ if $N\longrightarrow^{*}R$ would make
the lbl function non computable; on the other hand putting $\mbox{\it
lbl}(x)=\emptyset$, which is the only reasonable and conservative choice as we
do not know possible substitutions for $x$ in $\lambda x.\,(M\,\oplus\,x)$,
implies that the latter term has type $\omega\to\omega=\omega$ at best.

As a final remark, let us observe that we do not adopt exact typing of records
in general, but only for typing the right-hand side of $\oplus$-terms, a
feature that will be essential when typing mixins.

The following two lemmas are standard after [BCDC83].

######  Lemma 7.

$\bigcap_{i\in I}(\sigma_{i}\to\tau_{i})\leq\sigma\to\tau\Rightarrow\exists
J\subseteq I.\;\sigma\leq\bigcap_{j\in J}\sigma_{j}\And\bigcap_{j\in
J}\tau_{j}\leq\tau$

######  Proof 3.5.

By induction over the proof of $\bigcap_{i\in
I}(\sigma_{i}\to\tau_{i})\leq\sigma\to\tau$.

######  Lemma 8.

The following rule is admissible:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma,x:\tau\vdash
M:\sigma\quad\tau^{\prime}\leq\tau$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=95.34744pt\hbox{}}}\hbox{\kern
16.03816pt\hbox{$\displaystyle\Gamma,x:\tau^{\prime}\vdash M:\sigma$}}}}$

By induction over the derivation of $\Gamma,x:\tau\vdash M:\sigma$. The only
non-trivial case is when $\Gamma,x:\tau\vdash M:\sigma$ is an instance of
$(\textrm{\it Ax})$ and $M\equiv x$. In this case $\sigma=\tau$ and we replace
the axiom by the inference:

tensy  $\displaystyle\penalty 1\Gamma,x:\tau^{\prime}\vdash
x:\tau^{\prime}\quad\tau^{\prime}\leq\tau$ $(\leq)$
$\displaystyle\Gamma,x:\tau^{\prime}\vdash x:\tau$

######  Lemma 9 (Generation).

Let $\sigma\neq\omega$:

  1. (1)

$\Gamma\vdash
x:\sigma\Leftrightarrow\exists\tau.\;x:\tau\in\Gamma\And\tau\leq\sigma$,

  2. (2)

$\Gamma\vdash\lambda x.M:\sigma\Leftrightarrow\exists\;I,(\sigma_{i})_{i\in
I},(\tau_{i})_{i\in I}.~{}~{}\Gamma,x:\sigma_{i}\vdash
M:\tau_{i}\And\bigcap_{i\in I}(\sigma_{i}\rightarrow\tau_{i})\leq\sigma$,

  3. (3)

$\Gamma\vdash MN:\sigma\Leftrightarrow\exists\;\tau.~{}\Gamma\vdash
M:\tau\to\sigma\And\Gamma\vdash N:\tau$,

  4. (4)

$\Gamma\vdash{\langle l_{i}=M_{i}\mid i\in
I\rangle}:\sigma\Leftrightarrow\forall i\in I\
\exists\;\sigma_{i}.\;\Gamma\vdash M_{i}:\sigma_{i}\And{\langle
l_{i}:\sigma_{i}\mid i\in I\rangle}\leq\sigma$,

  5. (5)

$\Gamma\vdash M.l:\sigma\Leftrightarrow\Gamma\vdash M:{\langle
l:\sigma\rangle}$,

  6. (6)

$\Gamma\vdash M\oplus
R:\sigma\Leftrightarrow\exists\>\rho_{1},\rho_{2}.~{}\Gamma\vdash
M:\rho_{1}\And\Gamma\vdash R:\rho_{2}\And\mbox{\it lbl}(R)=\mbox{\it
lbl}(\rho_{2})\And\rho_{1}+\rho_{2}\leq\sigma$.

All the if parts are obvious. For the only if parts first observe that there
is a one-to-one correspondence between the term constructors and the rules in
the type system but in case of rules $(\omega)$, $(\cap)$ and $(\leq)$.
Indeed, rule $({\langle\rangle})$ is no exception as the typing
$\Gamma\vdash{\langle l_{i}=M_{i}\ |\ i\in I\rangle}:{\langle\rangle}$ is
derivable using $(\mbox{\it rec})$ and $(\leq)$ in all cases but when
$I=\emptyset$, in which case $({\langle\rangle})$ becomes the axiom
$\Gamma\vdash{\langle\rangle}:{\langle\rangle}$ and ${\langle\rangle}$ is a
nullary operator.

Disregarding rule $(\omega)$ because of the hypothesis $\sigma\neq\omega$, all
the statements in this lemma depend on the remark that any derivation
$\mathcal{D}$ of $\Gamma\vdash M:\sigma$ consists of a finite set of
subderivations $\mathcal{D}_{i}$ of judgments $\Gamma\vdash M:\sigma_{i}$ such
that each $\mathcal{D}_{i}$ ends by the rule corresponding to the main term
constructor of $M$, and that in $\mathcal{D}$ all the inferences below the
$\mathcal{D}_{i}$ are instances of either rule $(\cap)$ or $(\leq)$. By noting
that inferences using $(\cap)$ and $(\leq)$ commute that is:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\sigma^{\prime}\quad\sigma^{\prime}\leq\sigma$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=70.03766pt\hbox{\kern
2.70003pt$(\leq)$}}}\hbox{\kern 15.77872pt\hbox{$\displaystyle\Gamma\vdash
M:\sigma$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\quad\Gamma\vdash
M:\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=161.10652pt\hbox{\kern
2.70003pt$(\cap)$}}}\hbox{\kern 54.34595pt\hbox{$\displaystyle\Gamma\vdash
M:\sigma\cap\tau$}}}}~{}~{}\mbox{becomes}~{}~{}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\sigma^{\prime}\quad\Gamma\vdash M:\tau$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=86.13812pt\hbox{\kern
2.70003pt$(\cap)$}}}\hbox{\kern 17.16876pt\hbox{$\displaystyle\Gamma\vdash
M:\sigma^{\prime}\cap\tau$}}}}\hskip 4.5pt plus 1.0fil\penalty
2\quad\sigma^{\prime}\cap\tau\leq\sigma\cap\tau$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=188.47533pt\hbox{\kern
2.70003pt$(\leq)$}}}\hbox{\kern 68.03035pt\hbox{$\displaystyle\Gamma\vdash
M:\sigma\cap\tau$}}}}$

we can freely assume that all $(\cap)$ inferences precede $(\leq)$ rules,
concluding that $\bigcap_{i}\sigma_{i}\leq\sigma$.

Given that all the statements of this lemma are deduced by reading backward
rules $(\textrm{\it Ax})$, $(\rightarrow\mbox{\it I})$, $(\rightarrow\mbox{\it
E})$, $({\langle\rangle})$, $(\mbox{\it rec})$, $(\mbox{\it sel})$ and $(+)$.
All cases are either standard from [BCDC83] or are easy extensions thereof,
but that of rule $(+)$ in $(\ref{gen:merge})$ above. In this case we know that
in the derivation of $\Gamma\vdash M\oplus R:\sigma$ there are subderivations
ending by the inference:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\rho_{i,1}\quad\Gamma\vdash R:\rho_{i,2}\quad\mbox{\it
lbl}(\rho_{i,2})=\mbox{\it lbl}(R)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=181.32982pt\hbox{\kern
3.00003pt$(+)$}}}\hbox{\kern 45.7431pt\hbox{$\displaystyle\Gamma\vdash M\oplus
R:\rho_{i,1}+\rho_{i,2}$}}}}$

where the side condition $\mbox{\it lbl}(\rho_{i,2})=\mbox{\it lbl}(R)$ holds
for all $i\in I$; then by the remark above we have that $\bigcap_{i\in
I}(\rho_{i,1}+\rho_{i,2})\leq\sigma$. Now taking $\rho_{1}=\bigcap_{i\in
I}\rho_{i,1}$ and $\rho_{2}=\bigcap_{i\in I}\rho_{i,2}$ we have that:

$\begin{array}[b]{rcll}\sigma&\geq&\bigcap_{i\in I}(\rho_{i,1}+\rho_{i,2})\\\
&\geq&\bigcap_{i\in I}(\rho_{1}+\rho_{i,2})&\mbox{by Def.
\ref{def:typeInclusionRec-new}.\ref{leq-ax-11}, since $\rho_{i,1}\geq\rho_{1}$
for all $i\in I$}\\\ &=&\rho_{1}+\rho_{2}&\mbox{by
\ref{lem:label}.\ref{lem:label-c} since $\mbox{\it lbl}(\rho_{2})=\mbox{\it
lbl}(\rho_{i,2})$ for all $i\in I$.}\end{array}$

######  Lemma 10 (Substitution).

$\Gamma,x:\sigma\vdash M:\tau\And\Gamma\vdash N:\sigma\Rightarrow\Gamma\vdash
M\\{N/x\\}:\tau.$

######  Proof 3.6.

By induction over the derivation of $\Gamma,x:\sigma\vdash M:\tau$. Observe
that the writing $\Gamma,x:\sigma$ implies that $x\not\in\Gamma$; on the other
hand if $\Gamma\vdash N:\sigma$ is derivable then $\mbox{\it
fv}(N)\subseteq\Gamma$, hence $x\not\in\mbox{\it fv}(N)$.

######  Theorem 11 (Subject reduction).

$\Gamma\vdash M:\sigma\And M\longrightarrow N\Rightarrow\Gamma\vdash
N:\sigma$.

######  Proof 3.7.

The proof is by cases of reduction rules, using Lemma 9.

  1. (1)

Case $M\equiv(\lambda x.M^{\prime})N^{\prime}$. Then $N\equiv
M^{\prime}\\{N^{\prime}/x\\}$ by rule ($\beta$). By Lemma 9.3, there exists
$\tau$ such that $\Gamma\vdash(\lambda x.M^{\prime}):\tau\to\sigma$ and
$\Gamma\vdash N^{\prime}:\tau$. By Lemma 9.2, there exist
$I,\sigma_{i},\tau_{i}$ such that $\Gamma,x:\tau_{i}\vdash
M^{\prime}:\sigma_{i}$ for all $i\in I$ and $\bigcap_{i\in
I}(\tau_{i}\rightarrow\sigma_{i})\leq\tau\to\sigma$. By Lemma 7 this implies
that there is $J\subseteq I$ such that $\tau\leq\bigcap_{j\in J}\tau_{j}$ and
$\bigcap_{j\in J}\sigma_{j}\leq\sigma$. By Lemma 8 this implies that
$\Gamma,x:\tau\vdash M^{\prime}:\sigma_{j}$ for all $j\in J$, so that by rule
$(\cap)$ we have $\Gamma,x:\tau\vdash M^{\prime}:\bigcap_{j\in J}\sigma_{j}$
and hence $\Gamma,x:\tau\vdash M^{\prime}:\sigma$ by $(\leq)$. From this and
$\Gamma\vdash N^{\prime}:\tau$ we get $\Gamma\vdash
M^{\prime}\\{N^{\prime}/x\\}:\sigma$ by Lemma 10.

  2. (2)

Case $M\equiv\langle l_{i}=M_{i}\mid i\in I\rangle.l_{j}$. Then $N\equiv
M_{j}$ for some $j\in I$ by rule (sel). By Lemma 9.5 $\Gamma\vdash M:{\langle
l_{j}:\sigma\rangle}$, hence by 9.4 for all $i\in I$ there exists $\sigma_{i}$
such that $\Gamma\vdash M_{i}:\sigma_{i}$ and ${\langle l_{i}:\sigma_{i}\mid
i\in I\rangle}\leq{\langle l_{j}:\sigma\rangle}$. Now by the fact that $j\in
I$ and by Lemma 3.1 it follows that $\Gamma\vdash M_{j}:\sigma_{j}$ and
$\sigma_{j}\leq\sigma$, hence $\Gamma\vdash M_{j}:\sigma$ by rule $(\leq)$.

  3. (3)

Case $M\equiv\langle l_{i}=M_{i}\mid i\in I\rangle\,\oplus\,\langle
l_{j}=N_{j}\mid\ j\in J\rangle$. Then by rule ($\oplus$):

$N\equiv\langle l_{i}=M_{i},\ l_{j}=N_{j}\mid i\in I\setminus J,\ j\in
J\rangle.$

By Lemma 9.6 there exist the record types $\rho_{1},\rho_{2}$ such that:

    1. (a)

$\Gamma\vdash\langle l_{i}=M_{i}\mid i\in I\rangle:\rho_{1}$,

    2. (b)

$\Gamma\vdash\langle l_{j}=N_{j}\mid j\in J\rangle:\rho_{2}$,

    3. (c)

$\mbox{\it lbl}(\rho_{2})=\mbox{\it lbl}(\langle l_{j}=N_{j}\mid\ j\in
J\rangle)=\\{l_{j}\mid j\in J\\}$,

    4. (d)

$\rho_{1}+\rho_{2}\leq\sigma$.

By (3a) and (3b) and by Lemma 9.4 we have that for all $i\in I$ there exist
$\sigma_{i}$ such that $\Gamma\vdash M_{i}:\sigma_{i}$, with ${\langle
l_{i}:\sigma_{i}\mid i\in I\rangle}\leq\rho_{1}$, and similarly for all $j\in
J$ there are $\tau_{j}$ such that $\Gamma\vdash N_{j}:\tau_{j}$ and ${\langle
l_{j}:\tau_{j}\mid j\in J\rangle}\leq\rho_{2}$.

Since $\Gamma\vdash M_{i}:\sigma_{i}$ for all $i\in I$, a fortiori it holds
for all $i\in I\setminus J$. On the other hand, by Lemma 3.4 we know that
$\rho_{2}={\langle l_{k}:\tau^{\prime}_{k}\mid k\in K\rangle}$ for some $K$
and $\tau^{\prime}_{k}$, so that ${\langle l_{j}:\tau_{j}\mid j\in
J\rangle}\leq\rho_{2}$ implies $J\supseteq K$ and
$\tau_{k}\leq\tau^{\prime}_{k}$ for all $k\in K$ by Lemma 3.1. It follows that
$J=K$ by (3c), and $\Gamma\vdash N_{j}:\tau^{\prime}_{j}$ for all $j\in J$ by
rule $(\leq)$. Then by rule $(\mbox{\it rec})$ and $(\cap)$ we conclude that

$\Gamma\vdash N:{\langle l_{i}:\sigma_{i},\ l_{j}:\tau^{\prime}_{j}\mid i\in
I\setminus J,\ j\in J\rangle}.$

Now ${\langle l_{i}:\sigma_{i},\ l_{j}:\tau^{\prime}_{j}\mid i\in I\setminus
J,\ j\in J\rangle}={\langle l_{i}:\sigma_{i}\mid i\in I\rangle}+\rho_{2}$ by
Lemma 3.3, but since

$\displaystyle{\langle l_{i}:\sigma_{i}\mid i\in I\rangle}\leq\rho_{1}$

we have by Definition 3.1.9 that ${\langle l_{i}:\sigma_{i}\mid i\in
I\rangle}+\rho_{2}\leq\rho_{1}+\rho_{2}$; then we conclude that $\Gamma\vdash
N:\sigma$ by (3d) and rule $(\leq)$.

###  3.2. Class and Mixin combinators

The following definition of classes and mixins is inspired by [CHC90] and
[BC90] respectively, though with some departures to be discussed below. To
make the description more concrete, in the examples we add constants to
$\Lambda_{R}$.

Recall that a combinator is a term in $\Lambda_{R}^{0}$, namely a closed term.
Let $\mathbf{Y}$ be Curry’s fixed point combinator: $\lambda f.(\lambda
x.f(xx))(\lambda x.f(xx))$ (the actual definition of $\mathbf{Y}$ is
immaterial however, since all fixed point combinators have the same Böhm tree
as a consequence of [Bar84] Lemma 6.5.3, and hence have the same types in BCD
by the approximation theorem: see e.g. [BDS13] Theorem 12.1.17).

Let $\textsf{myClass},\textsf{state}$ and argClass be (term) variables and
$\mathbf{Y}$ be a fixed point combinator; then we define the following sets of
combinators:

$\begin{array}[]{llll}\text{Class:}&C&::=&\mathbf{Y}(\lambda\,\textsf{myClass}\
\lambda\,\textsf{state}.\,{\langle l_{i}=N_{i}\mid i\in
I\rangle})\\\\[2.84526pt]
\text{Mixin:}&M&::=&\lambda\,\textsf{argClass}.\,\mathbf{Y}(\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,(\textsf{argClass}\;\textsf{state})\,\oplus\,{\langle
l_{i}=N_{i}\mid i\in I\rangle})\\\\[2.84526pt] \end{array}$

We define ${\mathcal{C}}$ and ${\mathcal{M}}$ as the sets of classes and
mixins respectively.

To illustrate this definition let us use the abbreviation $\texttt{let
}x=N\texttt{ in }M$ for $M\\{N/x\\}$. Then a class combinator
$C\in{\mathcal{C}}$ can be written in a more perspicuous way as follows:

$C\equiv\mathbf{Y}(\lambda\,\textsf{myClass}\ \lambda\,\textsf{state}.\
\texttt{let }\textsf{self}=(\textsf{myClass}\;\textsf{state})\texttt{ in
}{\langle l_{i}=N_{i}\mid i\in I\rangle}).$ (3)

A class is the fixed point of a function, the class definition, mapping a
recursive definition of the class itself and a state $S$, that is the value or
a record of values in general, for the instance variables of the class, into a
record ${\langle l_{i}=N_{i}\mid i\in I\rangle}$ of methods. A class $C$ is
instantiated to an object $O\equiv C\,S$ by applying the class $C$ to a state
$S$. Hence we have:

$O\equiv C\,S\longrightarrow^{*}\texttt{let }\textsf{self}=(C\,S)\texttt{ in
}{\langle l_{i}=N_{i}\mid i\in I\rangle},$

where the variable self is used in the method bodies $N_{i}$ to call other
methods from the same object. Note that the recursive parameter myClass might
occur in the $N_{i}$ in subterms other than
$(\textsf{myClass}\;\textsf{state})$, and in particular
$N_{i}\\{C/\textsf{myClass}\\}$ might contain a subterm $C\,S^{\prime}$, where
$S^{\prime}$ is a state possibly different than $S$; even $C$ itself might be
returned as the value of a method. Classes are the same as in [CHC90] §4, but
for the explicit identification of self with
$(\textsf{myClass}\;\textsf{state})$.

We come now to typing of classes. Let $R={\langle l_{i}=N_{i}\mid i\in
I\rangle}$, and suppose that $C\equiv\mathbf{Y}(\lambda\,\textsf{myClass}\
\lambda\,\textsf{state}.\,R)\in{\mathcal{C}}$. To type $C$ we must find a type
$\sigma$ (a type of its state) and a sequence of types
$\rho_{1},\ldots,\rho_{n}\in\mathbb{T}_{{\langle\rangle}}$ such that for all
$0<i<n$:

$\textsf{myClass}:\sigma\to\rho_{i},\textsf{state}:\sigma\vdash R:\rho_{i+1}.$

Note that this is always possible for any $n$: in the worst case, we can take
$\rho_{i}={\langle l_{i}:\omega\mid i\in I\rangle}$ for all $0<i\leq n$. In
general one has more expressive types, depending on the typings of the $N_{i}$
in $R$ (see example 3.2 below). It follows that:

$\vdash\lambda\,\textsf{myClass}\
\lambda\,\textsf{state}.\,R:(\omega\to(\sigma\to\rho_{1}))\cap\bigcap_{i=1}^{n-1}((\sigma\to\rho_{i})\to(\sigma\to\rho_{i+1})),$

and therefore, by using the fact that
$\vdash\mathbf{Y}:(\omega\to\tau_{1})\cap\cdots\cap(\tau_{n-1}\to\tau_{n})\to\tau_{n}$
for arbitrary types $\tau_{1},\ldots,\tau_{n}$ (see e.g. [BDS13], p. 586), we
conclude that the typing of classes has the following shape (where
$\rho=\rho_{n}$):

$\vdash C\equiv\mathbf{Y}(\lambda\,\textsf{myClass}\
\lambda\,\textsf{state}.\,{\langle l_{i}=N_{i}\mid i\in
I\rangle}):\sigma\to\rho$ (4)

In conclusion the type of a class $C$ is the arrow from the type of the state
$\sigma$ to a type $\rho$ of its instances.

The class Num has a method get returning the current state and a method succ
returning the state of the instance object incremented by one. Beside there is
a third method set whose body is the identity function:

$\displaystyle\text{Num}=\mathbf{Y}(\lambda\textsf{myClass}.\lambda\textsf{state}.$
$\displaystyle\qquad\texttt{let }\textsf{self}=\textsf{myClass}\
\textsf{state}\texttt{ in }$
$\displaystyle\qquad\qquad{\langle\textit{get}=\textsf{state},\textit{set}=\lambda\textsf{state}^{\prime}.\textsf{state}^{\prime},\textit{succ}=\textsf{self}.\textit{set}(\textsf{self}.\textit{get}+1)\rangle}$

There are several ways in which functional state update can be implemented.
One possibility for a method to update the current state of the object
functionally is to return an updated instance of the object. As will become
clear later on, in the context of mixin applications it is unclear whether the
updated object has to be an instance of the early-bound inner class (Num in
the above example) or an instance of the class modified by mixin applications.
The former option loses information whenever an object that is an instance of
a class modified by mixin applications is updated. The latter option breaks
compatibility whenever a mixin incompatibly overwrites a method using record
merge, which will be discussed later on. In conclusion, the decision regarding
the instantiation of the updated object cannot be made a-priori, but depends
on the context in which the method that updates the object is called. Since in
the functional setting two object instances of one class are distinguished
only by the underlying state, a method, such as set, that modifies the
underlying object state returns the updated state and leaves instantiation to
the caller.

To Type Num, let us call

$R\equiv{\langle\textit{get}=\textsf{state},\textit{set}=\lambda\textsf{state}^{\prime}.\textsf{state}^{\prime},\textit{succ}=\textsf{self}.\textit{set}(\textsf{self}.\textit{get}+1)\rangle}$

where $\textsf{self}\equiv(\textsf{myClass}\ \textsf{state})$. Now we can
deduce:

$\textsf{myClass}:\omega,\textsf{state}:\text{Int}\vdash
R:{\langle\textit{get}:\text{Int},\textit{set}:\text{Int}\to\text{Int},\textit{succ}:\omega\rangle}=\rho_{1}.$

since
$\textsf{myClass}:\text{Int}\to\omega,\textsf{state}:\text{Int}\vdash\textsf{myClass}\
\textsf{state}:\omega$ and therefore
$\textsf{self}.\textit{set}(\textsf{self}.\textit{get}+1)$ is just typable by
$\omega$; on the other hand the type of set is any type of the identity, so
that $\text{Int}\to\text{Int}$ is a possibility.

Given $\rho_{1}$ we consider the new assumption
$\textsf{myClass}:\text{Int}\to\rho_{1}$ by which we obtain the typing
$\textsf{self}\equiv\textsf{myClass}\ \textsf{state}:\rho_{1}$ that is enough
to get $\textsf{self}.\textit{set}(\textsf{self}.\textit{get}+1):\text{Int}$
and hence:

$\textsf{myClass}:\text{Int}\to\rho_{1},\textsf{state}:\text{Int}\vdash
R:{\langle\textit{get}:\text{Int},\textit{set}:\text{Int}\to\text{Int},\textit{succ}:\text{Int}\rangle}=\rho_{2}.$

Eventually by (4) we conclude that $\text{Num}:\text{Int}\to\rho_{2}$.

In case of Num we have reached the type $\rho_{2}$ that doesn’t contain any
occurrence of $\omega$ in a finite number of steps. This is because method
succ of class Num returns a number; let us consider a variant
$\text{Num}^{\prime}$ of Num having a method succ that returns a new instance
of the class, whose state has been incremented:

$\displaystyle\text{Num}^{\prime}=\mathbf{Y}(\lambda\textsf{myClass}.\lambda\textsf{state}.$
$\displaystyle\qquad\texttt{let }\textsf{self}=\textsf{myClass}\
\textsf{state}\texttt{ in }$
$\displaystyle\qquad\qquad{\langle\textit{get}=\textsf{state},\textit{succ}=\textsf{myClass}(\textsf{self}.\textit{get}+1)\rangle}$

Let us call
$R^{\prime}\equiv{\langle\textit{get}=\textsf{state},\textit{succ}=\textsf{myClass}(\textsf{self}.\textit{get}+1)\rangle}$,
where $\textsf{self}\equiv(\textsf{myClass}\ \textsf{state})$ as above. Then

$\textsf{myClass}:\text{Int}\to\omega,\textsf{state}:\text{Int}\vdash
R^{\prime}:{\langle\textit{get}:\text{Int},\textit{succ}:\omega\rangle}=\rho^{\prime}_{1}.$

By assuming $\textsf{myClass}:\text{Int}\to\rho^{\prime}_{1}$ and
$\textsf{state}:\text{Int}$, we have that $\textsf{self}:\rho^{\prime}_{1}$
and hence $\textsf{self}.\textit{get}:\text{Int}$. It follows that
$\textsf{myClass}(\textsf{self}.\textit{get}+1):\rho^{\prime}_{1}$ so that

$\textsf{myClass}:\text{Int}\to\rho^{\prime}_{1},\textsf{state}:\text{Int}\vdash
R^{\prime}:{\langle\textit{get}:\text{Int},\textit{succ}:\rho^{\prime}_{1}\rangle}=\rho^{\prime}_{2}.$

In general, putting $\rho^{\prime}_{0}=\omega$ and
$\rho^{\prime}_{i+1}={\langle\textit{get}:\text{Int},\textit{succ}:\rho^{\prime}_{i}\rangle}$
we have for all $i$:

$\textsf{myClass}:\text{Int}\to\rho^{\prime}_{i},\textsf{state}:\text{Int}\vdash
R^{\prime}:{\langle\textit{get}:\text{Int},\textit{succ}:\rho^{\prime}_{i}\rangle}=\rho^{\prime}_{i+1}.$

From this by (4) we conclude that
$\text{Num}^{\prime}:\text{Int}\to\rho^{\prime}_{i}$ for all $i$. We note that
this time, differently than in case of Num, we cannot get rid of occurrences
$\omega$ in the $\rho^{\prime}_{i}$.

A variant of this typing uses the type constants Odd and Even called semantic
types in [Reh13] where they are used in the intersection types
$\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}$
or
$\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}$
(see also below Section 5.3). Let us suppose that we have axioms
$x:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\vdash
x+1:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}$
and
$x:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\vdash
x+1:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}$
added to the typing system. Then a more interesting type for
$\text{Num}^{\prime}$ is

$\displaystyle\text{Num}^{\prime}:\quad$
$\displaystyle(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\langle\textit{get}:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}},\textit{succ}:{\langle\textit{get}:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\rangle}\rangle})~{}\cap$
$\displaystyle(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\langle\textit{get}:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}},\textit{succ}:{\langle\textit{get}:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\rangle}\rangle}).$

Although $\text{Num}^{\prime}$ is closer to what is done with object-oriented
programming, in the context of mixin application, introduced in the remainder
of this section, we shall not consider this kind of recursive definition in
this work, as previously explained.

A mixin $M\in{\mathcal{M}}$ is a combinator such that, if $C\in{\mathcal{C}}$
then $M\,C$ reduces to a new class $C^{\prime}\in{\mathcal{C}}$. Writing $M$
in a more explicit way we obtain:

$\displaystyle
M\equiv\lambda\,\textsf{argClass}.\,\mathbf{Y}(\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,$
$\displaystyle\texttt{let
}\textsf{super}=(\textsf{argClass}\;\textsf{state})\texttt{ in }$
$\displaystyle\texttt{let
}\textsf{self}=(\textsf{myClass}\;\textsf{state})\texttt{ in }$
$\displaystyle\textsf{super}\,\oplus\,{\langle l_{i}=N_{i}\mid i\in
I\rangle})$

In words, a mixin merges an instance $C\,S$ of the input class $C$ with a new
state $S$ together with a difference record $R\equiv{\langle l_{i}=N_{i}\mid
i\in I\rangle}$, that would be written $\Delta(C\,S)$ in terms of [BC90]. Note
that our mixins are not the same as class modificators (also called wrappers
e.g. in [Bra92]). Wrappers bind super to the unmodified class definition
applied to self _without_ taking the fixed point. In our case, super is simply
an instance of the unmodified class. The effect is that we have a static (or
early) binding instead of dynamic (or late) binding of self.

Let
$M\equiv\lambda\,\textsf{argClass}.\,\mathbf{Y}(\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,(\textsf{argClass}\;\textsf{state})\,\oplus\,R)\in{\mathcal{M}}$;
to type $M$ we have to find types $\sigma^{1},\sigma^{2},\rho^{1}$ and a
sequence $\rho^{2}_{1},\ldots,\rho^{2}_{n}\in\mathbb{T}_{{\langle\rangle}}$ of
record types such that for all $1\leq i<n$ it is true that $\mbox{\it
lbl}(R)=\mbox{\it lbl}(\rho^{2}_{i})$ and setting

$\displaystyle\Gamma_{0}$
$\displaystyle=\\{\textsf{argClass}:\sigma^{1}\to\rho^{1},\textsf{myClass}:\omega,\textsf{state}:\sigma^{1}\cap\sigma^{2}\\}$
$\displaystyle\Gamma_{i}$
$\displaystyle=\\{\textsf{argClass}:\sigma^{1}\to\rho^{1},\textsf{myClass}:(\sigma^{1}\cap\sigma^{2})\to\rho^{1}+\rho_{i}^{2},\textsf{state}:\sigma^{1}\cap\sigma^{2}\\}\text{
for all }1\leq i<n$

we may deduce for all $0\leq i<n$:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Gamma_{i}\vdash\textsf{state}:\sigma^{1}\cap\sigma^{2}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.92972pt\hbox{\kern
3.00003pt$(\leq)$}}}\hbox{\kern
8.70149pt\hbox{$\displaystyle\Gamma_{i}\vdash\textsf{state}:\sigma^{1}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=116.70415pt\hbox{\kern
3.00003pt$(\rightarrow\mbox{\it E})$}}}\hbox{\kern
14.06903pt\hbox{$\displaystyle\Gamma_{i}\vdash\textsf{argClass}\;\textsf{state}:\rho^{1}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\qquad\Gamma_{i}\vdash
R:\rho_{i+1}^{2}\qquad\mbox{\it lbl}(R)=\mbox{\it lbl}(\rho^{2}_{i+1})$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=321.8066pt\hbox{\kern
3.00003pt$(+)$}}}\hbox{\kern
86.2134pt\hbox{$\displaystyle\Gamma_{i}\vdash(\textsf{argClass}\;\textsf{state})\,\oplus\,R:\rho^{1}+\rho_{i+1}^{2}$}}}}$

Hence for all $0\leq i<n$ we can derive the typing judgment:

$\displaystyle\textsf{argClass}:\sigma^{1}\to\rho^{1}\vdash\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,(\textsf{argClass}\;\textsf{state})\,\oplus\,R:$
$\displaystyle\hskip
128.0374pt((\sigma^{1}\cap\sigma^{2})\to(\rho^{1}+\rho_{i}^{2}))\to(\sigma^{1}\cap\sigma^{2})\to(\rho^{1}+\rho_{i+1}^{2})$

and therefore, by reasoning as for classes, we get (setting
$\rho^{2}=\rho_{n}^{2}$):

$\vdash
M\equiv\lambda\,\textsf{argClass}.\,\mathbf{Y}(\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,(\textsf{argClass}\;\textsf{state})\,\oplus\,R):\\\
(\sigma^{1}\to\rho^{1})\to(\sigma^{1}\cap\sigma^{2})\to(\rho^{1}+\rho^{2})$
(5)

Spelling out this type, we can say that $\sigma^{1}$ is a type of the state of
the argument-class of $M$; $\sigma^{1}\cap\sigma^{2}$ is the type of the state
of the resulting class, that refines $\sigma^{1}$. Type $\rho^{1}$ expresses
the requirements of $M$ about the methods of the argument-class, i.e. what is
assumed to hold for the usages of super and argClass in $R$ to be properly
typed; $\rho^{1}+\rho^{2}$ is a type of the record of methods of the refined
class, resulting from the merge of the methods of the argument-class with
those of the difference $R$; since in general there will be overridden
methods, whose types might be incompatible, the $+$ type constructor cannot be
replaced by intersection. On the other hand, $M$ preserves typings of any
label that is not in $R$.

######  Lemma 12.

For any $\sigma$ and $\rho={\langle l:\tau\rangle}$ such that
$l\not\in\mbox{\it lbl}(R)$ we have

$\vdash
M\equiv\lambda\,\textsf{argClass}.\,\mathbf{Y}(\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,(\textsf{argClass}\;\textsf{state})\,\oplus\,R):(\sigma\to\rho)\to(\sigma\to\rho)$

######  Proof 3.8.

Let $\\{l_{1},\ldots,l_{n}\\}=\mbox{\it lbl}(R)$. We have $\vdash R:{\langle
l_{1}:\omega,\ldots,l_{n}:\omega\rangle}$. Since $l\not\in\mbox{\it lbl}(R)$
we obtain $\rho+{\langle l_{1}:\omega,\ldots,l_{n}:\omega\rangle}={\langle
l:\tau,l_{1}:\omega,\ldots,l_{n}:\omega\rangle}\leq\rho$. Using the above
general type derivation with $\sigma^{1}=\sigma^{2}=\sigma$, $\rho^{1}=\rho$,
$\rho^{2}={\langle l_{1}:\omega,\ldots,l_{n}:\omega\rangle}$ and
$\vdash\mathbf{Y}:(\omega\to(\sigma\to\rho))\to(\sigma\to\rho)$ we obtain
$\vdash
M:(\sigma\to\rho)\to(\sigma\to\rho+\rho^{2})\leq(\sigma\to\rho)\to(\sigma\to\rho)$.

Let us consider the mixin Comparable adding a method compare to its argument
class, which is supposed to have a method get:

$\displaystyle\text{Comparable}=\lambda\textsf{argClass}.\mathbf{Y}(\lambda\textsf{myClass}.\lambda\textsf{state}.$
$\displaystyle\qquad\texttt{let }\textsf{super}=\textsf{argClass}\
\textsf{state}\texttt{ in }$ $\displaystyle\qquad\texttt{let
}\textsf{self}=\textsf{myClass}\ \textsf{state}\texttt{ in }$
$\displaystyle\qquad\qquad\textsf{super}\oplus{\langle\textit{compare}=\lambda
o.(o.\textit{get}==\textsf{self}.\textit{get})\rangle})$

We write $==$ for a suitable equality operator, which is distinct from the
symbol $=$ used in our calculus to associate labels to their values in a
record.

For the sake of readability, we take the types $\sigma^{1}$ and $\sigma^{2}$
of the respective states of the argument class and the resulting class to be
just Int and simply write Int for $\text{Int}\cap\text{Int}$ which is the type
we assume for state. If we set

$\Gamma_{0}=\\{\textsf{argClass}:\text{Int}\to{\langle\textit{get}:\text{Int}\rangle},\textsf{myClass}:\text{Int}\to\omega,\textsf{state}:\text{Int}\\}$

we have
$\Gamma_{0}\vdash\textsf{super}:{\langle\textit{get}:\text{Int}\rangle}$ but
$\Gamma_{0}\vdash\textsf{self}:\omega$ so that $\Gamma_{0}\vdash\lambda
o.(o.\textit{get}==\textsf{self}.\textit{get}):\tau\to\omega$ for any type
$\tau$ given to $o$; but $\tau\to\omega=\omega$ by Definition 3.1, so that we
conclude

$\Gamma_{0}\vdash\textsf{super}\oplus{\langle\textit{compare}=\lambda
o.(o.\textit{get}==\textsf{self}.\textit{get})\rangle}:{\langle\textit{get}:\text{Int}\rangle}+{\langle\textit{compare}:\omega\rangle}.$

Now, taking

$\Gamma_{1}=\\{\textsf{argClass}:\text{Int}\to{\langle\textit{get}:\text{Int}\rangle},\textsf{myClass}:\text{Int}\to{\langle\textit{get}:\text{Int}\rangle}+{\langle\textit{compare}:\omega\rangle},\textsf{state}:\text{Int}\\}$

and using the fact that
${\langle\textit{get}:\text{Int}\rangle}+{\langle\textit{compare}:\omega\rangle}={\langle\textit{get}:\text{Int}\rangle}\cap{\langle\textit{compare}:\omega\rangle}\leq{\langle\textit{get}:\text{Int}\rangle}$
we have
$\Gamma_{1}\vdash\textsf{self}:{\langle\textit{get}:\text{Int}\rangle}$, that
implies $\Gamma_{1}\vdash\textsf{self}.\textit{get}:\text{Int}$ and therefore
$\Gamma_{1}\vdash\lambda
o.(o.\textit{get}==\textsf{self}.\textit{get}):{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool}$.
By (5) we conclude that Comparable has type

$(\text{Int}\to{\langle\textit{get}:\text{Int}\rangle})\to\text{Int}\to{\langle\textit{get}:\text{Int}\rangle}+{\langle\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool}\rangle}.$

We finally observe that if the argument class $C$ has type
$\text{Int}\to{\langle\textit{get}:\text{Int},\textit{compare}:\tau\rangle}$
for some type $\tau$, then we have that
$\text{Int}\to{\langle\textit{get}:\text{Int},\textit{compare}:\tau\rangle}\leq\text{Int}\to{\langle\textit{get}:\text{Int}\rangle}$,
so that the class $C^{\prime}\equiv\text{Comparable}\,C$ has the correct type
$\text{Int}\to{\langle\textit{get}:\text{Int}\rangle}+{\langle\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool}\rangle}$
as the method $\textsf{super}.\textit{compare}$ is overridden in
$\textsf{super}\oplus{\langle\textit{compare}=\lambda
o.(o.\textit{get}==\textsf{self}.\textit{get})\rangle}$. This is because, even
by keeping the typing
$\textsf{super}:{\langle\textit{get}:\text{Int},\textit{compare}:\tau\rangle}$
through the derivation, we obtain that
$\textsf{super}\oplus{\langle\textit{compare}=\lambda
o.(o.\textit{get}==\textsf{self}.\textit{get})\rangle}$ has type

${\langle\textit{get}:\text{Int},\textit{compare}:\tau\rangle}+{\langle\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool}\rangle}={\langle\textit{get}:\text{Int},\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool}\rangle}$

which is the same as
${\langle\textit{get}:\text{Int}\rangle}+{\langle\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool}\rangle}$.
For a more general typing of Comparable see Appendix B.

##  4\. Bounded Combinatory Logic

Our main goal is synthesize meaningful mixin compositions. For this purpose,
we use the logical programming language given by inhabitation in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ (bounded combinatory logic with
constructors). Conveniently, necessary type information can be inferred from
intersection types for $\Lambda_{R}$.
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ is an extension of bounded
combinatory logic $\textsf{BCL}_{k}(\to,\cap)$ [DMRU12] by covariant
constructors. Constructors can be utilized to encode record types and useful
features of $+$ while extending the existing synthesis framework (CL)S
[BDD+14]. In this section, we present
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ along with its fundamental
properties, in particular decidability of inhabitation.

###  4.1. $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$

_Combinatory terms_ are formed by application of combinators from a
_repository_ (combinatory logic context) $\Delta$. [Combinatory Term]
$E,E^{\prime}::=C\;|\;(E\;E^{\prime})\quad\text{ where }C\in\textrm{\it
dom}(\Delta)$ We create repositories of typed combinators that can be
considered logic programs for the existing synthesis framework (CL)S [BDD+14]
to reason about semantics of such compositions. The underlying type system of
(CL)S is the intersection type system BCD [BCDC83], which we extend by
covariant constructors. The extended type system $\mathbb{T}_{\mathbb{C}}$,
while suited for synthesis, is flexible enough to encode record types and
features of $+$.

[Intersection Types with Constructors $\mathbb{T}_{\mathbb{C}}$] The set
$\mathbb{T}_{\mathbb{C}}$ is given by:

$\mathbb{T}_{\mathbb{C}}\ni\sigma,\tau,\tau_{1},\tau_{2}\
::=a\mid\alpha\mid\omega\mid\tau_{1}\rightarrow\tau_{2}\mid\tau_{1}\cap\tau_{2}\mid
c(\tau)$

where $a$ ranges over constants, $\alpha$ over type variables and $c$ over
unary constructors $\mathbb{C}$.

$\mathbb{T}_{\mathbb{C}}$ adds the following two subtyping axioms to the BCD
system (cf. Definition 3.1)

$\tau_{1}\leq\tau_{2}\Rightarrow c(\tau_{1})\leq c(\tau_{2})\qquad\quad
c(\tau_{1})\cap c(\tau_{2})\leq c(\tau_{1}\cap\tau_{2})$

The additional axioms ensure _constructor distributivity_ , i.e.,
$c(\tau_{1})\cap c(\tau_{2})=c(\tau_{1}\cap\tau_{2})$.

The notion of _level_ of a type is used as a bound to ensure decidability of
inhabitation, or equivalently termination of logic programs in (CL)S.

[Level] We define the _level_ of a type as follows:

$\displaystyle\operatorname{level}(\omega)=\operatorname{level}(a)=\operatorname{level}(\alpha)=0$
$\displaystyle\operatorname{level}(c(\tau))=1+\operatorname{level}(\tau)$
$\displaystyle\operatorname{level}(\sigma\to\tau)=1+\max(\operatorname{level}(\sigma),\operatorname{level}(\tau))$
$\displaystyle\operatorname{level}(\sigma\cap\tau)=\max(\operatorname{level}(\sigma),\operatorname{level}(\tau))$

We define the level of a substitution $S$ as
$\operatorname{level}(S)=\max\\{\operatorname{level}(S(\alpha))\mid\alpha\in\textrm{\it
dom}(S)\\}$.

[Type Assignment $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$]

$\begin{array}[]{ccc }{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1C:\tau\in\Delta\qquad\operatorname{level}(S)\leq k$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=113.90738pt\hbox{\kern
3.00003pt$(\text{Var})$}}}\hbox{\kern
29.2701pt\hbox{$\displaystyle\Delta\vdash_{k}C:S(\tau)$}}}}&\quad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Delta\vdash_{k}E:\sigma\to\tau\qquad\Delta\vdash_{k}E^{\prime}:\sigma$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=118.32826pt\hbox{\kern
3.00003pt$(\rightarrow\mbox{\it E})$}}}\hbox{\kern
35.31538pt\hbox{$\displaystyle\Delta\vdash_{k}EE^{\prime}:\tau$}}}\par}\\\ \\\
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Delta\vdash_{k}E:\sigma\quad\Delta\vdash_{k}E:\tau$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=93.2964pt\hbox{\kern
3.00003pt$(\cap)$}}}\hbox{\kern
17.74718pt\hbox{$\displaystyle\Delta\vdash_{k}E:\sigma\cap\tau$}}}}&\quad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Delta\vdash_{k}E:\sigma\qquad\sigma\leq\tau$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=85.7384pt\hbox{\kern
3.00003pt$(\leq)$}}}\hbox{\kern
22.38075pt\hbox{$\displaystyle\Delta\vdash_{k}E:\tau$}}}}\end{array}$

For a set of typed combinators $\Delta$ and a type
$\tau\in\mathbb{T}_{\mathbb{C}}$ we say $\tau$ is inhabited in $\Delta$, if
there exists a combinatory term $E$ and a $k\in\mathbb{N}$ such that
$\Delta\vdash_{k}E:\tau$.

###  4.2. $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ Inhabitation

In this section we extend the understanding of $\textsf{BCL}(\to,\cap)$
inhabitation [DMRU12] to constructors. First, we extend the necessary notions
of _paths_ and _organized types_ to constructors in the following way.

[Path] A _path_ $\pi$ is a type of the form:
$\pi::=a\mid\alpha\mid\sigma\to\pi\mid c(\omega)\mid c(\pi)$, where $\alpha$
is a variable, $\tau$ is a type, $c$ is a constructor and $a$ is a constant.

[Paths in $\tau$] Given a type $\tau\in\mathbb{T}_{\mathbb{C}}$, the set
$\mathbb{P}(\tau)$ of paths in $\tau$ is defined as

$\displaystyle\mathbb{P}(a)=\\{a\\}$
$\displaystyle\mathbb{P}(\sigma\to\tau)=\\{\sigma\to\pi\mid\pi\in\mathbb{P}(\tau)\\}$
$\displaystyle\mathbb{P}(\alpha)=\\{\alpha\\}$
$\displaystyle\mathbb{P}(\sigma\cap\tau)=\mathbb{P}(\sigma)\cup\mathbb{P}(\tau)$
$\displaystyle\mathbb{P}(\omega)=\emptyset$
$\displaystyle\mathbb{P}(c(\tau))=\begin{cases}\\{c(\omega)\\}&\text{if
}\mathbb{P}(\tau)=\emptyset\\\
\\{c(\pi)\mid\pi\in\mathbb{P}(\tau)\\}&\text{else}\end{cases}$

Observe that $\mathbb{P}(\tau)=\emptyset$ iff $\tau=\omega$.

[Organized Type] A type $\tau$ is called organized, if
$\tau\equiv\bigcap_{i\in I}\pi_{i}$, where $\pi_{i}$ for $i\in I$ are paths.

For brevity, we sometimes write $\bigcap\mathbb{P}(\tau)$ for
$\pi_{1}\cap\ldots\cap\pi_{n}$ where
$\mathbb{P}(\tau)=\\{\pi_{1},\ldots,\pi_{n}\\}$. If
$\mathbb{P}(\tau)=\emptyset$, then we set
$\bigcap\mathbb{P}(\tau)\equiv\omega$.

######  Lemma 13.

Given a type $\tau\in\mathbb{T}_{\mathbb{C}}$, the type
$\bigcap\mathbb{P}(\tau)$ is organized with $\bigcap\mathbb{P}(\tau)=\tau$.

The detailed proof by induction of Lemma 13 is in the appendix.

######  Lemma 14.

Given a type $\tau\in\mathbb{T}_{\mathbb{C}}$ we have
$|\bigcap\mathbb{P}(\tau)|\leq|\tau|^{2}$, where $|\cdot|$ denotes the number
of nodes in the syntax tree of a given type.

By induction using Definition 4.2 we have $|\mathbb{P}(\tau)|\leq|\tau|$. The
only non-trivial cases for the inductive proof of the main statement are
(assuming $\mathbb{P}(\tau)\neq\emptyset$)

$\displaystyle|\bigcap\mathbb{P}(c(\tau))|$
$\displaystyle=\sum\limits_{\pi\in\mathbb{P}(\tau)}(|\pi|+2)-1=|\mathbb{P}(\tau)|+|\bigcap\mathbb{P}(\tau)|\leq|\tau|+|\tau|^{2}\leq|c(\tau)|^{2}$
$\displaystyle|\bigcap\mathbb{P}(\sigma\to\tau)|$
$\displaystyle=\sum\limits_{\pi\in\mathbb{P}(\tau)}(|\sigma|+|\pi|+2)-1=(|\sigma|+1)\cdot|\mathbb{P}(\tau)|+|\bigcap\mathbb{P}(\tau)|\leq|\sigma\to\tau|^{2}$

Due to Lemma 14, for any intersection type there exists an equivalent
organized intersection type computable in polynomial time. Note that organized
types are not necessarily normalized [Hin82] or strict [Bak11]. However,
organized types have the following property known from normalized types.

######  Lemma 15.

Given two types $\sigma,\tau\in\mathbb{T}_{\mathbb{C}}$, we have
$\sigma\leq\tau$ iff for each path $\pi\in\mathbb{P}(\tau)$ there exists a
path $\pi^{\prime}\in\mathbb{P}(\sigma)$ such that $\pi^{\prime}\leq\pi$ and

  * •

If $\pi\equiv\alpha$ (resp. $a$), then $\pi^{\prime}\equiv\alpha$ (resp. $a$).

  * •

If $\pi\equiv\sigma_{2}\to\tau_{2}$, then
$\pi^{\prime}\equiv\sigma_{1}\to\tau_{1}$ such that $\sigma_{2}\leq\sigma_{1}$
and $\tau_{1}\leq\tau_{2}$.

  * •

If $\pi\equiv c(\tau_{1})$, then $\pi^{\prime}\equiv c(\sigma_{1})$ such that
$\sigma_{1}\leq\tau_{1}$.

The detailed proof by induction of Lemma 15 is in the appendix.

We say a path $\pi$ has the _arity_ of at least $m$ if
$\pi\equiv\sigma_{1}\to\ldots\to\sigma_{m}\to\tau$ for some
$\sigma_{1},\ldots\sigma_{m},\tau\in\mathbb{T}_{\mathbb{C}}$. Additionally,
for such a path $\pi$ we define $\arg_{i}(\pi)=\sigma_{i}$ for $1\leq i\leq m$
and $\operatorname{tgt}_{m}(\pi)=\tau$. We define $\mathbb{P}_{m}(\tau)$ as
the set of paths in $\tau$ having arities of at least $m$.

$\textsf{BCL}_{k}(\to,\cap)$ inhabitation is $(k+2)$-ExpTime complete
[DMRU12]. The upper bound is derived by constructing an alternating Turing
machine based on the _path lemma_ [DMRU12, Lemma 11]. Accordingly, we
formulate a path lemma for $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$. Let
$\operatorname{atoms}(\tau)$ be the set of constants, variables and
constructor names occurring in $\tau$. Additionally, for a substitution $S$
let
$\operatorname{atoms}(S)=\bigcup\\{\operatorname{atoms}(S(\alpha))\mid\alpha\in\textrm{\it
dom}(S)\\}$, and for a repository $\Delta$ let
$\operatorname{atoms}(\Delta)=\bigcup\\{\operatorname{atoms}(\tau)\mid
C:\tau\in\Delta\\}$.

######  Lemma 16 (Path Lemma for $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$).

The following are equivalent conditions:

  1. (1)

$\Delta\vdash_{k}C\,E_{1}\,\ldots E_{m}:\tau$

  2. (2)

There exists a set of paths
$P\subseteq\mathbb{P}_{m}(\bigcap\\{S(\Delta(C))\mid\operatorname{level}(S)\leq
k,\operatorname{atoms}(S)\subseteq\operatorname{atoms}(\Delta)\cup\operatorname{atoms}(\tau)\\})$
such that

    1. (a)

$\bigcap_{\pi\in P}\operatorname{tgt}_{m}(\pi)\leq\tau$

    2. (b)

$\Delta\vdash_{k}E_{i}:\bigcap_{\pi\in P}\arg_{i}(\pi)$ for $1\leq i\leq m$

The detailed proof of Lemma 16, which is a slight extension of [DMRU12, Lemma
11], is in the appendix.

In the above Lemma 16 we can bound the size of the set $P$ of paths of level
at most $k$. Let $\exp_{k}$ be the iterated exponential function, i.e.
$\exp_{0}(n)=n$ and $\exp_{k+1}(n)=2^{\exp_{k}(n)}$.

######  Lemma 17.

There exists a polynomial $p$ such that (modulo $=$) for any $k\in\mathbb{N}$
the number of level-$k$ types over $n$ atoms is at most $\exp_{k+1}(p(n))$,
and the size of such types is at most $\exp_{k}(p(n))$.

######  Proof 4.1.

Since normalizing (i.e. recursively organizing) a type does not increase its
level, we only need to consider normalized types. Fix the set of atoms
$\mathbb{A}$ with $|\mathbb{A}|=n$. Let $\mathbb{P}^{k}$ denote the set of
paths of level at most $k$, and $\mathbb{T}^{k}$ the set of normalized types
of level at most $k$. We have

$\displaystyle|\mathbb{A}|=n\leq n|\mathbb{T}^{k}|^{2}\text{ and }$
$\displaystyle|\\{\sigma\to\pi\mid\sigma\in\mathbb{T}^{k},\pi\in\mathbb{P}^{k}\\}|\leq|\mathbb{T}^{k}|\cdot|\mathbb{P}^{k}|\leq
n|\mathbb{T}^{k}|^{2}\text{ and }$ $\displaystyle|\\{c(\pi)\mid
c\in\mathbb{A},\pi\in\mathbb{P}^{k}\\}|\leq|\mathbb{A}|\cdot|\mathbb{P}^{k}|\text{
therefore }$
$\displaystyle|\mathbb{P}^{k+1}|\leq|\mathbb{A}|+|\\{\sigma\to\pi\mid\sigma\in\mathbb{T}^{k},\pi\in\mathbb{P}^{k}\\}|+|\\{c(\pi)\mid
c\in\mathbb{A},\pi\in\mathbb{P}^{k}\\}|\leq 3n|\mathbb{T}^{k}|^{2}\text{ and
}$ $\displaystyle|\mathbb{T}^{k+1}|\leq|\\{\bigcap P\mid
P\subseteq\mathbb{P}^{k+1}\\}|\leq 2^{3n|\mathbb{T}^{k}|^{2}}$

By induction on $k$ we have that there exists a polynomial $p$ such that

$|\mathbb{T}^{k}|\leq\exp_{k+1}(p(n)+\sum\limits_{i=0}^{k-1}\frac{p(n)}{2^{i}})\leq\exp_{k+1}(3p(n))$

Let $s_{k}$ be the maximal size of a type of level $k$ with atoms in
$\mathbb{A}$. We have

$s_{k+1}\leq|\mathbb{P}^{k+1}|\cdot(2s_{k}+2)\leq
3n|\mathbb{T}^{k}|^{2}\cdot(2s_{k}+2)$

By induction on $k$ we have that there exists a polynomial $p$ such that
$s_{k}\leq\exp_{k}(p(n))$.

For the interested reader, only the rank of a given type influences the height
of the exponentiation tower.

Using Lemma 16 we can decide $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$
inhabitation by the alternating Turing machine shown in Figure 1.

Figure 1. Alternating Turing machine deciding inhabitation in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$
$\begin{array}[]{ll}&\mathit{Input}:\ \ \Delta,\tau,k\\\ &\mathit{loop:}\\\
1&\mbox{\sc choose}\ (C:\sigma)\in\Delta\\\
2&\sigma^{\prime}:=\bigcap\\{S(\sigma)\mid\operatorname{level}(S)\leq
k,\operatorname{atoms}(S)\subseteq\operatorname{atoms}(\Delta)\cup\operatorname{atoms}(\tau)\\}\\\
3&\mbox{\sc choose}\ m\in\\{0,\ldots,\text{maximal arity of paths in
}\sigma^{\prime}\\}\\\ 4&\mbox{\sc choose}\
P\subseteq\mathbb{P}_{m}(\sigma^{\prime})\\\ &\\\ 5&\mbox{\sc if}\
(\bigcap_{\pi\in P}\mathit{tgt}_{m}(\pi)\leq\tau)\ \mbox{\sc then}\\\ 6&\ \
\mbox{\sc if }(m=0)\mbox{ {\sc then accept}}\\\ 7&\ \ \mbox{{\sc else} }\\\
8&\ \ \ \ \mbox{\sc forall}(i=1\ldots m)\\\ 9&\ \ \ \ \ \
\tau:=\bigcap_{\pi\in P}\mathit{arg}_{i}(\pi)\\\ 10&\ \ \ \ \ \ \mbox{\sc goto
}\mathit{loop}\\\ \end{array}$

######  Theorem 18.

$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ inhabitation in $(k+2)$-ExpTime.

######  Proof 4.2.

The alternating Turing machine in Figure 1 directly implements Lemma 16 and is
therefore sound and complete. To show that the machine operates in alternating
$(k+1)$-ExpSpace, we need to bound the size of (organized) $\sigma^{\prime}$,
which is $(n\cdot\exp_{k+1}(p(n))\cdot\exp_{k}(p(n)))^{2}$ due to Lemmas 17
and 14. By the identity ASpace$(f(n))$ $=$ DTime$(2^{\mathcal{O}(f(n))})$
[CKS81], $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ inhabitation is in
$(k+2)$-ExpTime.

##  5\. Mixin Composition Synthesis by Type Inhabitation

In this section, we present an encoding of record types by
$\mathbb{T}_{\mathbb{C}}$ types that capture mixin semantics. We use the
encoding to define a repository of typed combinators from classes and mixins
that can be used to synthesize meaningful mixin compositions by means of
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ inhabitation. In the following we
fix a finite set of labels $\mathcal{L}\subseteq\mbox{\bf Label}$ that are
used in the particular domain of interest for mixin composition synthesis.

###  5.1. Records as Unary Covariant Distributing Constructors

First, we need to encode record types as $\mathbb{T}_{\mathbb{C}}$ types. We
define constructors ${\llangle\cdot\rrangle}$ and $l(\cdot)$ for
$l\in\mathcal{L}$ to represent record types using the following partial
translation function
${\llbracket\cdot\rrbracket}\colon\mathbb{T}\to\mathbb{T}_{\mathbb{C}}$ as
follows:

$\displaystyle{\llbracket\omega\rrbracket}$ $\displaystyle=\omega$
$\displaystyle{\llbracket a\rrbracket}$ $\displaystyle=a$
$\displaystyle{\llbracket\sigma\to\tau\rrbracket}$
$\displaystyle={\llbracket\sigma\rrbracket}\to{\llbracket\tau\rrbracket}$
$\displaystyle{\llbracket\sigma\cap\tau\rrbracket}$
$\displaystyle={\llbracket\sigma\rrbracket}\cap{\llbracket\tau\rrbracket}$
$\displaystyle{\llbracket{\langle l:\tau\rangle}\rrbracket}$
$\displaystyle={\llangle l({\llbracket\tau\rrbracket})\rrangle}$
$\displaystyle{\llbracket{\langle\rangle}\rrbracket}$
$\displaystyle={\llangle\omega\rrangle}$

By definition, we have ${\llbracket{\langle l_{i}:\tau_{i}\mid i\in
I\rangle}\rrbracket}={\llbracket\bigcap_{i\in I}{\langle
l_{i}:\tau_{i}\rangle}\rrbracket}=\bigcap_{i\in I}{\llangle
l_{i}({\llbracket\tau_{i}\rrbracket})\rrangle}$ if $I\neq\emptyset$.

######  Lemma 19.

For any $\sigma,\tau\in\mathbb{T}$ such that ${\llbracket\sigma\rrbracket}$
and ${\llbracket\tau\rrbracket}$ are defined we have $\sigma=\tau$ iff
${\llbracket\sigma\rrbracket}={\llbracket\tau\rrbracket}$.

######  Proof 5.1.

Routine induction on $\leq$ derivation observing that $\sigma,\tau$ do not
contain $+$, ${\llbracket\cdot\rrbracket}$ is homomorphic wrt. $\to$ and
$\cap$, and atomic records are covariant and distribute over $\cap$.

The translation function ${\llbracket\cdot\rrbracket}$ is not defined for
types containing $+$. Since $+$ has non-monotonic properties, it cannot be
immediately represented by a covariant type constructor. Simply applying Lemma
3.4 would require to consider all arguments a mixin could possibly be applied
to. Such an unwieldy specification would not be adequate for synthesis. There
are two possibilities to deal with this problem. The first option is extending
the type-system used for inhabitation. Here, the main difficulty is that
existing inhabitation algorithms rely on the separation of intersections into
paths [DMRU12]. As demonstrated in the remark accompanying Lemma 5, it becomes
unclear how to perform such a separation in the presence of the non-monotonic
$+$ operation. The second option, pursued in the rest of this section, is to
use the expressiveness of schematism provided by
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$. Specifically, encoding particular
$\mathbb{T}$ types containing $+$ that capture mixin semantics as
$\mathbb{T}_{\mathbb{C}}$ types suited for
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ inhabitation. Ultimately, we are
able to achieve completeness (cf. Theorem 23) wrt. particular mixin typings
(cf. Property $(\star)$) which restrict the general shape (5). This
restriction allows for a concise schematic mixin specification suited for
synthesis by $\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ inhabitation.

Let
$M\equiv\lambda\,\textsf{argClass}.\,\mathbf{Y}(\lambda\,\textsf{myClass}\,\lambda\,\textsf{state}.\,(\textsf{argClass}\;\textsf{state})\,\oplus\,R)\in{\mathcal{M}}$
be such that for some $\sigma,\rho_{1},\rho_{2}$, which do not contain $+$,
with $\mbox{\it lbl}(\rho_{2})=\mbox{\it lbl}(R)$ and all
$\rho\in\mathbb{T}_{{\langle\rangle}}$ we have

$\displaystyle\vdash M:(\sigma\to\rho\cap\rho_{1})\to(\sigma\to\rho+\rho_{2})$
($\star$)

We define the $\mathbb{T}_{\mathbb{C}}$ type

$\tau_{M}\equiv\big{(}({\llbracket\sigma\rrbracket}\to{\llbracket\rho_{1}\rrbracket})\to({\llbracket\sigma\rrbracket}\to{\llbracket\rho_{2}\rrbracket})\big{)}\cap\bigcap\limits_{l\in\mathcal{L}\setminus\mbox{\it
lbl}(R)}\big{(}({\llbracket\sigma\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\to({\llbracket\sigma\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\big{)}$

Note that $\tau_{M}$ contains only labels $l\in\mathcal{L}$ and type variables
$\alpha_{l}$ where $l\in\mathcal{L}$ because $\sigma,\rho_{1},\rho_{2}$ do not
contain type variables (cf. Definition 3.1).

######  Lemma 20 (Translation Soundness).

Assume $(\star)$.
For any substitution $S$ and type $\tau\in\mathbb{T}$ such that
${\llbracket\tau\rrbracket}=S(\tau_{M})$ we have $\vdash M:\tau$.

######  Proof 5.2.

We necessarily have
$S(\tau_{M})={\llbracket\big{(}(\sigma\to\rho_{1})\to(\sigma\to\rho_{2})\big{)}\cap\bigcap\limits_{l\in\mathcal{L}\setminus\mbox{\it
lbl}(R)}\big{(}(\sigma\to{\langle l:\tau_{l}\rangle})\to(\sigma\to{\langle
l:\tau_{l}\rangle})\big{)}\rrbracket}$ for some $\tau_{l}$ for
$l\in\mathcal{L}\setminus\mbox{\it lbl}(R)$. Due to $(\star)$ with
$\rho={\langle\rangle}$ we have $\vdash
M:(\sigma\to\rho_{1})\to(\sigma\to\rho_{2})$, and by Lemma 12 we have $\vdash
M:(\sigma\to{\langle l:\tau_{l}\rangle})\to(\sigma\to{\langle
l:\tau_{l}\rangle})$ for any $l\in\mathcal{L}\setminus\mbox{\it lbl}(R)$, thus
showing the claim.

Translation Soundness forces instantiations of $\tau_{M}$ to remain within
typings of $M$ in $\Lambda_{R}$. _Negative information_ , i.e. information
about labels absent in $R$, is encoded by explicitly capturing all positive
information, excluding labels in $\mbox{\it lbl}(R)$, in instances of

$\bigcap\limits_{l\in\mathcal{L}\setminus\mbox{\it
lbl}(R)}\big{(}({\llbracket\sigma\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\to({\llbracket\sigma\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\big{)}$

Schematism, i.e. the possibility to instantiate type variables $\alpha_{l}$,
is essential to capture mixin behavior. This encoding is possible under the
assumption of a finite set of labels $\mathcal{L}$, which is valid because
synthesis does not introduce new labels. The encoding overhead is polynomially
bounded by product of the number of mixin combinators and the number of
labels.

######  Lemma 21 (Translation Completeness).

Assume $(\star)$.
For any $\rho\in\mathbb{T}_{{\langle\rangle}}$ with $\mbox{\it
lbl}(\rho)\subseteq\mathcal{L}$ there exists a substitution $S$ and a type
$\tau\in\mathbb{T}$ such that $S(\tau_{M})\leq{\llbracket\tau\rrbracket}$ and
$\tau=(\sigma\to\rho\cap\rho_{1})\to(\sigma\to\rho+\rho_{2})$.

Let $\rho=\bigcap\limits_{l\in L}{\langle l:\tau_{l}\rangle}$ for some
$L\subseteq\mathcal{L}$. By Lemma 3.4 we may assume for each $l\in L$ that
$\tau_{l}$ does not contain $+$. We define

$S(\alpha_{l})=\begin{cases}{\llbracket\tau_{l}\rrbracket}&\text{if }l\in
L\setminus\mbox{\it lbl}(R)\\\ \omega&\text{else}\end{cases}$

and successively applying Lemma 19 obtain

$\displaystyle S(\tau_{M})$
$\displaystyle\leq{\llbracket\big{(}(\sigma\to\rho_{1})\to(\sigma\to\rho_{2})\big{)}\cap\bigcap\limits_{l\in
L\setminus\mbox{\it lbl}(R)}\big{(}(\sigma\to{\langle
l:\tau_{l}\rangle})\to(\sigma\to{\langle
l:\tau_{l}\rangle})\big{)}\rrbracket}$
$\displaystyle\leq{\llbracket\big{(}(\sigma\to\bigcap\limits_{l\in
L\setminus\mbox{\it lbl}(R)}{\langle
l:\tau_{l}\rangle}\cap\rho_{1})\to(\sigma\to\bigcap\limits_{l\in
L\setminus\mbox{\it lbl}(R)}{\langle
l:\tau_{l}\rangle}\cap\rho_{2})\big{)}\rrbracket}$
$\displaystyle\leq{\llbracket\big{(}(\sigma\to\rho\cap\rho_{1})\to(\sigma\to\underbrace{\bigcap\limits_{l\in
L\setminus\mbox{\it lbl}(R)}{\langle
l:\tau_{l}\rangle}\cap\rho_{2}}_{=\rho+\rho_{2}\text{ by Lem.
}\ref{lem:label}.\ref{lem:label-b}})\big{)}\rrbracket}$

Translation Completeness ensures that each type $\Lambda_{R}$ of $M$ according
to $(\star)$ is captured by some instance of $\tau_{M}$.

Using the above translation properties, we construct a repository of typed
combinators representing classes and mixins.

###  5.2. Mixin Composition

In this section we denote type assignment in $\Lambda_{R}$ by
$\vdash_{{\langle\rangle}}$ and fix the following ingredients:

  * •

A finite set of classes $\mathcal{C}$.

  * •

For each $C\in\mathcal{C}$ types
$\sigma_{C}\in\mathbb{T},\rho_{C}\in\mathbb{T}_{{\langle\rangle}}$ such that
${\llbracket\sigma_{C}\to\rho_{C}\rrbracket}$ is defined and
$\vdash_{{\langle\rangle}}C:\sigma_{C}\to\rho_{C}$.

  * •

A finite set of mixins $\mathcal{M}$.

  * •

For each $M\in\mathcal{M}$ types $\sigma_{M}\in\mathbb{T}$ and
$\rho_{M}^{1},\rho_{M}^{2}\in\mathbb{T}_{{\langle\rangle}}$ such that
${\llbracket\sigma_{M}\rrbracket},{\llbracket\rho_{M}^{1}\rrbracket},{\llbracket\rho_{M}^{2}\rrbracket}$
are defined and for all types $\rho\in\mathbb{T}_{{\langle\rangle}}$ we have
$\vdash_{{\langle\rangle}}M:(\sigma_{M}\to\rho\cap\rho_{M}^{1})\to(\sigma_{M}\to\rho+\rho_{M}^{2})$.

  * •

For each $M\in\mathcal{M}$ the non-empty set of labels $L_{M}=\mbox{\it
lbl}(\rho_{M}^{2})\subseteq\mathcal{L}$ defined by $M$.

We translate given classes and mixins to the following repository
$\Delta_{\mathcal{L}}^{\mathcal{C},\mathcal{M}}$ of combinators

$\displaystyle\Delta_{\mathcal{L}}^{\mathcal{C},\mathcal{M}}=$
$\displaystyle\\{C:{\llbracket\sigma_{C}\to\rho_{C}\rrbracket}\mid
C\in\mathcal{C}\\}$
$\displaystyle\cup\\{M:\big{(}({\llbracket\sigma_{M}\rrbracket}\to{\llbracket\rho_{M}^{1}\rrbracket})\to({\llbracket\sigma_{M}\rrbracket}\to{\llbracket\rho_{M}^{2}\rrbracket})\big{)}$
$\displaystyle\quad\cap\bigcap\limits_{l\in\mathcal{L}\setminus
L_{M}}\big{(}({\llbracket\sigma_{M}\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\to({\llbracket\sigma_{M}\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\big{)}\mid M\in\mathcal{M}\\}$

Note that we use identifiers $C$ for classes and $M$ for mixins just as
symbolic names in the repository, while they are also typable closed terms in
$\Lambda_{R}$.

To simplify notation, we introduce the infix metaoperator $\gg$ such that
$x\gg f=f\ x$. It is left associative and has the lowest precedence.
Accordingly, $x\gg f\gg g=g\ (f\ x)$.

Although types in $\Delta_{\mathcal{L}}^{\mathcal{C},\mathcal{M}}$ do not
contain record-merge, types of mixin compositions in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ are sound, which is shown in the
following Theorem 22.

######  Theorem 22 (Soundness).

Let $M_{1},\ldots,M_{n}\in\mathcal{M}$ be mixins, let $C\in\mathcal{C}$ be a
class, let $\sigma\in\mathbb{T},\rho\in\mathbb{T}_{{\langle\rangle}}$ be types
such that ${\llbracket\sigma\to\rho\rrbracket}$ is defined, and let
$k\in\mathbb{N}$.
If $\Delta_{\mathcal{L}}^{\mathcal{C},\mathcal{M}}\vdash_{k}C\gg
M_{1}\gg\ldots\gg M_{n}:{\llbracket\sigma\to\rho\rrbracket}$, then
$\vdash_{{\langle\rangle}}C\gg M_{1}\gg M_{2}\gg\ldots\gg
M_{n}:\sigma\to\rho$.

######  Proof 5.3.

Induction on $n$ using Lemma 20 and $(\rightarrow\mbox{\it E})$.

Complementarily, types of mixin compositions in
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$ are complete wrt. $\Lambda_{R}$
type assumptions for classes and mixins listed above. Specifically, we show in
the following Theorem 23 that, assuming arguably natural typings of classes
and mixins, we can find corresponding
$\textsf{BCL}_{k}(\mathbb{T}_{\mathbb{C}})$-counterparts of $\Lambda_{R}$ type
derivations.

######  Theorem 23 (Partial Completeness).

Let $\Gamma\subseteq\\{x_{C}:\sigma_{C}\to\rho_{C}\mid
C\in\mathcal{C}\\}\cup\\{x_{M}^{\rho}:(\sigma_{M}\to\rho\cap\rho_{M}^{1})\to(\sigma_{M}\to\rho+\rho_{M}^{2})\mid
M\in\mathcal{M},\rho\in\mathbb{T}_{{\langle\rangle}},{\llbracket\rho\rrbracket}\text{
is defined}\\}$ be a finite context and let
$\sigma\in\mathbb{T},\rho\in\mathbb{T}_{{\langle\rangle}}$ be types such that
${\llbracket\sigma\to\rho\rrbracket}$ is defined. Let
$k=\max(\\{\operatorname{level}({\llbracket\rho_{C}\rrbracket})\mid
C\in\mathcal{C}\\}\cup\\{\operatorname{level}({\llbracket\rho_{M}^{2}\rrbracket})\mid
M\in\mathcal{M}\\}\cup\\{\operatorname{level}({\llbracket\rho\rrbracket})\\})$.
Let $M_{1},\ldots,M_{n}\in\mathcal{M}$ be mixins.
If $\Gamma\vdash_{{\langle\rangle}}x_{C}\gg x_{M_{1}}^{\rho_{1}}\gg\ldots\gg
x_{M_{n}}^{\rho_{n}}:\sigma\to\rho$, then
$\Delta_{\mathcal{L}}^{\mathcal{C},\mathcal{M}}\vdash_{k}C\gg
M_{1}\gg\ldots\gg M_{n}:{\llbracket\sigma\to\rho\rrbracket}$.

######  Proof 5.4.

Induction on $n$ choosing for each $x_{M}^{\rho}$ where
$\rho=\bigcap\limits_{l\in L}{\langle l:\tau_{l}\rangle}$ the substitution
$\alpha_{l}\mapsto{\llbracket\tau_{l}\rrbracket}$ for $l\in L\setminus L_{M}$
and $\alpha_{l}\mapsto\omega$ otherwise to type
$M\in\Delta_{\mathcal{L}}^{\mathcal{C},\mathcal{M}}$ and using
$(\rightarrow\mbox{\it E})$, $(\leq)$, Lemma 21.

Note that Theorem 23 defines a bound $k$ based on the input. In the following,
we use this bound ensuring that the provided examples are in fact computable.
We extend the running example by the following mixin Succ2.

$\displaystyle\text{Succ2}=\lambda\textsf{argClass}.\mathbf{Y}(\lambda\textsf{myClass}.\lambda\textsf{state}.$
$\displaystyle\qquad\texttt{let }\textsf{super}=\textsf{argClass}\
\textsf{state}\texttt{ in }$ $\displaystyle\qquad\texttt{let
}\textsf{self}=\textsf{myClass}\ \textsf{state}\texttt{ in }$
$\displaystyle\qquad\qquad\textsf{super}\oplus{\langle\textit{succ2}=\texttt{let
}\textsf{super}^{\prime}=\textsf{argClass}(\textsf{super}.\textit{succ})\texttt{
in }\textsf{super}^{\prime}.succ\rangle})$

Succ2 adds the method succ2 that is the twofold application of succ. Note that
the object super is updated functionally in succ2. Using the above
translation, we obtain

$\displaystyle\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable}\\}}=\\{$
$\displaystyle\quad\text{Num}:\text{Int}\to{\llangle\textit{get}(\text{Int})\cap\textit{set}(\text{Int}\to\text{Int})\cap\textit{succ}(\text{Int})\rrangle},$
$\displaystyle\quad\text{Comparable}:\big{(}(\text{Int}\to{\llangle\textit{get}(\text{Int})\rrangle})\to(\text{Int}\to{\llangle\textit{compare}({\llangle\textit{get}(\text{Int})\rrangle}\to\text{Bool})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{get}(\alpha_{\textit{get}})\rrangle})\to(\text{Int}\to{\llangle\textit{get}(\alpha_{\textit{get}})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{set}(\alpha_{\textit{set}})\rrangle})\to(\text{Int}\to{\llangle\textit{set}(\alpha_{\textit{set}})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{succ}(\alpha_{\textit{succ}})\rrangle})\to(\text{Int}\to{\llangle\textit{succ}(\alpha_{\textit{succ}})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{succ2}(\alpha_{\textit{succ2}})\rrangle})\to(\text{Int}\to{\llangle\textit{succ2}(\alpha_{\textit{succ2}})\rrangle})\big{)},$
$\displaystyle\quad\text{Succ2}:\big{(}(\text{Int}\to{\llangle\textit{succ}(\text{Int})\rrangle})\to(\text{Int}\to{\llangle\textit{succ2}(\text{Int})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{get}(\alpha_{\textit{get}})\rrangle})\to(\text{Int}\to{\llangle\textit{get}(\alpha_{\textit{get}})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{set}(\alpha_{\textit{set}})\rrangle})\to(\text{Int}\to{\llangle\textit{set}(\alpha_{\textit{set}})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{succ}(\alpha_{\textit{succ}})\rrangle})\to(\text{Int}\to{\llangle\textit{succ}(\alpha_{\textit{succ}})\rrangle})\big{)}$
$\displaystyle\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{compare}(\alpha_{\textit{compare}})\rrangle})\to(\text{Int}\to{\llangle\textit{compare}(\alpha_{\textit{compare}})\rrangle})\big{)}\\}$

We may ask inhabitation questions such as

$\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable}\\}}\vdash_{k}?:{\llbracket\text{Int}\to{\langle\textit{succ}:\text{Int},\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool},\textit{succ2}:\text{Int}\rangle}\rrbracket}$

and obtain the combinatory term
“$\text{Num}\gg\text{Comparable}\gg\text{Succ2}$” as the synthesized result.
From Theorem 22 we know

$\vdash_{{\langle\rangle}}\text{Num}\gg\text{Comparable}\gg\text{Succ2}:\text{Int}\to{\langle\textit{succ}:\text{Int},\textit{compare}:{\langle\textit{get}:\text{Int}\rangle}\to\text{Bool},\textit{succ2}:\text{Int}\rangle}$

The presented encoding has several benefits with respect to scalability.
First, the size of the presented repositories is polynomial in
$|\mathcal{L}|*|\mathcal{C}|*|\mathcal{M}|$. Second, expanding the label set
$\mathcal{L}$ can be performed automatically in polynomial time by adding
additional components $({\llbracket\sigma_{M}\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})\to({\llbracket\sigma_{M}\rrbracket}\to{\llangle
l(\alpha_{l})\rrangle})$ to each mixin $M$ for each new label $l$. Third,
adding a class/mixin to an existing repository is as simple as adding one
typed combinator for the class/mixin. Existing combinators in the repository
remain untouched. As an example, we add the following mixin SuccDelta to
$\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable}\\}}$.

$\displaystyle\text{SuccDelta}=\lambda\textsf{argClass}.\mathbf{Y}(\lambda\textsf{myClass}.\lambda\textsf{state}.$
$\displaystyle\qquad\texttt{let }\textsf{super}=\textsf{argClass}\
\textsf{state}\texttt{ in }$ $\displaystyle\qquad\texttt{let
}\textsf{self}=\textsf{myClass}\ \textsf{state}\texttt{ in
}\textsf{super}\oplus{\langle\textit{succ}=\lambda
d.(\textsf{super}.\textit{set}(\textsf{super}.get+d)\rangle}))$

In $\Lambda_{R}$ for all types $\rho\in\mathbb{T}_{{\langle\rangle}}$ we have

$\vdash_{{\langle\rangle}}\text{SuccDelta}\colon(\text{Int}\to\rho\cap{\langle\textit{get}:\text{Int},\textit{set}:\text{Int}\to\text{Int}\rangle})\to(\text{Int}\to\rho+{\langle\textit{succ}:\text{Int}\to\text{Int}\rangle})$

We obtain the following extended repository

$\displaystyle\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable},\text{SuccDelta}\\}}=\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable}\\}}$
$\displaystyle\qquad\cup\\{\text{SuccDelta}:\big{(}(\text{Int}\to{\llangle\textit{get}(\text{Int})\cap\textit{set}(\text{Int}\to\text{Int})\rrangle})\to(\text{Int}\to{\llangle\textit{succ}(\text{Int}\to\text{Int})\rrangle})\big{)}$
$\displaystyle\qquad\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{get}(\alpha_{\textit{get}})\rrangle})\to(\text{Int}\to{\llangle\textit{get}(\alpha_{\textit{get}})\rrangle})\big{)}$
$\displaystyle\qquad\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{set}(\alpha_{\textit{set}})\rrangle})\to(\text{Int}\to{\llangle\textit{set}(\alpha_{\textit{set}})\rrangle})\big{)}$
$\displaystyle\qquad\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{succ2}(\alpha_{\textit{succ2}})\rrangle})\to(\text{Int}\to{\llangle\textit{succ2}(\alpha_{\textit{succ2}})\rrangle})\big{)}$
$\displaystyle\qquad\qquad\cap\big{(}(\text{Int}\to{\llangle\textit{compare}(\alpha_{\textit{compare}})\rrangle})\to(\text{Int}\to{\llangle\textit{compare}(\alpha_{\textit{compare}})\rrangle})\big{)}\\}$

Asking the inhabitation question

$\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable},\text{SuccDelta}\\}}\vdash_{k}?:{\llbracket\text{Int}\to{\langle\textit{succ}:\text{Int}\to\text{Int},\textit{succ2}:\text{Int}\rangle}\rrbracket}$

synthesizes “$\text{Num}\gg\text{Succ2}\gg\text{SuccDelta}$”. Note that even
in such a simplistic scenario the order in which mixins are applied can be
crucial mainly because $\,\oplus\,$ is not commutative. Moreover, the early
binding of self and the associated preservation of overwritten methods allows
for destructive overwrite of succ by SuccDelta without invalidating succ2 that
is previously added by Succ2. This also may make multiple applications of a
single mixin meaningful.

In order to improve the reading experience, the running example is coherently
arranged in the appendix.

###  5.3. Semantic Types

An additional benefit of using intersection types and, in particular, the
(CL)S framework is the availability of the so called _semantic types_ [Reh13].
Semantic types can be used to further specify the semantics of typed
combinators in a repository and restrict/guide the inhabitant search. Semantic
types consist of additional constants a and constructors
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{c}}(\cdot)$
that arise in the current domain of interest (semantic types are well suited
to capture taxonomies [Reh13]). Native types are augmented by semantic types
using intersection. For example, consider the native type Int. We may be
interested in whether the current value is Even or Odd. Therefore, we may
augment the native type by this information resulting in types of the form
$\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}$
representing even integers or
$\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}$
representing odd integers. This becomes increasingly interesting when we have
knowledge about functional dependencies between semantic types in the domain
of interest. In particular, knowing that successors of even integers are odd
and vice versa, we may augment the native type of Num to represent this domain
knowledge

$\displaystyle\text{Num}:$
$\displaystyle(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{get}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\rrangle})$
$\displaystyle\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\llangle\textit{get}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}})\rrangle})$
$\displaystyle\cap(\text{Int}\to{\llangle\textit{set}((\text{Int}\to\text{Int})\cap({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\cap({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}))\rrangle})$
$\displaystyle\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{succ}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}})\rrangle})$
$\displaystyle\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\llangle\textit{succ}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\rrangle})$

The above type of Num expresses that the get method returns the semantic type
of the underlying state of the object, the set method does not take the
underlying state of the object into account, and the succ method returns the
opposed semantic type. Note that, if all semantic components are erased, the
remaining type of Num is exactly the original native type.

In the setting of mixin composition synthesis, semantic types enhance the
expressiveness of the type system. The mixin Succ2 from our running example
can be typed in the following way

$\displaystyle\text{Succ2}:(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{succ}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}})\rrangle})\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\llangle\textit{succ}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\rrangle})$
$\displaystyle\quad\to(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{succ2}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\rrangle})\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\llangle\textit{succ2}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}})\rrangle})$

The above type of Succ2 expresses that given the proper semantic types of
succ, the semantic type of succ2 corresponds to the semantic type of the
underlying state of the object, i.e. the twofold successor of an even (resp.
odd) integer is even (resp. odd).

This allows to distinguish methods with different semantics in the domain of
interest but exhibiting identical native types. Consider the following mixin
Parity that overwrites the method succ to be the twofold successor such that
the parity of the underlying state remains the same.

$\displaystyle\text{Parity}=\lambda\textsf{argClass}.\mathbf{Y}(\lambda\textsf{myClass}.\lambda\textsf{state}.$
$\displaystyle\qquad\texttt{let }\textsf{super}=\textsf{argClass}\
\textsf{state}\texttt{ in }$ $\displaystyle\qquad\texttt{let
}\textsf{self}=\textsf{myClass}\ \textsf{state}\texttt{ in
}\textsf{super}\oplus{\langle\textit{succ}=\textsf{super}.\textit{succ2}\rangle})$

Parity can be typed in the following way

$\displaystyle\text{Parity}:(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{succ2}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\rrangle})\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\llangle\textit{succ2}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}})\rrangle})$
$\displaystyle\quad\to(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{succ}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}})\rrangle})\cap(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}}\to{\llangle\textit{succ}(\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Odd}})\rrangle})$

Asking the inhabitation question

$\Delta_{\\{\textit{get},\textit{set},\textit{succ},\textit{succ2},\textit{compare}\\}}^{\\{\text{Num}\\},\\{\text{Succ2},\text{Comparable},\text{SuccDelta},\text{Parity}\\}}\vdash_{k}\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\to{\llangle\textit{succ}:\text{Int}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Even}}\rrangle}$

results in “$\text{Num}\gg\text{Succ2}\gg\text{Parity}$”. Note that due to the
early binding, succ2 uses the old succ method which has the required semantics
in order for Succ2 to be applied.

Let us explore the descriptive capabilities of semantic types using a more
illustrative example. Consider the domain of cryptography containing
algorithms for encrypting and signing data. Describing abstract properties
such as “encrypted” or “signed” at the lowest level, e.g. using Hoare logic,
requires an enormous amount of work. In practice, such properties are
described textually while the native type, e.g. String, does not capture
particular semantics. Consider the following repository

$\displaystyle\Delta_{\text{native}}=\\{$ $\displaystyle\text{Reader}:$
$\displaystyle\text{String}\to{\llangle\textit{get}(\text{String})\rrangle},$
$\displaystyle\text{Enc}:$
$\displaystyle(\text{String}\to{\llangle\textit{get}(\text{String})\rrangle})\to\text{String}\to{\llangle\textit{get}(\text{String})\rrangle},$
$\displaystyle\text{Sign}:$
$\displaystyle(\text{String}\to{\llangle\textit{get}(\text{String})\rrangle})\to\text{String}\to{\llangle\textit{get}(\text{String})\rrangle},$
$\displaystyle\text{Time}:$
$\displaystyle(\text{String}\to{\llangle\textit{get}(\text{String})\rrangle})\to\text{String}\to{\llangle\textit{get}(\text{String})\rrangle}\\}$

with the following textual description

  * •

The Reader class provides a get method that returns some plain text data.

  * •

The Enc mixin replaces the get method of a given class with a new get method
that returns the encrypted result of the overwritten get method.

  * •

The Sign mixin replaces the get method appending the signature to the result
of the overwritten get method.

  * •

The Time mixin replaces the get method appending a time-stamp to the result of
the overwritten get method.

Unfortunately, the types in $\Delta$ are too general to be used for synthesis
of meaningful compositions. However, we can use semantic types to embed the
textual description of the particular semantics in our domain of interest into
$\Delta_{\text{native}}$ resulting in the following repository

$\displaystyle\Delta=\\{$ $\displaystyle\text{Reader}:$
$\displaystyle\text{String}\to{\llangle\textit{get}(\text{String}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Plain}})\rrangle},$
$\displaystyle\text{Enc}:$
$\displaystyle(\text{String}\to{\llangle\textit{get}(\text{String}\cap\alpha)\rrangle})\to(\text{String}\to{\llangle\textit{get}(\text{String}\cap{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textsf{Enc}}(\alpha))\rrangle}),$
$\displaystyle\text{Sign}:$