enumitemNegative labelwidth 16115 LABEL:LastPageSep. 07, 2018Feb. 13, 2020

# Covariance and Contravariance:
a fresh look at an old issue
(a primer in advanced type systems
for learning functional programmers)

Giuseppe Castagna  CNRS, Institut de Recherche en Informatique Fondamentale,
Université de Paris, France

###### Abstract.

Twenty years ago, in an article titled “Covariance and contravariance:
conflict without a cause”, I argued that covariant and contravariant
specialization of method parameters in object-oriented programming had
different purposes and deduced that, not only they could, but actually they
should both coexist in the same language.

In this work I reexamine the result of that article in the light of recent
advances in (sub-)typing theory and programming languages, taking a fresh look
at this old issue.

Actually, the revamping of this problem is just an excuse for writing an essay
that aims at explaining sophisticated type-theoretic concepts, in simple terms
and by examples, to undergraduate computer science students and/or willing
functional programmers.

Finally, I took advantage of this opportunity to describe some undocumented
advanced techniques of type-systems implementation that are known only to few
insiders that dug in the code of some compilers: therefore, even expert
language designers and implementers may find this work worth of reading.

###### Key words and phrases:

Object-oriented languages, type theory, subtyping, intersection types,
overloading, semantic subtyping

##  1\. Introduction

Twenty years ago I wrote an article titled “Covariance and contravariance:
conflict without a cause” [Cas95] where I argued that the heated debate that
at the time opposed the faction of covariant overriding of methods in object-
oriented languages against the congregation of the contravariant
specialization had no real ground, since the two policies had different
orthogonal purposes that not only could but actually should coexist in the
same language. The article was, I would dare to say, fairly successful even
outside the restricted research circles. For instance, for many years at the
entry “Contra-/Co- variance” of FAQ of the comp.object Usenet newsgroup
(question 71) the answer was just a pointer to my article (actually, to the
tech-rep that preceded the publication). In spite of that, I think that the
message of the article did not (or, at least, could not) reach practitioners
and thus influence actual programming. Probably all that may have got to
(some) programmers was that there was some theoretical paper that explained
what each of covariance and contravariance was good for (with the associated
reaction: “…so what?”). One reason for that, I think, is that at the time both
type theory and programming languages were not developed enough to well
explain the issue. I will not explain here again the whole article but the
point is that in order to expose my argumentation I had to invent some
constructions that did not look close to anything present in programming
languages at the time: in particular I had to use weird “overloaded types”
(these were sets of function types with two eerie formation conditions), write
functions by using a strange “&”-infix notation, and even in their most simple
form functions had to distinguish two kinds of parameters by separating them
by a vertical bar. I am sure that alone any of these oddity was enough to put
off any serious programmer.

Twenty years have passed, both programming languages and, even more, type
theory have much evolved to a point that I think it is now possible to explain
covariance and contravariance to practitioners, a task the first half of this
article is devoted to.

To do that I will use the type theory of _semantic subtyping_ [FCB08], while
to illustrate all the examples I chose to use the programming language _Perl
6_ [Per], but an important aspect of this paper is that you can read it
without any preliminary knowledge of them.

A reader aware of the theory of semantic subtyping may be astonished that I
use such a theory to target practitioners. As a matter of fact, semantic
subtyping is a sophisticated theory that relies on complex set-theoretic
properties that, for sure, do not belong to the education and practice
background of most practitioners. The point is that while the underlying
theory of types is probably out of reach of an average programmer, its types
are very easy to use and understand for this programmer since, as I show in
this paper, they can be explained in terms of very simple notions such as sets
of values and set containment. It is like cars. Forty years ago most cars had
such a simple conception that nearly everybody with some experience and few
common tools could open the trunk and fix them.111 Though at that time I did
not succeed to convince my parents to let me repair our family car (well, I
was twelve). Nowadays cars are so full of electronics that for many of them
you must go to authorized dealers to have it repaired since this is out of
reach for generic repairers. However, all this complexity is hidden to the
end-user, and cars today are much simpler to drive than they were forty years
ago. So it is for type systems, whose definitions are getting more and more
involved but (in several cases) they are getting simpler and simpler for the
programmer to use.

For what concerns the Perl 6 language, I am not a great user or supporter of
it (the examples I give here count among the most complicated programs I wrote
in it). Although it probably does not have the most elegant (and surely not
the most streamlined) syntax I ever saw in a programming language, I chose it
because it has the double advantage of having enough syntax to explain the
covariance/contravariance problem and of having a fuzzy-yet-to-be-fixed type
system. So while all the expressions I will write can be run on any of the
several Perl 6 implementations currently being developed, I will keep of Perl
types just their syntax (and with several liberties), and give to these types
my very personal interpretation. Although Perl 6 is not the best candidate to
present this paper (the perfect candidate would be the programming language
$\mathbb{C}$Duce [BCF03, CDu] whose type system is here borrowed and grafted
on Perl) one of the challenges of this paper was to use a mainstream
programming language that was not designed with types in mind—far from that—,
whence the choice of Perl 6. I am aware that this choice will make some
colleague researchers sneer and some practitioners groan: please give me the
benefit of the doubt till Section 4.

##### Plan of the article.

I organize the rest of the paper as if it were the documentation bundled with
a TV set. When you buy a TV you want to read the instructions on how to tune
channels and connect it to your Wii™: these are in the user manual. You
usually skip the electrical schemes that come with it, unless you want to
repair it, or to build your own TV from them. Besides, if you are curious to
know why these electrical schemes show you nightly news instead of exploding
and killing everybody in the room, then you probably are a researcher and you
need to read few articles and books on electronics and electromagnetism for
which the bundled documentation is useless.

Section 2 is my “user manual”: it is a primer on types for a Perl programmer
who never used types (seriously) before. There I use (a personalized version
of) Perl 6 types to explain what types are and how they are related in the
“semantic subtyping” framework. Although most of the notions will be known to
most of the readers, the purpose of the presentation is to demonstrate that
with few easy-to-grasp key concepts, it is possible to bring programmers to
sophisticated reasoning about programs and types. Section 3 applies the
notions introduced in the primer to the covariance vs. contravariance issue.
In that section I will present object-oriented programming in Perl 6, show why
one can consider objects and classes as syntactic sugar to define some “multi
subroutines”, explain the issue of covariance and contravariance and their use
in terms of these multi subroutines. Section 4 is my “electrical blueprint”.
It aims at language designers and implementers and explains how semantic
subtyping can be efficiently implemented, by describing the algorithms and
data structures to be used to check type inclusion and perform type
assignment. Section 5 is the one that you never find in a TV documentation and
it gives a roadmap to the references that allow a researcher to understand the
principles underlying semantic subtyping and why the algorithms of the
preceding sections work: if you do not believe me and you need pointers to the
formal proofs, then this is the section you need to look at. In Section 6 I
try to summarize the lessons that can be drawn from this work and, in
particular, what I learnt from writing it. The primer section contains several
exercises whose solutions are given in appendix. All the article long I use
(admittedly, too many) footnotes to complete the main text with practical
observations, missing definitions, and technical considerations for the
advanced reader; the last kind of footnotes are marked by an asterisk and can
be safely skipped (actually, on second thought, I suggest skipping all
footnotes unless you are lost).

This article has several possible keys of reading; an obvious one is that this
paper can be taken as a proposal for a statically safe type-system for the
functional core of Perl 6 and a specification of the algorithms to implement
it. However, the actual motivation to write this article came from two
distinct sources. The first motivation is that semantic subtyping explains the
covariance/contravariance issue of [Cas95] in much a cleaner way and without
resorting to a somehow “ad hoc” formalism (as the $\lambda\&$-calculus of
[Cas95] was). So for a long time I have been wanting to reframe my old work in
terms of semantic subtyping. But the motivation that spurred me to start
writing it, is that few years ago I started to teach an undergraduate course
on advanced programming at École Normale Supérieure de Cachan. Formerly I had
been teaching issues about covariance and contravariance only at master level,
and I then realized that while the problem is still relevant, the original
explanation was too high-level for undergraduate students (i.e., it still
contained too many $\lambda$’s). The real target reader of this work is, thus,
the undergraduate student of an advanced programming course, and this explains
why all examples of this paper are written in a popular language and it does
not contain a single “$\lambda$”, theorem, or inference rule (just two formal
definitions). So the not so hidden challenge tackled by this work is to
explain sophisticated type theoretic concepts to a willing functional
programmer. These two motivations also explain why I consider this work as
both a _theoretical_ and an _educational_ pearl, in the sense of the ICFP and
POPL conferences call for papers.

##  2\. Types primer for the learning programmer

###  2.1. What is a type?

If you know what a value is (i.e., any result that can be returned by an
expression), then you know what a type is: it is a set of values (though not
all sets of values are types222* Formally, this can be seen by considering
cardinalities: types and values are inductively defined and, therefore, they
form recursively enumerable sets, while the powerset of values is not. More
prosaically, the set of all functions that when applied to, say, an integer
formed by an odd number of digits return a palindrome integer, is a set of
values that hardly seems to conform to the idea of a type.) Then you also know
what _subtyping_ is since it coincides with set containment: a type is a
subtype of a second type if all values of/in the former type are values of/in
the latter. What a type system does is to define a _typing relation_ that is a
relation between expressions and types. This relation must have the property
that an expression is given (i.e., it is related to) a type only if whenever
it returns a value, then the value is of/in that type.

Let me give some more details. I will consider a very restricted syntax for
Perl types (and actually some of these types were just proposed but never
implemented) as described by the following grammar:333 For the reader not
aware of the notation that follows (called EBNF grammar), this is a standard
way to define the syntax of some language (in our case, the language of
types). It can be understood by reading the symbol “::=” as “is either” and
the symbol “|” as “or”. This yields the following reading. “A type T  _is
either_ Bool _or_ Int _or_ Any _or_ (T1 , T2) (where T1 and T2 are types) _or_
T1|T2 (where T1 and T2 are types) _or_ …”. Notice that to define, say, (T1 ,
T2) we assumed to know what the types T1 and T2 that compose it are: this
roughly corresponds to defining types _by induction_.

$\texttt{T}::=\texttt{Bool}\,\mid\,\texttt{Int}\,\mid\,\texttt{Any}\,\mid\,\texttt{(}\texttt{T}\,\texttt{,}\,\texttt{T}\texttt{)}\,\mid\,\texttt{T}\texttt{|}\texttt{T}\,\mid\,\texttt{T}\texttt{\&}\texttt{T}\,\mid\,\texttt{not(}\texttt{T}\texttt{)}\,\mid\,\texttt{T}\texttt{-{}->}\texttt{T}$

What does each type mean? To define the meaning of a type, we define the set
of values it denotes. Since the types above are defined inductively we can
define their precise meaning by induction, namely:

Bool:

denotes the set that contains just two values $\\{$true , false$\\}$

Int:

denotes the set that contains all the numeric constants: $\\{$0, -1, 1, -2, 2,
-3,…$\\}$.

Any:

denotes the set that contains all the values of the language.

$\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}$:

denotes the set that contains all the possible pairs $(v_{1},v_{2})$ where
$v_{1}$ is a value in $\texttt{T}_{1}$ and $v_{2}$ a value in
$\texttt{T}_{2}$, that is $\\{(v_{1},v_{2})\mid
v_{1}\in\texttt{T}_{1}\,,\,v_{2}\in\texttt{T}_{2}\\}$.

$\texttt{T}_{1}\texttt{|}\,\texttt{T}_{2}$:

denotes the _union_ of the sets denoted by $\texttt{T}_{1}$ and
$\texttt{T}_{2}$, that is the set $\\{v\mid v\in\texttt{T}_{1}\textrm{ or
}v\in\texttt{T}_{2}\\}$

$\texttt{T}_{1}\texttt{\&}\,\texttt{T}_{2}$:

denotes the _intersection_ of the sets denoted by $\texttt{T}_{1}$ and
$\texttt{T}_{2}$, that is the set $\\{v\mid v\in\texttt{T}_{1}\textrm{ and
}v\in\texttt{T}_{2}\\}$.

not(T):

denotes the set of all the values that are not in the set denoted by T, that
is $\\{v\mid v\not\in\texttt{T}\\}$. So in particular not(Any)denotes the
empty set.

$\texttt{T}_{1}\texttt{-{}->}\texttt{T}_{2}$:

is the set of all function values that when applied to a value in
$\texttt{T}_{1}$, if they return a value (i.e., if the application does not
loop), then this value is in $\texttt{T}_{2}$.

Of course, the last case is the most delicate one and deserves more
explanation. First of all we must define what a “functional value” is. A
functional value is a (closed444 A function is closed if all the variables
that appear in its body are either the parameters of the function or they have
been defined inside the body) expression that defines a function. In
$\lambda$-calculus we would say it is a lambda-abstraction.555 Lambda-
abstractions have been recently integrated in languages such as C# and Java,
where they are called “lambda-expressions”. In Perl 6 it is any expression of
the form “sub `(`_parameters_`)` `{` _body_`}` ”. So for instance sub `(Int
$x){ return $x + 1 }` is a Perl 6 value that denotes the successor
function.666 In Perl variables are prefixed by the dollar sign, and sub is the
apocope for subroutine. Functions can be named (which will turn out to be
quite handy in what follows) such as for sub `succ(Int $x){ return $x + 1 }`
which gives the name succ to the successor function. It is easy to see that
succ is a value in Int\-->Int: it suffices to apply the definition I gave for
arrow types, that is, check that when succ is applied to a value in Int, it
returns a value in Int (succ is total).777* Notice that the definition of the
set of values denoted by an arrow type does not depend on the inputs on which
a function diverges. As a consequence, the function that diverges on all
inputs belongs to every arrow type. This is the reason why the set denoted by
an arrow type (or by any intersection of arrow types) is never empty: it
always contains the function that diverges on all arguments.

###  2.2. What is a subtype?

Perl 6 provides the constructor subset to define types such as Nat, Even, and
Odd, respectively denoting the set of natural, even, and odd numbers. For
instance, the last two types can be defined as follows (where % is in Perl 6
the modulo operator):

       subset Even of Int where { $_ % 2 == 0 }
       subset Odd  of Int where { $_ % 2 == 1 }

(e.g., the first is Perl syntax for $\textit{Even}=\\{x\in\texttt{Int}\mid
x\;\mathbf{mod}\;2=0\\}$). Both these types are subsets of Int.888 More
precisely, I should have said “they denote subsets”, but from now on I
identify types with the sets of values they denote. Let us use these types to
show that a same value may belong to different types. For instance, it is easy
to see that succ is also a value in Even-->Int: if we apply succ to a even
number, it returns a value in Int. Since succ is a value both in Even-->Int
and in Int-->Int, then, by definition of intersection type, it is a value in
(Even-->Int) & (Int-->Int). This is true not only for succ but also for all
values in Int-->Int: whenever we apply a function in Int-->Int to an even
number, if it returns a value, then this value is in Int. We say that
Int-->Int is a _subtype_ of Even-->Int and write it as Int-->Int <:
Even-->Int. So, as I informally said at the beginning of the section,
subtyping is just set containment on values. [Subtype] A type $\texttt{T}_{1}$
is a _subtype_ of a type $\texttt{T}_{2}$, written
$\texttt{T}_{1}\texttt{<:}\texttt{T}_{2}$, if all values in $\texttt{T}_{1}$
are values in $\texttt{T}_{2}$. While the subtyping relation
Int-->Int<:Even-->Int holds, the converse (i.e., Even-->Int <:Int-->Int) does
not. For instance, the division-by-two function sub `(Int $x){ $x / 2 }` is a
value in Even-->Int but not in Int-->Int since when applied to an integer does
not always return an integer (for Perl’s purists: notice that I omitted the
return keyword: since in Perl 6 it is optional, in this section I will
systematically omit it). Actually, since we have that Int-->Int<:Even-->Int,
then stating that succ has type (Even-->Int) & (Int-->Int) does not bring any
further information: we are intersecting a set with a superset of it,
therefore this intersection type is _equivalent to_ (i.e., it denotes the same
set of values as) Int-->Int. To see an example of a meaningful intersection
type, the reader can easily check that the succ function is in (Even-->Odd) &
(Odd-->Even): succ applied to an even number returns an odd number (so it is
in Even-->Odd) and applied to an odd number it returns an even one (so it is
also in Odd-->Even). And this brings useful information since (Even-->Odd) &
(Odd-->Even)<:Int-->Int is a _strict_ containment, that is, there are values
of the type on the right hand-side of “<:” that do not have the type on the
left hand-side of the relation (e.g., the identity function is in Int-->Int,
but it has neither type Even-->Odd, nor type Odd-->Even).999***(!) My fellow
type theorists—but probably just them—may have noticed that I was a tad sloppy
here. The theory I use in this paper gives expressions an _intrinsic
semantics_ (in the sense of Reynolds [Rey03]) since the semantics of functions
depends on the explicit type annotations of their parameters. So, strictly
speaking, it is not the succ function I defined in the previous page that has
type (Even-->Odd) & (Odd-->Even) (since, its parameter is annotated by Int,
then the function has type Int-->Int…and every supertype of it, but not the
above intersection type) but, rather, a version of it explicitly annotated
with the intersection type at issue. Likewise, the definition of the division-
by-two function above is not well-typed and should rather be written as sub
(Even $x){ $x / 2 }. In particular, the intrinsic semantics explains why later
in Section 2.3 the second version of sumC has type (13) but not (12).  The
subtyping relation above holds not only for Even and Odd, but it can be
generalized to any pair of arbitrary types. Since Int is equivalent to
Odd|Even (i.e., the two types denote the same set of values), then the last
subtyping relation can be rewritten as (Even-->Odd) & (Odd-->Even)
<:(Odd|Even)\-->(Odd|Even). This is just an instance of the following relation

$(\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1})\,\texttt{\&}\,(\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2})~{}~{}\texttt{<:}~{}~{}(\texttt{S}_{1}\texttt{|}\texttt{S}_{2})\texttt{-{}->}(\texttt{T}_{1}\texttt{|}\texttt{T}_{2})$
(1)

that holds for all types, $\texttt{S}_{1}$, $\texttt{S}_{2}$,
$\texttt{T}_{1}$, and $\texttt{T}_{2}$, whatever these types are. A value in
the type on the left hand-side of (1) is a function that if applied to an
$\texttt{S}_{1}$ value it returns (if any) a value in $\texttt{T}_{1}$, and if
it is applied to a value in $\texttt{S}_{2}$ it returns (if any) a value in
$\texttt{T}_{2}$. Clearly, this is also a function that when it is applied to
an argument that is either in $\texttt{S}_{1}$ or in $\texttt{S}_{2}$, it will
return a value either in $\texttt{T}_{1}$ or in $\texttt{T}_{2}$ (from now on
I will omit the “if any” parentheses). I leave as an exercise to the reader
[EX1] the task to show that the inclusion is strict, that is, that there
exists a value in the type on the right-hand side of (1) that is not in the
type on left-hand side (see exercise solutions in the appendix).

This shows how some simple reasoning on values allows us to deduce
sophisticated subtyping relations. By a similar reasoning we can introduce two
key notions for this paper, those of covariance and of contravariance. These
two notions come out as soon as one tries to deduce when a type
$\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$ is included in another function
type $\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2}$. Let us first try to deduce
it on a specific example: consider the function sub` double(Int $x){ x+x }`.
This function is of type Int\-->Even. It is easy to see that double (but also
any other function in Int\-->Even) is also a function in Int-->Int, since
whenever it returns an Even, it therefore returns an Int. If double returns an
Int when applied to an Int, then in particular double returns an Int when it
is applied to, say, an Odd number: that is, double is a function in
Odd\-->Int. Since this reasoning holds true for every function in Int-->Even,
then we can deduce that Int-->Even<:Odd-->Int. This relation holds not only
for Int, Even, and Odd, but also for every pair of types whose sub-components
are in a similar relation. Every function value in
$\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$ transforms values in
$\texttt{S}_{1}$ into values in $\texttt{T}_{1}$; therefore, it is also a
function that transforms values in any type $\texttt{S}_{2}$ smaller than
$\texttt{S}_{1}$ into values that are contained in $\texttt{T}_{1}$ and, thus,
in any type $\texttt{T}_{2}$ greater than $\texttt{T}_{1}$. Since these two
conditions are also necessary for containment, then we have following
rule101010* For the advanced reader, in the presence of an empty type, the two
conditions on the right-hand side of (2) are sufficient but not necessary. If
we use Empty to denote not(Any)—i.e., the empty type—, then the correct rule
is:
$(\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1})\,\texttt{<:}\,(\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2})$
if and only if $(\texttt{S}_{2}\texttt{<:}\texttt{S}_{1}\mbox{ and
}\texttt{T}_{1}\texttt{<:}\texttt{T}_{2})$ _or_
$(\texttt{S}_{2}\texttt{<:}\texttt{Empty})$. Likewise in the presence of an
empty type the right-hand side condition of (3) later on are not necessary:
$\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{T}_{1}\texttt{)}\,\texttt{<:}\,\texttt{(}\texttt{S}_{2}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}$
if and only if $(\texttt{S}_{1}\texttt{<:}\texttt{Empty})\mbox{ \emph{or}
}(\texttt{T}_{1}\texttt{<:}\texttt{Empty})\mbox{ \emph{or}
}(\texttt{S}_{1}\texttt{<:}\texttt{S}_{2}~{}\mbox{ \emph{and}
}~{}\texttt{T}_{1}\texttt{<:}\texttt{T}_{2})$.:

$(\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1})\,\texttt{<:}\,(\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2})~{}~{}~{}\Longleftrightarrow~{}~{}~{}\texttt{S}_{2}\texttt{<:}\texttt{S}_{1}~{}\mbox{
and }~{}\texttt{T}_{1}\texttt{<:}\texttt{T}_{2}$ (2)

We notice that while the “T” types have the same positions with respect to <:
in both sides of equation (2), the “S” types have a different position on the
right and left sides of (2). Borrowing the terminology from category theory,
it is customary to say that the function type constructor “\-->” is
_covariant_ on the codomain type—since it preserves the direction of the <:
relation—, and is _contravariant_ on the domain type—since it inverts the
direction of the <: relation.

As a final remark, note that while in general it is easy to check whether a
value is in some type (just apply the rules of Section 2.1), it is usually
quite harder to decide whether a type is contained into another. However,
while a programmer should clearly master the former problem, she should be
just mildly worried by the latter. Of course, she must be able to use in her
programming practice some generic subtyping rules such as (2) and at least the
following (pretty straightforward) ones:

$\displaystyle\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{T}_{1}\texttt{)}\,\texttt{<:}\,\texttt{(}\texttt{S}_{2}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}$
$\displaystyle\Longleftrightarrow$
$\displaystyle\texttt{S}_{1}\texttt{<:}\texttt{S}_{2}~{}\mbox{ and
}~{}\texttt{T}_{1}\texttt{<:}\texttt{T}_{2}$ (3)
$\displaystyle\texttt{S}_{1}\texttt{<:}\texttt{S}_{2}~{}\mbox{ and
}~{}\texttt{T}_{1}\texttt{<:}\texttt{T}_{2}$ $\displaystyle\Longrightarrow$
$\displaystyle\texttt{S}_{1}\texttt{\&}\texttt{T}_{1}\,\texttt{<:}\,\texttt{S}_{2}\texttt{\&}\texttt{T}_{2}$
(4) $\displaystyle\texttt{S}_{1}\texttt{<:}\texttt{S}_{2}~{}\mbox{ and
}~{}\texttt{T}_{1}\texttt{<:}\texttt{T}_{2}$ $\displaystyle\Longrightarrow$
$\displaystyle\texttt{S}_{1}\texttt{|}\texttt{T}_{1}\,\texttt{<:}\,\texttt{S}_{2}\texttt{|}\texttt{T}_{2}$
(5) S<:T $\displaystyle\Longleftrightarrow$ not(T)<:not(S) (6)

However she is not required to be able to decide subtyping for every possible
pair of types, since this requires a knowledge deeper than the few above rules
(as an aside, notice that the rules (2)–(6) are not enough to deduce the
subtyping relation in (1): technically one says that the above set of rules
provides a sound but incomplete axiomatization of the subtyping
relation111111* To deduce such a kind of relations one should also use axioms
such as the following ones (excerpted from [BDCdL95])
$\displaystyle(\texttt{S}\texttt{-{}->}\texttt{T})\texttt{\&}(\texttt{S}\texttt{-{}->}\texttt{U})$
<: S\-->T&U (7)
$\displaystyle(\texttt{S}\texttt{-{}->}\texttt{U})\texttt{\&}(\texttt{T}\texttt{-{}->}\texttt{U})$
<: S|T\-->U (8) The reader may try as an exercise to prove that both the
relations in (7) (8) above and their converse hold [EX2].). The problem of
deciding subtyping between two generic types is a task for the language
designer and implementer. This is the one who must implement the algorithms
that not only check the containment of two generic types, but also generate
informative error messages that explain the programmer the reasons why some
containment she used does not hold. In Section 4 I will explain for the
language designer how to do it.

###  2.3. Intersections, overloading, and dispatching

The cognoscente reader will have recognized in the intersection of arrow types
such as
$(\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1})\,\texttt{\&}\,(\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2})$
the type typical of overloaded functions: a function of this type returns
results of different types according to the type of its argument. Strictly
speaking, an overloaded function is a function that executes different code
for arguments of different types: the semantics of the function is
“overloaded” since formed of different semantics each corresponding to a
different piece of code. The only function we have seen so far with an
intersection type—i.e., succ—is not really “overloaded” since it always
executes the same code both for arguments in Even and for arguments in Odd. In
this case it would be more correct to speak of _behavioral type refinement_
since intersections of arrows do not correspond to different pieces of code
(each implementing different functions all denoted by the same operator) but,
instead, they provide a more precise description of the function
behavior.121212* Such a usage of intersection types is known—in my opinion,
somehow misleadingly—as _coherent overloading_ : see Section 1.1.4 in [Pie91].
However Perl 6 allows the programmer to define “real” overloaded functions by
giving multiple definitions of the same function prefixed by the multi
modifier:

     multi sub sum(Int $x, Int $y) { $x + $y }
     multi sub sum(Bool $x, Bool $y) { $x && $y }

Here the sum function has two different definitions: one for a pair of integer
parameters (in which case it returns their sum) and one for a pair of Boolean
parameters (in which case it returns their logical “and” denoted in Perl by
`&&`). For instance, sum(37,5) returns 42 and sum(True,False) returns False.
Clearly, the function sum above has the following type

$(\texttt{(}\texttt{Int}\,\texttt{,}\,\texttt{Int}\texttt{)}\texttt{-{}->}\texttt{Int})\
\texttt{\&}\
(\texttt{(}\texttt{Bool}\,\texttt{,}\,\texttt{Bool}\texttt{)}\texttt{-{}->}\texttt{Bool}),$
(9)

which states that if the function is applied to a pair of integers, then it
returns integer results, and that if it is applied to a pair of Boolean
arguments it returns Boolean results. The actual code to be executed is chosen
at run-time according to the type of the actual parameters.

Although in the case above both parameters are taken into account to select
the code, it is clear that checking the type of just one parameter—e.g., the
first one—would have sufficed. So I could have equivalently written the sum
function in a _curried_ 131313 In mathematics and computer science, _currying_
is the technique of transforming a function that takes multiple arguments (or
a tuple of arguments) in such a way that it can be called as a chain of
functions, each with a single argument. version I call sumC:

     multi sub sumC(Int  $x){ sub (Int  $y){$x + $y } }
     multi sub sumC(Bool $x){ sub (Bool $y){$x && $y} }

The syntax above makes it clear that only the type of the parameter $x is used
to select the code, while the second parameter is just an argument to be
passed to the function returned by the selection. Perl 6 provides a very handy
double-semicolon syntax “;;” to distinguish parameters that are used for the
selection of a multi-function (those on the left of “;;”) from those that are
just passed to the selected code (those on the right of “;;”). So by using the
syntactic sugar “;;”, the code above can be “equivalently” rewritten
as:141414* Strictly speaking this and the previous definition of sumC are not
equivalent since the first application is curried and therefore it must be fed
by one argument at a time (e.g., sumC(3)(39)) while in the latter it is not,
so it receives all the arguments at once (e.g., sumC(3,39)): the second
notation forbids partial application. Here I just focus on the types and not
on the particular syntax, so I will sweep such differences under the carpet.

     multi sub sumC(Int $x ;; Int $y) { $x + $y }
     multi sub sumC(Bool $x ;; Bool $y) { $x && $y }

The type of the sum function has changed since in both multi definitions
(either curried or with“;;”) sumC has type:

$({\texttt{Int}}\texttt{-{}->}({\texttt{Int}}\texttt{-{}->}\texttt{Int}))\
\texttt{\&}\
(\texttt{Bool}\texttt{-{}->}(\texttt{Bool}\texttt{-{}->}\texttt{Bool})).$ (10)

The functions of this type are different from those of the type in (9): the
type in (9) is the set of all functions that when applied to a pair of
integers return an integer and when applied to a pair of Booleans they return
a Boolean. The functions in the type of (10) are functions that when applied
to an integer return a function from integers to integers, and when applied to
a Boolean they return a function from Booleans to Booleans.

Currying requires some care when all arguments are necessary to select the
code to execute. Imagine that I wanted to add the code to handle the cases
when the two arguments are of different types and that, therefore, I added two
extra multi definitions for sum, which is then defined in the following
(weird) recursive way:

     multi sub sum(Int $x, Int $y) { $x + $y }
     multi sub sum(Bool $x, Bool $y) { $x && $y }
     multi sub sum(Bool $x, Int $y) { sum($x , $y>0) }
     multi sub sum(Int $x, Bool $y) { sum($y , $x) }

As a consequence sum has now the following type (the reader is invited to
check the typing as an exercise [EX3])

$\begin{array}[]{rcl}&&(\texttt{(}\texttt{Int}\,\texttt{,}\,\texttt{Int}\texttt{)}\texttt{-{}->}\texttt{Int})\\\\[-1.13809pt]
&\texttt{\&}&(\texttt{(}\texttt{Bool}\,\texttt{,}\,\texttt{Bool}\texttt{)}\texttt{-{}->}\texttt{Bool})\\\\[-1.13809pt]
&\texttt{\&}&(\texttt{(}\texttt{Bool}\,\texttt{,}\,\texttt{Int}\texttt{)}\texttt{-{}->}\texttt{Bool})\\\\[-1.13809pt]
&\texttt{\&}&(\texttt{(}\texttt{Int}\,\texttt{,}\,\texttt{Bool}\texttt{)}\texttt{-{}->}\texttt{Bool}).\end{array}$
(11)

If, as we did with the previous version, we want define a variant of this
function that _dispatches_ (i.e., performs the selection) only on the first
argument, then every selection for the first argument must return a nested
multi function that will dispatch on the second argument. That is, we are
looking for a function sumC of the following type:

$\begin{array}[]{rcl}&&(\texttt{Int}\;\texttt{-{}->}\;((\texttt{Int}\texttt{-{}->}\texttt{Int})\
\texttt{\&}\ (\texttt{Bool}\texttt{-{}->}\texttt{Bool})))\\\\[-0.85358pt]
&\texttt{\&}\\!\\!\\!\\!&(\texttt{Bool}\texttt{-{}->}((\texttt{Bool}\texttt{-{}->}\texttt{Bool})\
\texttt{\&}\ (\texttt{Int}\texttt{-{}->}\texttt{Bool})))\end{array}$ (12)

The type above is the type of functions that when they are applied to an
integer return another function of type (Int-->Int) & (Bool-->Bool) and that
when they are applied to a Boolean return another function of type
(Bool-->Bool) & (Int-->Bool). In other terms they are functions that can be
applied to a sequence of two arguments of type Int or Bool: if the first
argument is an integer, then the result of the double application will be of
the same type as the type of the second argument; if the first argument is a
Boolean, then also the result will be a Boolean.151515 By equation (8) and the
exercise in Footnote 11, the type in (12) is equivalent to:
$(\texttt{Int}\;\texttt{-{}->}\;((\texttt{Int}\texttt{-{}->}\texttt{Int})\
\texttt{\&}\ (\texttt{Bool}\texttt{-{}->}\texttt{Bool})))\ \texttt{\&}\
(\texttt{Bool}\texttt{-{}->}((\texttt{Bool}\texttt{|}\texttt{Int})\texttt{-{}->}\texttt{Bool}));$
prove it as an exercise [EX4].

How is a function of the type in (12) defined? In particular how can we define
sumC—the curried version of the second definition of sum—which should have
this type? A first attempt consists in defining two auxiliary multi functions
sumI and sumB that perform the dispatch on the second argument of sumC and
that are called according to whether the first argument of sumC is an integer
(sumI) or a Boolean (sumB), respectively:

     multi sub sumI(Int $y ;; Int $x){ $x + $y }
     multi sub sumI(Bool $y ;; Int $x) { sumC($y,$x)}
     multi sub sumB(Bool $y ;; Bool $x) {  $x && $y }
     multi sub sumB(Int $y ;; Bool $x) { sumC($x,$y>0) }
     multi sub sumC(Int $x ;; Int|Bool $y) { sumI($y,$x) }
     multi sub sumC(Bool $x ;; Int|Bool $y) { sumB($y,$x) }

In a nutshell, sumC calls sum _X_($y,$x) where _X_ is either I or B according
to whether the first argument of sumC is of type Int or Bool. When called,
each sum _X_ subroutine dispatches to the appropriate code according to the
type of its first argument, that is, the second argument of the calling sumC.
This technique gives us a definition of sumC with the expected behavior but
not the expected type. The first multi definition of sumC has type
$\texttt{Int}\;\texttt{-{}->}\;(\texttt{Int}\texttt{|}\texttt{Bool})\texttt{-{}->}(\texttt{Int}\texttt{|}\texttt{Bool})$
(notice in particular that the second argument has a union type), while the
second multi definition of sumC has type
$\texttt{Bool}\texttt{-{}->}(\texttt{Int}\texttt{|}\texttt{Bool})\texttt{-{}->}\texttt{Bool}$.
Thus the whole sumC function has type (see also Footnote 9):

$\begin{array}[]{rcl}&&(\texttt{Int}\;\texttt{-{}->}\;(\texttt{Int}\texttt{|}\texttt{Bool})\texttt{-{}->}(\texttt{Int}\texttt{|}\texttt{Bool}))\\\\[-0.85358pt]
&\texttt{\&}\\!\\!\\!\\!&(\texttt{Bool}\texttt{-{}->}(\texttt{Int}\texttt{|}\texttt{Bool})\texttt{-{}->}\texttt{Bool})\vspace{-.5mm}\end{array}$
(13)

and this type is less precise than (i.e., it is a supertype of) the type in
(12) (see also the type in Footnote 15 that is equivalent to the (12) type).
For instance, the type in (12) states that when a function of this type is
applied to two arguments of type Int, then the result will be of type Int,
while the type in (13) states, less precisely, that the result will be of type
Int|Bool.

The solution to define a version of sumC that has the type in (12) is not so
difficult: instead of defining separate auxiliary functions (to which the
second argument of sumC must be explicitly passed as an argument) I will use
nested multi subroutines. Unfortunately Perl 6 does not allow the programmer
to write anonymous multi functions. But if we suppose that anonymous multi
functions were allowed (e.g., by considering anonymous multi definitions in
the same block to define the same anonymous function—a suggestion to the
designers of Perl), then the correspondence between the following definition
of sumC and the type in (12) should be, I think, pretty clear:

     multi sub sumC(Int $x){
             multi sub (Int $y) { $x + $y }
             multi sub (Bool $y) { sumC($y)($x) }
           }
                                                                           (14)
     multi sub sumC(Bool $x){
             multi sub (Bool $y) { $x && $y }
             multi sub (Int $y) {sumC($x)($y>0)}
           }

This code states that sumC is a multi-subroutine formed by two definitions
each of which returns as result another (anonymous) multi-subroutine.161616
Although the code (2.3) cannot be executed in Perl 6 because of the absence of
anonymous multi-subroutines, it can be faked by non-anonymous multi-
subroutines as follows:
multi sub sumC(Int $x){
multi sub foo(Int $y) { $x + $y }
multi sub foo(Bool $y) { sumC($y)($x) }
&foo
}
multi sub sumC(Bool $x){
multi sub foo(Bool $y) { $x && $y }
multi sub foo(Int $y) {sumC($x)($y>0)}
&foo
}
where &foo is Perl’s notation to return the subroutine named foo.

I have not done anything new here. As it will be clear later on, to define the
code in (2.3) I just applied the “double dispatching” technique proposed by
Ingalls in 1986 at the first OOPSLA conference [Ing86], though I doubt that
anybody at the time saw it as a special case of currying in the presence of
intersection types: as a matter of fact, it is not so straightforward to see
that the type in (12) is the curried version of the type in (11) (the code in
(2.3) is actually a “proof”—in the sense of [BCL91]—that currying is the
relation between the type in (12) and the one in (11)).

###  2.4. Formation rules for multi-subroutines

In order to conclude the discussion about multi-subroutines I have to give
some more details about how their “dynamic dispatch” is performed. When I
first introduced multi-subroutines I said that the code to execute was chosen
at run-time according to the type of the actual parameter: this is called
_dynamic dispatch_ , since the argument of the function is _dispatched_ to the
appropriate code _dynamically_ , that is, at run-time. However, in all the
examples I showed so far delaying the choice of the code until run-time does
not seem a smart choice since in all of them it is possible to choose the code
at compile time according to whether the arguments are Booleans or Integers.
In other terms, the examples I gave are not conceptually different from
operator overloading as found in Algol 68 where it is resolved at static time
(i.e., during the compilation). Of course, making the dispatch at run-time is
computationally much more expensive than making it at compile time. Therefore,
dynamic dispatch is useful and justified only if the selection of the code may
give at run time a result different from the one that would be obtained at
compile time, that is to say, if the type of function arguments may evolve
during the computation. In statically-typed languages171717 In a typed
programming language, types can be checked either at compile-time or a run-
time. Languages that check types at compile time are called statically-typed
languages, while those that check types at run-time are said to be dynamically
typed. A combination of static and dynamic type-checking is also possible. In
this work I focus on how to define static type-checking for Perl, which
currently is dynamically typed. this happens in the presence of a subtyping
relation: without subtyping an expression in a statically-typed language must
have the same type the whole computation long; with a subtyping relation,
instead, the type of an expression may change during the computation, notably
decrease:

> _In a statically-typed language with subtyping, the type of the expression
> occurring at a given point of a program may decrease during the
> computation._

This is the reason why in the presence of subtyping it is sensible to
distinguish between the _static_ and _dynamic_ type of an expression, the
former being the type of the expression at compile time, the latter the type
that this expression has after being completely evaluated.

As a simple example take the successor function I defined at the beginning of
this presentation and apply it to, say, (3+2):

      (sub(Int $x){$x+1})(3+2)

At compile time the function in the expression above has type Int-->Int (i.e.,
the usual type of the successor function) while the argument has type Int
(i.e., the type of the application of the plus operator to two integers);
therefore the whole expression has (static) type Int. The first step of
execution computes the argument expression to 5; the type of the argument has
thus decreased from Int to Odd, while the whole application has still type Int
(the application of a function of type Int-->Int to an argument of type Odd
has type Int). The second step of execution computes the application and
returns 6: the type of the whole expression has just decreased from Int to
Even.

Now that we have seen that in Perl 6 types may dynamically evolve, let us see
an example of how to use dynamic dispatch. For instance, we can define the sum
of two integers modulo 2 as follows.

multi sub mod2sum(Even $x , Odd $y) { 1 } multi sub mod2sum(Odd $x , Even $y)
{ 1 } (15) multi sub mod2sum(Int $x , Int $y) { 0 }

When mod2sum is applied to a pair of integers, then the most specific
definition that matches the (dynamic) types of the arguments is selected. So
if the argument is a pair composed by an even and an odd number then,
according to their order, either the first or the second branch is selected.
If the integers are instead both even or both odd, then only the last
definition of mod2sum matches the type of the argument and thus is selected.
Since in general it is not possible to determine at compile time whether an
integer expression will evaluate to an even or an odd number, then a selection
delayed until runtime is the only sensible choice. Let us study the type of
mod2sum. Obviously, the function has type (Int , Int)-->Int. However, it is
easy to deduce for this function a type much more precise. First, notice that
the subset construction allows the programmer to define types that contain
just one value. For instance the singleton type Two that contains only the
value “2” is defined as:

       subset Two of Int where { $_ = 2 }.

Let me adopt the convention to use the same syntax to denote both a value and
the singleton type containing it. So I will use 2 rather than Two to denote
the above singleton type. More generally, for every value _v_ of type T in the
language I assume the following definition as given

       subset _v_ of T where { $_ = _v_ }.

With the above conventions, it is easy to deduce for mod2sum the type (Int ,
Int)-->0|1, that is, the type of a function that when applied to a pair of
integers returns either 0 or 1. But a slightly smarter type system could
deduce a much more informative type:

$\tt\begin{array}[]{cl}&(\texttt{(}\texttt{Even}\,\texttt{,}\,\texttt{Odd}\texttt{)}\texttt{-{}->}\texttt{1})\\\\[-1.13809pt]
\texttt{\&}\\!\\!\\!\\!\\!&(\texttt{(}\texttt{Odd}\,\texttt{,}\,\texttt{Even}\texttt{)}\texttt{-{}->}\texttt{1})\\\\[-1.13809pt]
\texttt{\&}\\!\\!\\!\\!\\!&(\texttt{(}\texttt{Int}\\!\,\texttt{,}\,\\!\texttt{Int}\texttt{)}\texttt{-{}->}\texttt{0}\texttt{|}\texttt{1})\end{array}$
(16)

First of all, notice that if in the last arrow of the intersection above we
had specified just 0 as return type, then this would have been an error.
Indeed, mod2sum does _not_ have (Int , Int)-->0 type: it is not true that when
mod2sum is applied to a pair of integers it always returns 0. But the type
checker can be even smarter and precisely take into account the code selection
policy. The code selection policy states that the code that is selected is the
most specific one that is compatible with the type of the argument(s). Since
the first two multi definitions of mod2sum in (15) are more specific (i.e.,
they have smaller input types) than the third and last multi definition, then
the code in this last multi definition will be selected only for arguments
whose types are not compatible with the first two multi definitions. That is,
this last definition will be selected only for pairs of integers that are
neither in (Odd , Even) nor in (Even , Odd). So a smarter type checker will
deduce for mod2sum the following type:181818*** Yet another caveat for my
fellow type theorists. The sloppiness hinted at by Footnote 9 does not apply
here: even though the third multi definition of mod2sum is declared for (Int ,
Int) arguments, we can consider all the multi expressions of mod2sum as
forming a single definition that contains all the information needed to deduce
the type (17). This is similar to what happens when typing pattern-matching
expressions, where the types of the capture variables of a pattern are
computed by taking into account the patterns that are matched before it.

$\tt\begin{array}[]{cl}&(\texttt{(}\texttt{Even}\,\texttt{,}\,\texttt{Odd}\texttt{)}\texttt{-{}->}\texttt{1})\\\\[-1.13809pt]
\texttt{\&}\\!\\!\\!\\!\\!&(\texttt{(}\texttt{Odd}\,\texttt{,}\,\texttt{Even}\texttt{)}\texttt{-{}->}\texttt{1})\\\\[-1.13809pt]
\texttt{\&}\\!\\!\\!\\!\\!&((\texttt{(}\texttt{Int}\\!\,\texttt{,}\,\\!\texttt{Int}\texttt{)}\texttt{\&}\texttt{not}\texttt{(}\texttt{Even}\\!\,\texttt{,}\,\\!\texttt{Odd}\texttt{)}\texttt{\&}\texttt{not}\texttt{(}\texttt{Odd}\\!\,\texttt{,}\,\\!\texttt{Even}\texttt{)})\texttt{-{}->}\texttt{0})\end{array}$
(17)

This type is strictly more precise than (i.e., it is a strict subtype of) the
type in (16) (as an exercise [EX5], we invite the reader to find a function
value that is in the type in (16) and not in type in (17)). Actually the type
is so precise that it completely defines the function it types. Indeed it is
easy by some elementary set-theoretic reasoning to see that (Int ,
Int)&not(Even , Odd)&not(Odd , Even) is equivalent to (i.e., it denotes the
same set of values as) the type (Even , Even)|(Odd , Odd). Equally easy is to
see that for every type $\texttt{T}_{1}$, $\texttt{T}_{2}$, S, the type
$\texttt{T}_{1}\texttt{|}\texttt{T}_{2}\texttt{-{}->}\texttt{S}$ is equivalent
to
$(\texttt{T}_{1}\texttt{-{}->}\texttt{S})\texttt{\&}(\texttt{T}_{2}\texttt{-{}->}\texttt{S})$,
since every function in the former type has both the arrow types in the
intersection, and vice versa (_cf._ the exercise of Footnote 11). By applying
these two equivalences to (17) (in particular to the last factor of the top-
level intersection) we obtain that (17) is equivalent to

$\tt\begin{array}[]{rcl}&&(\texttt{(}\texttt{Even}\,\texttt{,}\,\texttt{Odd}\texttt{)}\texttt{-{}->}\texttt{1})\\\\[-1.13809pt]
&\texttt{\&}\\!\\!\\!&(\texttt{(}\texttt{Odd}\,\texttt{,}\,\texttt{Even}\texttt{)}\texttt{-{}->}\texttt{1})\\\\[-1.13809pt]
&\texttt{\&}\\!\\!\\!&(\texttt{(}\texttt{Odd}\,\texttt{,}\,\texttt{Odd}\texttt{)}\texttt{-{}->}\texttt{0})\\\\[-1.13809pt]
&\texttt{\&}\\!\\!\\!&(\texttt{(}\texttt{Even}\,\texttt{,}\,\texttt{Even}\texttt{)}\texttt{-{}->}\texttt{0})\end{array}$
(18)

from which it is easy to see that this last type is the most precise type we
can deduce for mod2sum. Before proceeding, let me stop an instant to answer a
possible doubt of the reader. The reader may wonder whether it is permitted to
apply a function of type (18) (equivalently, of type (17)) to an argument of
type (Int , Int): as a matter of fact, no arrow in (18) has (Int , Int) as
domain. Of course it is permitted: the _domain_ of a function typed by an
intersection of arrows is the _union_ of the domains of all the arrows. In the
specific case the union of the domains of the four arrows composing (18) is
(Even , Odd)|(Odd , Even)|(Odd , Odd)|(Even , Even), that is, (Int , Int). So
a function with type (18) can be applied to any argument whose type is (a
subtype of) (Int , Int). The precise rule to type such an application is
explained later on.

####  2.4.1. Ambiguous selection

Dynamic dispatch does not come for free. Besides the cost of performing code
selection at run-time, dynamic dispatch requires a lot of care at static time
as well, which is the whole point here. In particular, dynamic dispatch
introduces two new problems, those of _ambiguous selection_ and of _covariant
specialization_. In order to illustrate them I must better describe how
dynamic selection is performed at runtime. I said that always the most
specific code is selected. This is the code of the multi expression whose
parameter types best approximate the types of the arguments. In practice
consider a function defined by $n$ multi expressions—call them _branches_ —,
the $i$-th branch being defined for inputs of type $\texttt{T}_{i}$. Apply
this function to an argument that evaluates to a value of type T. The possible
candidates for the selection are all the branches whose input type
$\texttt{T}_{i}$ is a supertype of T. Among them we choose the one defined for
the least $\texttt{T}_{i}$, that is, the most specific branch.

Of course, the system must verify—possibly at compile time—that whenever the
function is applied to an argument in the function domain, then a most
specific branch will always exist. Otherwise we bump into an ambiguous
selection problem. For instance, imagine that in order to spare a definition I
decided to write the function mod2sum in the following (silly) way:

$\begin{array}[]{l}\texttt{{\tt{\color[rgb]{.275,.51,.705}\definecolor[named]{pgfstrokecolor}{rgb}{.275,.51,.705}multi
sub }}}\texttt{mod2sum(Even \$x , Int \$y)\char 123\relax \$y \% 2 \char
125\relax}\\\
\texttt{{\tt{\color[rgb]{.275,.51,.705}\definecolor[named]{pgfstrokecolor}{rgb}{.275,.51,.705}multi
sub }}}\texttt{mod2sum(Int \$x , Odd \$y)\char
123\relax\;\,(\$x+1)\;\%\;2\;\,\char 125\relax}\end{array}$ (19)

If the first argument is even, then we return the second argument modulo 2; if
the second argument is odd, then we return the successor of the first argument
modulo 2. While from a mathematical viewpoint this definition is correct,
computationally this definition is problematic since it may lead an ambiguous
dynamic selection. Let _e_ be an expression of type Int, then mod2sum(_e_ ,1)
is well-typed (a static selection would choose the code of the second branch).
But if _e_ reduces to an even number, then both codes can be applied and there
is not a branch more specific than the other: according to the current Perl
semantics the execution is stuck.191919* Two solutions alternative to being
stuck are to choose one of the two branches either at random or according to a
predetermined priority. Both solutions are compatible with the typing
discipline we are describing in this work (and with the silly definition (19))
but they are seldom used: the use of some priority corresponds to using _class
precedence lists_ in object-oriented languages with multiple inheritance
(e.g., this is what is used in Common Lisp Object System), while I am not
aware of any language that uses random selection. Clearly such a problem can
and must be statically detected (though, current implementations of Perl 6
detect it only at run-time). This can be done quite easily as explained
hereafter. Consider again our silly definition (19) of mod2sum which is
composed by two branches (i.e., pieces of code) one for inputs of type (Even ,
Int), the other for inputs of type (Int , Odd). Consider the intersection of
these two types, (Even , Int) & (Int , Odd), which is equal to (Even , Odd).
The function mod2sum can be applied to values in this intersection, but there
does not exist a most specific branch to handle them. In order to avoid
selection ambiguity, we have to perform systematically such a check on the
intersections of the input types, as stated by the following definition:
[Ambiguity] Let _$\texttt{T}_{h}$_ denote the input type of the $h$-th branch
of a multi-subroutine composed of $n$ branches. The multi-subroutine is _free
from ambiguity_ if and only if for all $i$, $j\in[1..n]$ and $i\not=j$, either
_$\texttt{T}_{i}\texttt{\ &}\texttt{T}_{j}$_ is empty (i.e.,
_$\texttt{T}_{i}\texttt{\
&}\texttt{T}_{j}\texttt{<:}\texttt{not(}\texttt{Any}\texttt{)}$_), or the set
_$\\{\texttt{T}_{h}\mid\texttt{T}_{i}\texttt{\
&}\texttt{T}_{j}\texttt{<:}\texttt{T}_{h},h\in[1..n]\\}$_ has a unique least
element.202020 The condition of uniqueness ensures that all the
$\texttt{T}_{h}$ are (semantically) distinct. In words, although we must test
that for all possible types of the arguments, there always exists a most
specific branch, in practice it suffices to test such existence for the types
that are a non-empty intersection of the input types of two distinct branches.
A compiler must reject any multi-subroutine that is not free of ambiguity.

Ambiguity freedom is a formation condition for the definition of multi-
subroutines that constrains the input types of the various branches and
ensures that the computation will never be stuck on a selection. It is
important to understand that _this is not a problem related to the type
system_ , but just a problem about giving the semantics of multi-subroutine
definitions. The type system has no problem of having functions of type

( (Even,Int) --> 0|1 ) & ( (Int,Odd) --> 0|1 ) (20)

which, intuitively, is the type that corresponds to the multi subroutine in
(19): a function of this type can be applied to arguments of type (Int , Int)
and the result will be given the type `0|1`; the definition of mod2sum given
at the beginning of Section 2.4 has indeed this type. The problem only occurs
when there are two multi _definitions_ with parameters (Even , Int) and (Int ,
Odd) since they make the run-time selection (thus, the semantics) of the
multi-subroutine undefined. In [Cas95] I explained how the problem of
ambiguity corresponds in object-oriented languages to the problem of method
selection with multiple inheritance: I invite the interested reader to refer
to that work for more information.

####  2.4.2. Overriding

In order to ensure the soundness of the type system (i.e., that all type
errors will be statically detected) we must impose a second condition on the
definition of multi-subroutines, which constrains the return types of the
branches. We have already seen that since types evolve along the computation,
so does the selection of the branches. For instance, take again the original
definition of mod2sum as I defined it in (15). If we apply the function to a
pair of expressions of type Int—e.g., mod2sum(3+3,3+2)—, then the compiler
statically deduces that the third branch will be selected. But if the pair of
expressions reduces to a pair composed of, say, an even and an odd
number—e.g., mod2sum(6,5)–, then at run-time the code of the first branch will
be executed. Now, different branches may have different return types. This is
clearly shown by the functions sum and sumC which in the first version I gave
for them are formed of two branches returning different types (Int and Bool
for the former, and Int-->Int and Bool-->Bool for the latter, as respectively
stated by the types in (9) and (10)). Since the selected branch may change
along the computation, so can the corresponding return type, that is, the type
of the application. Type soundness can be statically ensured only if the type
of every expression decreases with the computation. Why is it so? Imagine that
a function f with input type Int is applied to an expression of type Int.
Before performing the application we evaluate the argument. Therefore the
value returned at runtime by this expression must be of type Int or of a
smaller type, say Even, but not of a distinct type such as Bool, since the
function f expects arguments of type Int, not of type Bool. This must hold
also when the argument of f is the result of the application of a multi-
subroutine, which implies that if the branch selected for the multi-subroutine
changes along the computation, then the newly selected branch must have a
return type smaller than or equal to the return type of the previously
selected branch. Consider now a multi-function with $n$ branches (as in
Definition 19) whose $i$-th branch has input type $\texttt{T}_{i}$ (for $1\leq
i\leq n$), apply it to an argument, and statically determine that the selected
branch is the $h$-th one. What are the branches that can potentially be
selected at run-time? Since the type of the argument cannot but decrease along
the computation, then the candidates for selection are all the branches whose
input type is a subtype of $\texttt{T}_{h}$. These are the branches that
_specialize_ (I will also say _override_ or _refine_) the branch
$\texttt{T}_{h}$ and, as can be evinced by the discussion above, soundness is
ensured only if the return types of these branches are smaller than or equal
to the return type of the $h$-th branch. This yields the following definition.
[Specialization] Let _$\texttt{T}_{h}$_ and _$\texttt{S}_{h}$_ respectively
denote the input type and the return type of the $h$-th branch of a multi-
subroutine composed of $n$ branches. The multi-subroutine is _specialization
sound_ if and only if for all $i$, $j\in[1..n]$, _$\texttt{T}_{i}\texttt{
<:}\texttt{T}_{j}$_ implies _$\texttt{S}_{i}\texttt{ <:}\texttt{S}_{j}$_. In
words, the return type of each branch must be smaller than or equal to the
return type of all the branches it specializes.

Definition 2.4.2 for specialization-soundness is, as Definition 19 for
ambiguity-freedom, a formation rule for programs in Perl 6. These rules
concern more the definition of the language, than its type theory. As the type
system has no problem to have a type of the form as in (20) which intersects
two arrows whose domains have a common lower bound, so the type system has no
problem in considering functions of type:

$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$
(21)

even if the return type of the arrow with the smaller domain is not smaller
than the other return type. We will return on this type later on. For the time
being, notice that while ambiguity-freedom is needed to ensure unambiguous
semantics of the programs, specialization-soundness is necessary to ensure the
soundness of the system. Thus even if both are formation rules for Perl 6
programs, specialization-soundness can be explained and justified purely in
terms of the type system. In order to do that we need to better explain how to
deduce the type of the application of a function whose type is an intersection
of arrow types to some argument in its domain. To that end let us consider
again the type in (20). This type is not very interesting since both arrows
that compose it return the same type: now we know (see Footnote 11) that
$(\texttt{S}_{1}\texttt{-{}->}\texttt{T})\texttt{\&}(\texttt{S}_{2}\texttt{-{}->}\texttt{T})$
is equivalent to
$\texttt{S}_{1}\texttt{|}\texttt{S}_{2}\texttt{-{}->}\texttt{T}$ and therefore
(20) is equivalent to a single arrow without intersections (i.e.,
((Even,Int)|(Int,Odd))-->(0|1)). In order to make the type more interesting
let us modify it by using two distinct output types whose intersection and
union are non trivial. For instance, let us consider the following type:

((Even,Int)-->(0,Int)) & ((Int,Odd)-->(Int,1)) (22)

A function of this type accepts any pair of integers that is not in
(Odd,Even): the domain of the function is the union of the domains of the
arrows, that is (Even,Int)|(Int,Odd); if we use “\” to denote set-theoretic
difference (i.e., S\T is syntactic sugar for S&not(T)) then this type is
equivalent to (Int,Int)\\(Odd,Even). The type in (22) specifies that if the
first projection of the argument of a function of this type is even, then the
first projection of the result will be 0, and if the second projection of the
argument is odd, then the second projection of the result will be 1. A simple
example of a function with this type is the function that maps $(x,y)$ to
$(x\,\mathbf{mod}\,2,y\,\mathbf{mod}\,2)$.

Let us now examine all the possible cases for an application of a function of
the type in (22). According to the type of the argument of the function, four
different cases are possible:

  1. (1)

The argument is of type (Even,Odd): both arrows _must_ apply; the first arrows
tell us that the first projection of the result will be 0, while the second
arrow tell us that the second projection will be 1; so we deduce the result
type (0,1), that is the intersection of the result types;

  2. (2)

The argument is of type (Even,Even): then only the first arrow applies and we
deduce the type (0,Int);

  3. (3)

The argument is of type (Odd,Odd): then only the second arrow applies and we
deduce the type (Int,1);

  4. (4)

The argument is of type (Int,Int)\\(Odd,Even) (i.e., we just know that it is
in the domain of the function): both arrows _may_ apply; since we do not know
which one will be used then we take the union of the result types, that is,
(0,Int)|(Int,1).

We can generalize this typing to the application of functions of a generic
type

$\tt(\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1})\,\texttt{\&}\,(\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2})$
(23)

to an argument of type T. Only four cases are possible:212121 There is a
mildly interesting fifth case when the type T of the argument is empty, that
is when the argument is statically known to diverge.

  1. (1)

If the argument is in $\texttt{S}_{1}\texttt{\&}\texttt{S}_{2}$ (i.e., if
$\texttt{T}\texttt{<:}\texttt{S}_{1}\texttt{\&}\texttt{S}_{2}$), then the
application has type $\texttt{T}_{1}\texttt{\&}\texttt{T}_{2}$.

  2. (2)

If the argument is in $\texttt{S}_{1}$ and case 1 does not apply (i.e.,
$\texttt{T}\texttt{<:}\texttt{S}_{1}$ and $\texttt{T}\texttt{\char
92\relax}\texttt{S}_{2}$ is not empty), then the application has type
$\texttt{T}_{1}$.

  3. (3)

If the argument is in $\texttt{S}_{2}$ and case 1 does not apply (i.e.,
$\texttt{T}\texttt{<:}\texttt{S}_{2}$ and $\texttt{T}\texttt{\char
92\relax}\texttt{S}_{1}$ is not empty), then the application has type
$\texttt{T}_{2}$.

  4. (4)

If the argument is in $\texttt{S}_{1}\texttt{|}\texttt{S}_{2}$ and no previous
case applies, then the application has type
$\texttt{T}_{1}\texttt{|}\texttt{T}_{2}$.

Of course things become more complicated with functions typed by an
intersection of three or more arrows: the complete formalization of the typing
of their applications is outside the scope of this primer and it will be given
in Section 4. But an intersection of two arrows is all we need to explain the
specialization soundness rule. So let us consider the type in (23) and suppose
that, say, $\texttt{S}_{2}\texttt{<:}\texttt{S}_{1}$. What happens when we
apply a function of this type to an argument of type $\texttt{S}_{2}$? Since
$\texttt{S}_{2}\texttt{<:}\texttt{S}_{1}$ then
$\texttt{S}_{2}\,\texttt{<:}\,\texttt{S}_{1}\texttt{\&}\texttt{S}_{2}$,
therefore it is the first of the four possible cases that applies: the
argument is in $\texttt{S}_{1}\texttt{\&}\texttt{S}_{2}$ and thus the result
will be of type $\texttt{T}_{1}\texttt{\&}\texttt{T}_{2}$ (…which is smaller
than $\texttt{T}_{2}$).

Let us rephrase what we just discovered: if we have a function of type

$(\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1})\,\texttt{\&}\,(\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2})$

with $\texttt{S}_{2}\texttt{<:}\texttt{S}_{1}$, and we apply it to an argument
of the smaller type, that is $\texttt{S}_{2}$, then the result will be in
$\texttt{T}_{1}\texttt{\&}\texttt{T}_{2}$. The fact that $\texttt{T}_{2}$ is
not smaller than $\texttt{T}_{1}$ does not matter because the typing rules
tell us that the application of this function to an argument of type
$\texttt{S}_{2}$ will return a result in a type smaller than $\texttt{T}_{1}$.

Let us consider a concrete example for $\texttt{S}_{i}$, $\texttt{T}_{i}$ by
going back to the type in (21). A function is of type
$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$
_only if_ for arguments of type Even it returns results in Odd&Int, that is in
Odd: although the arrow with domain Even does not specify a result type
smaller than the one for the arrow of domain Int, the typing rules ensure that
all the results will be included in the latter type. In the previous sentence
I italicized “only if” to stress its importance, since this is a point that
may lead to confusion. For instance, the function foo defined as:

       multi sub foo(Int $x) { 3 }
       multi sub foo(Even $x){ $x % 3 }

does _not_ have type
$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$,
despite the fact that the first branch returns an odd number when applied to
an integer and that the second branch returns an integer when applied to an
even number (recall that “ % ” is the modulo operator, so the result of
applying “ % 3” to an Even number can be either odd or even). The function foo
does not have this intersection type because when it is applied to an argument
of (static) type Int, it may return a result that is Even rather than Odd. For
an example of that consider foo(foo(8)): if foo were of type
$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$,
then the type deduced for foo(foo(8)) would be Odd (8 is of type Even, so
foo(8) is of type Int and, thus, foo(foo(8)) is of type Odd), but the
application would return 2 (both the inner and the outer application of foo
return 2). The definition above of foo has (just) type
$\texttt{Int}\to\texttt{Int}$; for foo to have type
$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$,
the second branch of foo should always return a result in Odd.

In the view of what I just wrote, I can next show that Definition 2.4.2 is, as
for the condition of ambiguity, just a formation rule and _not a problem
related to the type system_. It is a design choice that ensures that the type
of a well-typed multi definition is what a programmer expects it to be.
Consider a definition of the form

       multi sub bar($\texttt{S}_{1}$ $x) returns $\texttt{T}_{1}$ { ... }
       multi sub bar($\texttt{S}_{2}$ $x) returns $\texttt{T}_{2}$ { ... }

In Perl 6 the returns keyword declares the result type of a subroutine. In the
example above, it declares that the first definition has type
$\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$ and the second one type
$\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2}$. If each definition is well
typed, then the programmer expects the function bar defined the multi
definitions above to have type
($\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$)&($\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2}$).
Suppose that $\texttt{S}_{2}\texttt{<:}\texttt{S}_{1}$. In this case the
typing rules state that a function has type
($\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$)&($\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2}$)
only if whenever it is applied to an argument of type $\texttt{S}_{2}$ it
returns a result in $\texttt{T}_{1}\texttt{\&}\texttt{T}_{2}$. By the
semantics of multi definitions, if bar is applied to an argument of type
$\texttt{S}_{2}$, then it executes the second definition of bar and,
therefore, it returns a result in $\texttt{T}_{2}$. Putting the two
observations together we conclude that bar has type
($\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$)&($\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2}$)
if and only if
$\texttt{T}_{2}\,\texttt{<:}\,\texttt{T}_{1}\texttt{\&}\texttt{T}_{2}$ and—by
a simple set-theoretic reasoning—if and only if
$\texttt{T}_{2}\texttt{<:}\texttt{T}_{1}$: exactly the condition enforced by
Definition 2.4.2.

To say it otherwise: the type system does not have any problem in managing a
type of the form
($\texttt{S}_{1}\texttt{-{}->}\texttt{T}_{1}$)&($\texttt{S}_{2}\texttt{-{}->}\texttt{T}_{2}$)
even if $\texttt{S}_{1}$<:$\texttt{S}_{2}$ and $\texttt{T}_{1}$ and
$\texttt{T}_{2}$ are not related. However, such a type might confuse the
programmer since a function of this type applied to an argument of type
$\texttt{S}_{1}$ returns a result in $\texttt{T}_{1}$&$\texttt{T}_{2}$. In
order to avoid this confusion the language designer can (without loss of
generality) force the programmer to specify that the return type for a
$\texttt{S}_{1}$ input is (some subtype of) $\texttt{T}_{1}$&$\texttt{T}_{2}$.
This can be obtained by accepting only specialization sound definitions and
greatly simplifies the presentation of the type discipline of the language.
Let me show this again on the function foo I defined earlier in this section.
As said, the type deduced for its current defintion is Int-->Int. A definition
with explicit return types as

       multi sub foo(Int $x) returns Odd { 3 }
       multi sub foo(Even $x)returns Int { $x % 3 }

would be rejected for the reason that it is not specialization sound since the
second branch must return subtype of Odd, and Int is not one: this
justification is simpler than explaining that the function has not type
$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$
for the reason that the second branch does not always return an odd result. If
I modify the second branch so that it always returns odd numbers, but I do not
change the type annotations:

       multi sub foo(Int $x) returns Odd { 3 }
       multi sub foo(Even $x)returns Int { ($x+1) % 4 }

then the specialization sound policy would reject also this definition, for
the same reason as the previous one, even though now foo is of type
$(\texttt{Int}\texttt{-{}->}\texttt{Odd})\;\texttt{\&}\;(\texttt{Even}\texttt{-{}->}\texttt{Int})$.
But, once more, this is probably easier for the programmer to understand than
the fact that for every application in which the second branch is selected the
deduced type would be Odd rather than Int.

This concludes the presentation of the primer on type theory. In this section
I have introduced substantial type-theoretic concepts and explained them in
terms of the set-theoretic interpretation of types. We have seen how the set-
theoretic interpretation of types allows us to deduce non-trivial subtyping
relations on complex types. I have also tried to distinguish concepts that
concern the semantics of the language, such as the two conditions on the
definition of multi-subroutines, from the type-theoretic concepts that explain
and justify them. It is now time to put all we have learnt so far in practice
and apply it to understand and solve a controversy that has been the core of a
heated debate in the object-oriented languages community for several years in
the late eighties, early nineties: the so-called “covariance vs.
contravariance problem”.

###  2.5. Lessons to retain

For the busy programmer who did not have time to read this long section, all I
explained here can be summarized by the following six simple rules:

  1. (1)

Types are sets of values. In particular:

    1. (a)

the type S\-->T is the set of all functions that when applied to values in S
return only results in T;

    2. (b)

union, intersection, and negation types are the sets of values obtained by
applying the corresponding set operations.

  2. (2)

S is a subtype of T if and only if all values in S belong also to T.

  3. (3)

Two types are equal if they are the same set of values.

  4. (4)

A multi-subroutine is typed by the intersection of the types of each multi
definition; but, for that to hold, these definitions must satisfy the property
of covariant specialization (Definition 2.4.2)

  5. (5)

When a multi-subroutine is applied to an argument, the most precise multi
definition for that argument is used; but, for that to happen, the definitions
that compose the multi subroutine must be free from ambiguity (Definition 19).

  6. (6)

The definition of a subroutine in which only some arguments are used for code
selection (the “;;” notation) corresponds to defining a function whose
parameters are those preceding the “;;” and that returns another function
whose parameters are those following the “;;”.

##  3\. The covariance and contravariance (false) problem

If I have not disgusted my average programmer reader, yet, she should have
acquired enough acquaintance with types and dynamic dispatching to be ready to
tackle what in the study of object-oriented languages is called _the
covariance vs. contravariance problem_. Since this controversy took place in
the object-oriented community, I therefore start explaining it by using Perl 6
objects and then reframe it in the context introduced in the previous section.
I assume the reader to be familiar with the basic concepts of object-oriented
programming.

###  3.1. Objects in Perl 6

The classic example used in the late eighties to explain the problem at issue
was that of programming a window system in which the basic objects were
pixels, represented by the class Point written in Perl 6 as:

     class Point {
         has $.x is rw;
         has $.y is rw;

         method origin() {
             ($.x==0)&&($.y==0)
         }

         method move(Int $dx, Int $dy) {
             $.x += $dx;
             $.y += $dy;
             return self;
         }
     };

Objects (or _instances_) of the class Point have two _instance variables_
(_fields_ , in Java parlance) x and y, and two methods associated to the
messages origin and move, respectively. The former takes no argument and
returns whether the receiver point has null coordinates or not, the latter
takes two integers, modifies the instance variables of the receiver of the
message move (i.e., the _invocant_ of the method move, in Perl parlance), and
returns as result the receiver itself, which in Perl 6 is denoted by the
keyword self. New instances are created by the class method new. Methods are
invoked by sending the corresponding message to objects, by dot notation. For
example,

      my Point $a = Point.new(x => 23, y => 42);
      $a.move(19,-19);

creates an instance of the class Point whose instance variables have values 23
and 42 and then moves it by inverting the values of the instance variables.
Notice that in the definition of $a (first line of our code snippet: in Perl,
my is the keyword to define a variable in the current block) the name Point
has a double usage: while the second occurrence of Point denotes a _class_ (to
create a new instance) the first occurrence is a _type_ (to declare the type
of $a). In our set-theoretic interpretation the _type_ Point denotes the set
of all the objects that are instances of the _class_ Point.

If later we want to extend our window system with colors (in late eighties
black and white screens were the norm), then we define _by inheritance_ a
subclass ColPoint that adds a c field of type string (in Perl, Str) for the
color and a method iswhite, it _inherits_ the fields x and y and the method
origin from Point, and, finally, it _specializes_ (or _overrides_) the method
move of Point so that white colored points are not modified.

     class ColPoint is Point {
         has Str $.c is rw;

         method iswhite() {
             return ($.c=="white");
         }

         method move(Int $dx, Int $dy) {
             if not(self.iswhite()) {
                $.x += $dx;
                $.y += $dy;
             }
             return self;
         }
     };

In many object-oriented languages, Perl 6 included, inheritance is associated
with subtyping: declaring a subclass by the keyword is, as in the example
above, has the double effect of making the new class definition inherit the
code of the super-class definition _and_ of declaring the type of the objects
of the subclass to be a subtype of the type of the objects of the super-class.
In our example it declares ColPoint to be a subtype of Point. Therefore every
object of type/class ColPoint is also of type Point and, as such, it can be
used wherever a Point object is expected. For instance, the following code

     my Point $a = ColPoint.new(x=>2,y=>21,c=>"white");
     $a.move(3,3);

is legal and shows that it is legitimate to assign a ColPoint object to a
variable $a declared of type Point. Notice that, even though $a has static
type Point, it is dynamically bound to an object of type/class ColPoint and,
therefore, the code executed for `$a.move` will be the one defined in the
class ColPoint. In particular, during the execution of this method, the
message iswhite will be dynamically sent to (the object denoted by) `$a` even
though `$a` has static type Point, for which no iswhite method is defined (the
wordings “ _dynamic dispatch_ ” and “ _dynamic binding_ ” come from there). On
the contrary, an invocation such as `$a.iswhite()` will (or, rather, should,
since current implementations of Perl 6 do not check this point) be statically
rejected since `$a`, being of type Point, cannot in general answer to the
message iswhite, and it is in general out of reach of a type system to
determine at static time whether $a will be bound to a ColPoint or not
(although in this particular case it is pretty obvious).

###  3.2. Inheritance and subtyping

Since the objects of a subclass can be used where objects of the super-class
are expected, then definitions by inheritance must obey some formation rules
to ensure type soundness. This is sensible for overridden methods: while it is
harmless to add new instance variables or methods in a subclass,
specialization of methods requires the use of a subtype. The reasons for this
is that, as an object of a subclass can be used where an object of the super-
class is expected, so the overriding method of the subclass can be used where
the overridden method of the super-class is expected. This is clearly shown by
the code snippet $a.move(3,3) I wrote a few lines above: since $a is of
(static) type Point, then the type system assumes that the message move will
execute the method defined in the class Point, which expects a pair of
integers and returns a Point (i.e., it is a function of type (Int ,
Int)-->Point), even though in reality it is the method in the definition of
ColPoint that is used instead. Using the latter definition where the former is
expected is type safe since the type of the method in ColPoint is a subtype of
the type of the method in Point: rule (2) states that (Int , Int)-->ColPoint
<: (Int , Int)-->Point, and indeed $a.move(3,3) will return a color point,
that is, a value of a subtype of the expected Point type.

##### Contravariant overriding:

In general, to ensure type safety, when in a definition by inheritance we
specialize (i.e., override) a method the new method must have a subtype of the
type of the original method. By the co-/contra-variant rule in (2) this means
that the return type of the new method must be a subtype of the return type of
the old method (covariant specialization) while its arguments must have a
supertype of the type of the arguments of the old method (contravariant
specialization). Since the latter is taken as characteristics of this kind of
specialization, the whole rule has taken the name of _contravariant
overriding_.

##### Covariant overriding:

So far so good. Troubles start when one considers _binary methods_ , that is
methods with arguments of the same type as the type of the receiver [BCC+96].
The paradigmatic example is the equal method which, for the class Point, can
be defined as follows.

     class Point {
         has $.x is rw;
         has $.y is rw;

         method equal(Point $p) {
             ($.x==$p.x)&&($.y==$p.y)
         }
     };

When later we introduce the ColPoint class it is natural to want to redefine
the method equal so as $(i)$ it takes arguments of type ColPoint and $(ii)$ it
compares also the colors, that is:

     class ColPoint is Point {
         has Str $.c is rw;

         method equal(ColPoint $p) {
             ($.x==$p.x)&&($.y==$p.y)&&($.c==$p.c)
         }
     };

This is called _covariant_ specialization, since in the subclass a method
overrides the previous definition of the method by using parameters whose
types are subtypes of the types of the corresponding parameters in the
overridden method. Unfortunately, the definition above (and covariant
specialization in general) is unsound as shown by the following snippet which
is statically well typed but yields a type error at run-time:

     my Point $a = ColPoint.new(x=>2,y=>21,c=>"white");
     my Point $b = Point.new(x=>2,y=>21);
     $a.equal($b);

The code above passes static type-checking: in the first line a ColPoint
object is used where a Point instance is expected—which is legitimate—; in the
second line we simply create a new object; while in the last line we send the
message equal to the object $a with argument $b: since $a is (statically) a
Point object, then it is authorized to send to it the message equal with a
Point argument. However, at run-time $a is bound to a color point and by,
dynamic binding, the method in the definition of ColPoint is used. This tries
to access the c instance variable of the argument $b thus yielding a run-time
error: the static type system is unsound.222222* For Perl 6 purists. Since
Perl 6 performs dynamic type checking, then the run-time error actually
happens at the call of the equal method rather than at its execution. Here I
described the behaviour shown when types are checked only at compile time,
since a sound static type checking makes dynamic type checking useless. Also
notice that, for the sake of simplicity, I used “==” (rather than “eq” as
required in Perl) for the string equality operator.

To have soundness and use color points where points are expected the type of
the parameter of the equal method in ColPoint must be either Point or a
supertype of it.

Despite this problem, covariant overriding had (has?) its strenuous defenders
who advocated that they wanted both to use color points where points were
expected and to define an equal method that compared color points with other
color points and not just with points. The various solutions proposed (perform
a dynamic check for method arguments—as in O2—, adopt covariant specialization
despite its unsoundness—as in Eiffel—or simply do not care about parameter
types in overriding methods—as in Perl 6) were all incompatible with static
soundness of the type system (or, as for LOOM [BPF97], they gave up subtyping
relation between Point and ColPoint). Thus contravariant overriding and
covariant specialization looked as mutually exclusive typing disciplines for
inheritance, and the dispute about the merits and demerits of each of them
drifted towards a religious war. In what follows I will use the type theory we
learned in the primer contained in Section 2 to argue that covariance and
contravariance are not opposing views, but distinct concepts that can coexist
in the same object-oriented language. But first I have to transpose the whole
discussion in the setting of Section 2 where objects were absent. This is
quite easy since if we abstract from some details (e.g., encapsulation,
implementation, access), then the object-oriented part of Perl 6 is all
syntactic sugar.

###  3.3. It is all syntactic sugar

Consider a class definition in Perl 6. It is composed of two parts: the part
that describes the class’s objects (i.e., the fields that compose them) and
the part that describes the operations on the class objects (i.e., the
methods). Methods are nothing but functions associated to a name (the message)
and with an implicit parameter denoted by self. Thus a method such as the one
defined for move in class Point is a function with 3 parameters, one of type
Point (denoted by self) and two of type Int. As a matter of fact, if we write:

      my Point $a = Point.new(x => 23, y => 42);
      $a.move();

Perl 6 complains by

$\texttt{Not enough positional parameters passed; got 1 but expected 3},$

since in the second line of the above code it detected the point argument $a
of move, but the two integer arguments are missing. Now, if we consider a
single message, such as move, then it is associated to different function
definitions (the methods in Point and ColPoint for move) and the actual code
to execute when a message such as move is sent is chosen according to the type
of the receiver of the message, that is, according to the type of the methods’
hidden argument. In Section 2 we already saw that functions with multiple
definitions are called multi subroutines, and that the arguments used to
choose the code are those listed before the “;;” (if it occurs) in the
parameter list.

If we remove method definitions from classes and replace them by multis where
the receiver parameter has become an explicit parameter, then we cannot
observe any difference from an operational point of view. In other terms we
can rewrite the first two class definitions of Section 3.1 as follows and
obtain something that is observationally equivalent

      class Point {
         has $.x is rw;
         has $.y is rw;
      };

      multi sub origin(Point $self) {
         ($self.x==0)&&($self.y==0)
      };

      multi sub move(Point $self ;; Int $dx, Int $dy) {
         $self.x += $dx;
         $self.y += $dy;
         return $self;
      };

      class ColPoint is Point {
         has Str $.c is rw;
      };

      multi sub iswhite(ColPoint $self) {
         return ($self.c=="white");
      };

      multi sub move(ColPoint $self ;; Int $dx, Int $dy) {
         if not(iswhite($self)) {
            $self.x += $dx;
            $self.y += $dy;
         }
         return $self;
      };

Notice that class definitions now contain only instance variable declarations.
In practice, classes have become record types (i.e., respectively _hashes_ and
_structures_ in Perl and C) whose subtyping relation is explicitly
defined.232323* Technically, in this case one speaks of _name_ subtyping,
insofar as we _declared_ ColPoint to be a subtype of Point. Method definitions
are external to class definitions and have become multi subroutines enriched
with an extra parameter $self whose type is used to select the code to execute
and, as such, it is separated from the other parameters by “;;”. Finally,
method invocation has become function application. This is shown by the body
of the method move for ColPoint where the method invocation self.iswhite() has
been transformed into iswhite($self).

The transformation we just defined tells us that from a point of view of types
the two class definitions at the beginning of Section 3.1 are equivalent to
defining two (record) types Point and ColPoint (the latter subtype of the
former) and three multi-subroutines respectively of type:

    origin:  Point-->Bool
    iswhite: ColPoint-->Bool
    move:    (Point-->((Int , Int)-->Point)) & (ColPoint-->((Int , Int)-->ColPoint))

The formation rules of multi-subroutines are satisfied, specifically for move
where

ColPoint<:Point

requires by Definition 2.4.2 that ((Int , Int)-->ColPoint)<:((Int ,
Int)-->Point). Since the latter holds, then the above definitions—thus, the
class definitions at the beginning of Section 3.1—are type sound.

If we apply the same transformation to the equal method we obtain

      multi sub equal(Point $self ;; Point $p) {
        ($self.x==$p.x)&&($self.y==$p.y)  };

      multi sub equal(ColPoint $self ;; ColPoint $p) {
        ($self.x==$p.x)&&($self.y==$p.y)&&($self.c==$p.c)};

The definitions above define a function equal that _should_ have the following
type:

$\begin{array}[]{rcl}\texttt{equal:}\\!\\!\\!\\!&&(\texttt{Point}\texttt{-{}->}(\texttt{Point}\texttt{-{}->}\texttt{Bool}))\\\
&{\texttt{\&}}\\!\\!\\!\\!\\!\\!&(\texttt{ColPoint}\texttt{-{}->}(\texttt{ColPoint}\texttt{-{}->}\texttt{Bool}))\end{array}$
(24)

However, the two multi definitions yield a function that does not have this
type inasmuch as they do not comply with the specialization formation rule:
since ColPoint<:Point, then by Definition 2.4.2 we need
(ColPoint-->Bool)<:(Point-->Bool) which _by contravariance_ does not hold.
Thus the definition is unsound. An equivalent way to see this problem is that
a function equal is of the type in (24) only if when applied to a ColPoint
object it returns a value in the following intersection type:

$(\texttt{Point}\texttt{-{}->}\texttt{Bool})\texttt{\&}(\texttt{ColPoint}\texttt{-{}->}\texttt{Bool})$
(25)

(_cf._ the first of the cases listed right after equation (23) and the
discussion thereby); but the multi definitions above—in particular the second
multi definition of equal—do not (the second definition does not have type
Point-->Bool and, _a fortiori_ , it does not have the intersection above).

So far we did not learn anything new since we already knew that the definition
above was not sound. If however in the definition of the multi subroutine
equal we separate the two parameters by a “,” rather than a “;;”, that is

      multi sub equal(Point $self , Point $p) {
        ($self.x==$p.x)&&($self.y==$p.y)  };

      multi sub equal(ColPoint $self , ColPoint $p) {
        ($self.x==$p.x)&&($self.y==$p.y)&&($self.c==$p.c) };

then the definition becomes well typed, with type

$\begin{array}[]{rcl}\texttt{equal:}\\!\\!\\!\\!&&(\texttt{(}\texttt{Point}\,\texttt{,}\,\texttt{Point}\texttt{)}\texttt{-{}->}\texttt{Bool})\\\
&{\texttt{\&}}\\!\\!\\!\\!\\!\\!&(\texttt{(}\texttt{ColPoint}\,\texttt{,}\,\texttt{ColPoint}\texttt{)}\texttt{-{}->}\texttt{Bool})\end{array}$
(26)

In particular, the specialization formation rule of Definition 2.4.2 is now
satisfied: since we have (ColPoint , ColPoint)<:(Point , Point), then this
requires Bool<:Bool, which clearly holds. So the definition of equal is now
sound: where is the trick? The consequence of replacing “,” for “;;” is that
the new version of equal uses the dynamic types of _both_ arguments to choose
the code to execute. So the second definition of equal is selected only if
both arguments are (dynamically) instances of ColPoint. If any argument of
equal is of type Point, then the first definition is executed. For instance,
the method invocation $a.equal($b) I gave in Section 3.2 to show the
unsoundness of covariant specialization now becomes equal($a,$b); and since
the dynamic type of $b is also used to select the code to execute, then when
this type is Point the first definition of the multi subroutine equal is
selected.

With hindsight the solution is rather obvious: this transformation tells us
that it is not possible to choose the code for binary methods, such as equal,
by using the type of just one parameter (i.e., the type of the receiver); the
only sound solution is to choose the code to execute based on the types of
both arguments.

Finally, observe that we are not obliged to check the type of both arguments
at the same time: we can first check one argument and then, if necessary
(e.g., for equal if the first argument is a ColPoint), check the other. This
tells us how to solve the problem in the original setting, that is where
methods are defined in classes: it suffices to use multi subroutines also for
methods. In Perl 6 this is obtained by adding the modifier multi in front of a
method definition. This yields a solution in which the definition of the class
Point does not change:

     class Point {
         has $.x is rw;
         has $.y is rw;

         method equal(Point $p) {
             ($.x==$p.x)&&($.y==$p.y)
         }
     };

while the class ColPoint now defines a “multi method” for equal:

     class ColPoint  is Point {
         has Str $.c is rw;

         multi method equal(Point $p) {
             ($.x==$p.x)&&($.y==$p.y)
         }

         multi method equal(ColPoint $p) {
             ($.x==$p.x)&&($.y==$p.y)&&($.c==$p.c)
         }
     };

The body of the equal method with a ColPoint parameter is as before. We just
added an extra method in the class ColPoint to handle the case in which the
argument of equal is a Point, that is, it is an argument that was statically
supposed to be compared with another Point: in this case we do not check the c
instance variable. In words, if equal is sent to a Point, then the method
defined in Point is executed; if equal is sent to a ColPoint, then the type of
the argument is used to select the appropriate multi method.

While the type of equal defined in Point is Point-->Bool (as it was before),
the type of equal in ColPoint is now the intersection type
(Point-->Bool)&(ColPoint-->Bool). The latter is a subtype of the former
(obviously, since for all types S, T, we have S&T<:S). So at the end we did
not discover anything really new, since it all sums up to using the old
classic rule for subclassing:

> Overriding rule: the type of an overriding method must be a subtype of the
> type of the method it overrides

The only novelty is that now intersection types give us the possibility to
have some form of covariant specialization: in a class D subclass of a class C
we can safely override a method of type C-->S by a new method of type
(C-->S)&(D-->T) where the code associated to D-->T represents the covariant
specialization of the old method.

Two concluding remarks on the Point-ColPoint example. First, notice that the
type of equal in ColPoint is exactly the type we found in (25), that is, the
type suggested by the intersection type theory for the overriding method.
Hence, if we abstract from the “syntactic sugar” of the objects and we
consider methods as multi-subroutines with implicit parameters, then the last
two classes define a multi-subroutine equal that has type (24), the type we
were looking for. Second, it is worth noticing that the solution based on
multi methods is modular. The addition of the class ColPoint does not require
any modification of the class Point, and a class such as Point can be defined
independently of whether it will be later subclassed with a covariant method
specialization or not.242424* Interestingly, the same behaviour as the
solution above can be obtained simply by adding the modifier multi to the
method equal in Point to the definitions given in Section 3.2, since in that
case the (multi) method of Point is not overridden in ColPoint:
class Point {
has $.x is rw;
has $.y is rw;
multi method equal(Point $p) {
($.x==$p.x)&&($.y==$p.y)
}
};
class ColPoint is Point {
has Str $.c is rw;
multi method equal(ColPoint $p) {
($.x==$p.x)&&($.y==$p.y)&&($.c==$p.c)
}
}; however this solution is less modular than the one above since it may
require to modify the definition of Point when the class ColPoint is added at
a later time.

Excursus. In the preceding example the method that must be added to handle
covariant specialization is explicitly defined by the programmer. However, it
is possible to imagine a different solution in which this “missing” method is
instead added by the compiler. All the method added by the compiler has to do
is to call the overridden method (i.e., to dispatch the message to “super”).
The choice of whether the method added to handle covariant specialization is
to be written by the programmer or inserted by the compiler, is a choice that
concerns language design. The reader can refer to [BC97] and [BC96] to see how
the second choice can be implemented in Java and O2, respectively.

To summarize, we have just seen how the type theory we studied in Section 2
allows us to propose a solution to the covariant specialization of methods.
Although the rule for subclassing is still the usual one—you can override
methods only by methods of smaller type—, the presence of intersection types
tells us that it is fine to covariantly specialize a method as long as we do
it by a multi-method that dynamically handles the case in which the argument
has a supertype of the expected type (i.e., an argument that was intended for
the overridden method). Although the detailed explanation of how we arrived to
this solution is to some degree convoluted, the solution for the final
programmer amounts to retaining the _Overriding Rule_ I stated above and to be
able to apply it when complex types are involved, in particular when functions
are typed by intersection types. This is the reason why it is important for a
programmer to grasp the basic intuition of the subtyping relation and, in that
respect, the set-theoretic interpretation of types as sets of values should
turn out to be, I believe, of great help.

###  3.4. Lessons to retain

As for the previous section, I summarize for the busy programmer the content
of this section in two rules:

  1. (1)

The type of an overriding method must be a subtype of the type of the method
it overrides, whether these types are arrows or intersections of arrows.

  2. (2)

As a consequence of the previous point, it is sound to covariantly specialize
a method as long as we do it by a multi-method in which at least one
definition can handle arguments intended for the overridden method.

##  4\. Type algorithms for the language designer (i.e., the electrical
blueprints)

In this section I am going to describe the algorithms and data-structures
needed to implement the type system of the previous section. I will give a
bare description of the algorithms and data-structures and justify them just
informally. Detailed justifications and proof of formal properties such as
correctness can be found in the references commented in Section 5.

I will proceed first by defining the algorithm that decides whether two types
are in subtyping relation as defined in Definition 8. Next I will describe the
data structures used to efficiently implement types and their operations.
Then, I will describe the typing of expressions, focusing on those that are
more difficult to type, namely, subroutines, projections, applications, and
classes. I conclude the section with the algorithms for records whose
presentation is quite technical and can be skipped at first reading.

###  4.1. Type syntax

But first I must define the types I will be working with. These are the types
defined in Section 2.1 with two slight improvements: more precise base types
and recursive types.

More precisely I replace Bool and Int respectively by “tags” (ranged over by
$t$) and “intervals”, two base types that cover a wide range of possible
implementations. This yields the following grammar

$\texttt{T}::=\textit{t}\,\mid\,\texttt{[$i$..$j$]}\,\mid\,\texttt{Any}\,\mid\,\texttt{(}\texttt{T}\,\texttt{,}\,\texttt{T}\texttt{)}\,\mid\,\texttt{T}\texttt{-{}->}\texttt{T}\,\mid\,\texttt{T}\texttt{|}\texttt{T}\,\mid\,\texttt{T}\texttt{\&}\texttt{T}\,\mid\,\texttt{not(}\texttt{T}\texttt{)}$

An interval is denoted by [$i$..$j$] where $i$ and $j$ are numeric constants
or “*” (which denotes infinite). For instance, [2..4] is the type that denotes
the set $\\{$2, 3, 4$\\}$, [1..*] is the type of positive integers, while Int
now becomes a shorthand for [*..*]. A tag is a sequence of letters starting by
a back-quote, such as or , that denotes a user-defined value and are akin to
Perl’s “barewords” (actually, barewords are deprecated in Perl). When used as
a type, a tag denotes the singleton containing that tag. In particular, I can
encode Bool as the union of two tag types, |. The remaining types have the
same interpretation as before. Tags, intervals, products and arrows are called
_type constructors_ , while unions, intersections, and negations are called
_type connectives_. I will use Empty to denote the type not(Any), and
$S\setminus T$ to denote the set-theoretic difference of two sets $S$ and $T$
(i.e., $S\cap\neg T$).

To cope with recursive types, I will consider the set of possibly infinite
syntax trees generated by the grammar above (in technical jargon, it is the
language “coinductively” produced by the grammar) that satisfy the following
two conditions: $(a)$ they are _regular_ trees (i.e., each tree has finitely
many distinct subtrees) and $(b)$ on every infinite branch of a tree there are
infinitely many occurrences of product or arrow type constructors (these two
conditions are called “contractivity conditions”). The first restriction
ensures that recursive types have a finite representation (e.g., finite sets
of equations or recursive definitions). The second restriction ensures that
recursion always traverses at least one type _constructor_ , thus barring out
ill-formed types such as $\texttt{T}=\texttt{T}\texttt{|}\texttt{T}$ (which
does not carry any information about the set of values it denotes) or
$\texttt{T}=\texttt{not(}\texttt{T}\texttt{)}$ (which cannot represent any
set). A consequence of the second restriction is also that we can express only
finite unions and intersections.

The reader disconcerted by infinite trees can consider, instead, the following
inductive definition of types, that contains an explicit term for recursive
definitions and that is equivalent to the previous definition stated in terms
of infinite trees:

$\displaystyle\\!\textbf{Atoms}\ \ a$
$\displaystyle\\!\\!\\!\\!\\!\\!\\!::=\\!\\!\\!\\!\\!\\!\\!$
$\displaystyle\textit{t}\,\mid\,\texttt{[$i$..$j$]}\,\mid\,\texttt{(}\texttt{T}\,\texttt{,}\,\texttt{T}\texttt{)}\,\mid\,\texttt{T}\texttt{-{}->}\texttt{T}$
(26) Types T $\displaystyle\\!\\!\\!\\!\\!\\!\\!::=\\!\\!\\!\\!\\!\\!\\!$
$\displaystyle
a\,\mid\,X\,\mid\,\texttt{rec\,}X\texttt{\,=\,}a\,\mid\,\texttt{T}\texttt{|}\texttt{T}\,\mid\,\texttt{T}\texttt{\&}\texttt{T}\,\mid\,\texttt{not(}\texttt{T}\texttt{)}\,\mid\,\texttt{Any}\qquad$
(27)

Although this last definition is probably easier to understand, I will mainly
work with the one with infinite trees (since it yields simpler formulations of
the algorithms and is closer to actual implementation) and will reserve the
recursive types notation for the examples. Nevertheless, the last definition
is important because it clearly separates type constructors (i.e., the meta-
operators that construct atoms252525 We call them atoms in analogy to
propositional logic, since they are the building blocks on which the logical
connectives of union, intersection, and negation are applied (note that the
our arrows _do not_ denote logical implication).) from type connectives and
shows that there are four different kinds of constructors: tags, intervals,
products, and arrows. An important property that I will use in what follows is
that for each of these four kinds it is possible to define a top type that
contains all and only the types of the same kind, namely.

  1. (1)

(Any , Any) is the greatest product type. It contains all the pairs of values.
I use $\texttt{Any}_{\texttt{\tiny prod}}$ to denote it.

  2. (2)

Empty\-->Any is the greatest function type. It contains all the functions. I
use $\texttt{Any}_{\texttt{\tiny arrw}}$ to denote it.

  3. (3)

[*..*] (i.e., Int) is the largest interval. It contains all the integers. I
use $\texttt{Any}_{\texttt{\tiny ints}}$ to denote it.

  4. (4)

$\texttt{not(}\texttt{Any}_{\texttt{\tiny
prod}}\texttt{|}\texttt{Any}_{\texttt{\tiny
arrw}}\texttt{|}\texttt{Any}_{\texttt{\tiny ints}}\texttt{)}$ contains all the
tag values. I use $\texttt{Any}_{\texttt{\tiny tags}}$ to denote it.

A final consideration before describing the subtyping algorithm. Types are
possibly infinite trees that denote possibly infinite sets of values, but the
theory presented here accounts only for _finite_ values: there is not such a
value as, say, an infinite list. So while the type rec$\,X\,$= |(Int , $X$) is
the type of the finite lists of integers, the type rec$\,X\,$= (Int , $X$) is
the empty type.

###  4.2. Subtyping algorithm

The key property the subtyping algorithm is based on, is that types are sets.
Since subtyping is set-containment, then the algorithm uses classic set-
theoretic transformations to simplify the problem. For instance, to prove that
$\texttt{(}\texttt{T}_{1}\\!\,\texttt{,}\,\texttt{T}_{2}\texttt{)}\texttt{\&}\texttt{(}\texttt{S}_{1}\\!\,\texttt{,}\,\texttt{S}_{2}\texttt{)}$
is empty (i.e.,
$\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}\texttt{\&}\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{S}_{2}\texttt{)}\texttt{<:}\texttt{Empty}$),
the algorithm uses set-theoretic equivalences and decomposes the problem into
simpler subproblems, namely:
$\texttt{(}\texttt{T}_{1}\\!\\!\,\texttt{,}\,\\!\texttt{T}_{2}\texttt{)}\texttt{\&}\texttt{(}\texttt{S}_{1}\\!\\!\,\texttt{,}\,\\!\texttt{S}_{2}\texttt{)}$
is empty if and only if
$\texttt{(}\texttt{T}_{1}\texttt{\&}\texttt{S}_{1}\\!\,\texttt{,}\,\texttt{T}_{2}\texttt{\&}\texttt{S}_{2}\texttt{)}$
is empty, if and only if either $\texttt{T}_{1}\texttt{\&}\texttt{S}_{1}$ is
empty or ${\texttt{T}_{2}\texttt{\&}\texttt{S}_{2}}$ is empty. With that in
mind the subtyping algorithm can be summarized in 4 simple steps.

_Step 1_ :

transform the subtyping problem into an emptiness decision problem. Deciding
whether S<:T holds is equivalent to deciding whether the difference of the two
types is empty. So the first step of the algorithm is to transform the problem
S<:T into S&not(T)<:Empty.

_Step 2_ :

put the type whose emptiness is to be decided in a disjunctive normal form.
Our types are a propositional logic whose atoms are defined by grammar (26). A
_literal_ (ranged over by $\ell$) is either an atom or the negation of an
atom: $\ell::=a\,\mid\,\texttt{not(}a\texttt{)}$. Every type is equivalent to
a type in _disjunctive normal form_ , that is, a union of intersections of
literals:

$\bigvee_{i\in I}\bigwedge_{j\in J}\ell_{ij}$

with the convention that Any and Empty are, respectively, the empty
intersection and the empty union. Therefore, the second step of the algorithm
consists in transforming the type S&not(T) whose emptiness is to be checked,
into a disjunctive normal form.

_Step 3_ :

simplify mixed intersections. The algorithm has to decide whether a
disjunctive normal form, that is, a union of intersections, is empty. A union
is empty if and only if every member of the union is empty. Therefore the
problem reduces to deciding emptiness of an intersection of literals:
$\bigwedge_{i\in I}\ell_{i}$. Notice that there are four kinds of atoms and
thus of literals, one for each type constructor. Intersections that contain
literals of different kinds can be straightforwardly simplified: if in the
intersection there are two atoms of different constructors, say,
$\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}$ and
$\texttt{S}_{1}\texttt{-{}->}\texttt{S}_{2}$, then their intersection is empty
and so is the whole intersection; if one of the two atoms is negated and the
other is not, say,
$\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}$ and
$\texttt{not(}\texttt{S}_{1}\texttt{-{}->}\texttt{S}_{2}\texttt{)}$, then the
negated atom is useless and can be removed since it contains the one that is
not negated; if both atoms are negated, then the intersection can be split in
two intersections of atoms of the same kind by intersecting the atoms with the
respective top types (e.g.,
$\texttt{not(}\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}\texttt{)}\texttt{\&}\texttt{not(}\texttt{S}_{1}\texttt{-{}->}\texttt{S}_{2}\texttt{)}$
can be split into the union of
$\texttt{not(}\texttt{(}\texttt{T}_{1}\\!\,\texttt{,}\,\texttt{T}_{2}\texttt{)}\texttt{)}\texttt{\&}\texttt{(}\texttt{Any}\\!\,\texttt{,}\,\\!\texttt{Any}\texttt{)}$
and
$\texttt{not(}\texttt{S}_{1}\texttt{-{}->}\texttt{S}_{2}\texttt{)}\texttt{\&}(\texttt{Empty}\texttt{-{}->}\texttt{Any})$).

Therefore, the third step of the algorithm performs these simplifications so
that the problem is reduced to deciding emptiness of intersections that are
formed by literals of the same kind, that is one of the following cases (where
$P$ stands for “positives” and $N$ for “negatives”):

$\displaystyle\displaystyle\bigwedge_{p\in
P}t_{p}~{}\texttt{\&}~{}\bigwedge_{n\in N}\texttt{not(}t_{n}\texttt{)}$ (27)
$\displaystyle\displaystyle\bigwedge_{p\in
P}\texttt{[$i_{p}$..$j_{p}$]}~{}\texttt{\&}~{}\bigwedge_{n\in
N}\texttt{not(}\texttt{[$i_{n}$..$j_{n}$]}\texttt{)}$ (28)
$\displaystyle\displaystyle\bigwedge_{\texttt{\scriptsize(}\mathtt{S}_{1}\texttt{\scriptsize,}\,\mathtt{S}_{2}\texttt{\scriptsize)}\in
P}\\!\\!\\!\\!\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{S}_{2}\texttt{)}\quad~{}\texttt{\&}~{}\bigwedge_{\texttt{\scriptsize(}\mathtt{T}_{1}\texttt{\scriptsize,}\,\mathtt{T}_{2}\texttt{\scriptsize)}\in
N}\\!\\!\\!\\!\texttt{not(}\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}\texttt{)}$
(29)
$\displaystyle\displaystyle\bigwedge_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\\!\\!\\!\\!({\texttt{S}_{1}}\texttt{-{}->}{\texttt{S}_{2}})\quad~{}\texttt{\&}~{}\bigwedge_{\mathtt{T}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{T}_{2}\in
N}\\!\\!\\!\\!\\!\texttt{not(}{\texttt{T}_{1}}\texttt{-{}->}{\texttt{T}_{2}}\texttt{)}$
(30)

_Step 4_ :

solve uniform intersections and recurse. At this point we have to decide
whether every intersection generated at the previous step is empty. When the
intersection is formed by atoms of base type—i.e., cases (27) and (28)—, then
emptiness can be immediately decided: an intersection as in equation (27) is
empty if and only if the same tag appears both in a positive and a negative
position (i.e., there exists $p\in P$ and $n\in N$ such that $t_{p}=t_{n}$) or
two distinct tags appear in positive position (i.e., there exists
$p_{1},p_{2}\in P$ such that $t_{p_{1}}\not=t_{p_{2}}$), while whether an
intersection as in equation (28) is empty can be decided by simple
computations on the interval bounds.

If instead the intersection is composed of products or arrows, then first we
check whether we already proved that the intersection type at issue is empty
(we have recursive types so we memoize intermediate results). If we did not,
then we memoize the type and decompose it using its set-theoretic
interpretation. Precisely, to decide emptiness of the type in (29), we
decompose the problem into checking that for all $N^{\prime}{\subseteq}N$

$\left(\bigwedge_{\texttt{\scriptsize(}\mathtt{S}_{1}\texttt{\scriptsize,}\,\mathtt{S}_{2}\texttt{\scriptsize)}\in
P}\\!\\!\\!\\!\\!\texttt{S}_{1}\;\;\texttt{<:}\\!\\!\\!\\!\\!\bigvee_{\texttt{\scriptsize(}\mathtt{T}_{1}\texttt{\scriptsize,}\,\mathtt{T}_{2}\texttt{\scriptsize)}\in
N^{\prime}}\\!\\!\\!\\!\\!\texttt{T}_{1}\right)\textsf{ or
}\left(\bigwedge_{\texttt{\scriptsize(}\mathtt{S}_{1}\texttt{\scriptsize,}\,\mathtt{S}_{2}\texttt{\scriptsize)}\in
P}\\!\\!\\!\\!\\!\texttt{S}_{2}\;\;\texttt{<:}\\!\\!\\!\\!\\!\bigvee_{\texttt{\scriptsize(}\mathtt{T}_{1}\texttt{\scriptsize,}\,\mathtt{T}_{2}\texttt{\scriptsize)}\in
N\setminus N^{\prime}}\\!\\!\\!\\!\\!\texttt{T}_{2}\right)$ (31)

holds, which is done by recursively proceeding to Step 1.

To decide emptiness of the type in (30), we decompose the problem into
checking whether there exists $\texttt{T}_{1}\texttt{-{}->}\texttt{T}_{2}\in
N$ such that
$\texttt{T}_{1}\leq\bigvee_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\texttt{S}_{1}$ and for all $P^{\prime}\subsetneq P$ (notice that
containment is strict)

$\left(\texttt{T}_{1}\quad\
\texttt{<:}\\!\\!\\!\\!\\!\bigvee_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P^{\prime}}\\!\\!\\!\\!\\!\texttt{S}_{1}\right)\textsf{ or
}\left(\bigwedge_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P\setminus
P^{\prime}}\\!\\!\\!\\!\\!\texttt{S}_{2}\;\;\texttt{<:}\quad\texttt{T}_{2}\right)$
(32)

holds, which is checked by recursively proceeding to Step 1.
[_End of the Algorithm_]

In order to complete the presentation of the algorithm above, let me show how
to define the recursive functions that compute the Boolean function defined in
(32) in Step 4. I focus on the algorithm for (32) since it is the most
difficult one and leave the case for products (31) as an exercise. Given an
atom $\texttt{T}_{1}\texttt{-{}->}\texttt{T}_{2}\in N$ I first need to check
whether
$\texttt{T}_{1}\leq\bigvee_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\texttt{S}_{1}$ and, if so, then compute a function, say, $\Phi$ that given
$\texttt{T}_{1}$, $\texttt{T}_{2}$ and $P$ checks whether for every strict
subset $P^{\prime}$ of $P$, the formula in (32) holds. The definition of
$\Phi$ is not straightforward, therefore I will introduce it gradually.

Let me first slightly simplify the problem by relaxing the strictness of the
containment: I will define a function $\Phi$ that checks (32) for every
(possibly non-strict) subset $P^{\prime}$ of $P$, that is, for $P$ too.
Indeed, notice that the requirement of strictness in $P^{\prime}\subsetneq P$
is just an optimization to avoid a useless check: we already know that for
$P^{\prime}=P$ the formula (32) is true (because
$\texttt{T}_{1}\leq\bigvee_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\texttt{S}_{1}$ holds). Therefore strictness is not needed for the
correctness the algorithm. I leave the implementation of the strictness
optimization for $\Phi$ as an exercise.

The basic idea to program the function $\Phi$ is the following: pick an
element $e$ in $P$ (the choice of $e$ can be arbitrary) and let $Q$ be
$P\setminus\\{e\\}$; then $\Phi$ does two things: $(i)$ it recursively solves
the problem for all subsets of $Q$ (i.e., the subsets of $P$ that do not
contain $e$) and $(ii)$ it recursively solves the problem for all subsets of
$Q$ to which $e$ is added (i.e., all the subsets of $P$ that contain $e$). To
avoid repeating calculations in different recursive calls, $\Phi$ keeps track
of three sets of elements of $P$: the set of elements that are still to be
selected to form some subset $P^{\prime}$ of $P$ (denoted by $P^{\circ}$); the
set of elements that were already selected to be in $P^{\prime}$ (denoted by
$P^{+}$); and the set of elements that were already selected not to be in
$P^{\prime}$ (denoted by $P^{-}$). A generic call for $\Phi$ will then be of
the form
$\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P^{\circ}\;,\;P^{+}\;,\;P^{-})$
such that $P=P^{\circ}\cup P^{+}\cup P^{-}$; such a call will pick an element
$\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}$ in $P^{\circ}$
and $(i)$ recursively solve the problem for all subsets of
$Q=P^{\circ}\setminus\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\}$
by adding the element to $P^{-}$ and thus recording that the element must not
be considered, that is
$\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;Q\;,\;P^{+}\;,\;P^{-}\cup\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\})$
and $(ii)$ recursively solve the problem for all subsets of $Q$ to which
$\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}$ is added, which is done
by adding the element to $P^{+}$, that is
$\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;Q\;,\;P^{+}\cup\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\}\;,\;P^{-})$.
In other terms, the recursive calls of
$\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P^{\circ}\;,\;P^{+}\;,\;P^{-})$
will solve the problem for all subsets of $P^{+}\cup P^{\circ}$ that contain
(at least) $P^{+}$, that is, these recursive calls will check equation (32)
for all subsets $P^{\prime}$ of $P$ such that $P^{+}\subseteq
P^{\prime}\subseteq P^{+}\cup P^{\circ}$. When $P^{\circ}$ is empty, and there
no longer is an element to pick to make the recursive calls, then $P^{+}$ is
the $P^{\prime}$ at issue and $P^{-}$ is $P\setminus P^{\prime}$. In that case
formula (32) tells us that we have to check that $\texttt{T}_{1}$ is smaller
than the union of the domains of all the arrows in $P^{+}$ and that
$\texttt{T}_{2}$ is larger than the intersection of the codomains of the
arrows in $P^{-}$. This leads to the last observation we need before giving
the actual definition of $\Phi$: we do not need to keep the whole $P^{+}$ and
$P^{-}$ sets; we just need the union of the domains for $P^{+}$ and the
intersection of the codomains for $P^{-}$. This yields the following recursive
definition of the subtyping relation for the arrow case
$\bigwedge_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}({\texttt{S}_{1}}\texttt{-{}->}{\texttt{S}_{2}})\;\texttt{<:}\;{{\texttt{T}_{1}}\texttt{-{}->}{\texttt{T}_{2}}}$:

$(\texttt{T}_{1}\;\texttt{<:}\bigvee_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\texttt{S}_{1})\;\textsf{ and
}\;\Phi(\texttt{T}_{1},\texttt{T}_{2},P,\texttt{Empty},\texttt{Any})$ (33)

where

$\begin{array}[]{l}\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;\varnothing\;,\;\texttt{D}\;,\;\texttt{C})=(\texttt{T}_{1}\texttt{<:}\texttt{D})\textsf{
or }(\texttt{C}\texttt{<:}\texttt{T}_{2})\\\\[5.69054pt]
\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\cup\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\}\;,\;\texttt{D}\;,\;\texttt{C})=\\\
\qquad\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\;,\;\texttt{D}\;,\;\texttt{C}\texttt{\&}\texttt{S}_{2}^{\circ})\textsf{
and
}\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\;,\;\texttt{D}\texttt{|}\texttt{S}_{1}^{\circ}\;,\;\texttt{C})\end{array}$

The definition $\Phi$ above is not very interesting: all it does is just to
explore the whole space of the subsets of $P$. But it becomes interesting when
we try to get rid of the two extra parameters C and D. Notice that C and D are
two accumulators respectively for the intersection of the Codomains and the
union of the Domains of the arrows singled out in the previous recursive
calls. As a matter of fact, we do not need these two extra parameters since we
can store them in the first two parameters, by using suitable set-theoretic
operations. If we define the function $\Phi^{\prime}$ as follows:

$\begin{array}[]{l}\Phi^{\prime}(\texttt{Empty}\;,\;\texttt{T}_{2}\;,\;\varnothing)=\texttt{true}\\\\[5.69054pt]
\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{Empty}\;,\;\varnothing)=\texttt{true}\\\\[5.69054pt]
\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;\varnothing)=\texttt{false}\hskip
93.89409pt\textrm{otherwise}\\\\[5.69054pt]
\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\cup\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\})=\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\texttt{\&}\texttt{S}_{2}^{\circ}\;,\;P)\textsf{
and
}\Phi^{\prime}(\texttt{T}_{1}\setminus\texttt{S}_{1}^{\circ}\;,\;\texttt{T}_{2}\;,\;P)\end{array}$

then it is not difficult to see that for all $\texttt{T}_{1}$,
$\texttt{T}_{2}$, $P$, C, and D,

$\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\;,\;\texttt{D}\;,\;\texttt{C})=\Phi^{\prime}(\texttt{T}_{1}\setminus\texttt{D}\;,\;\texttt{C}\setminus\texttt{T}_{2},P)$

and that, therefore, we can use

$(\texttt{T}_{1}\;\texttt{<:}\bigvee_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\texttt{S}_{1})\;\textsf{ and
}\;\Phi^{\prime}(\texttt{T}_{1},\texttt{not(}\texttt{T}_{2}\texttt{)},P)$ (34)

instead of (33).

I invite the reader to verify that both $\Phi$ and $\Phi^{\prime}$ compute the
Boolean function described in (32) and leave the definition of a similar
function for (31) as exercise [EX6]. In particular, I suggest trying to use
the properties
$\bigwedge_{\texttt{\scriptsize(}\mathtt{S}_{1}\texttt{\scriptsize,}\,\mathtt{S}_{2}\texttt{\scriptsize)}\in
P}\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{S}_{2}\texttt{)}=\texttt{(}\bigwedge_{\texttt{\scriptsize(}\mathtt{S}_{1}\texttt{\scriptsize,}\,\mathtt{S}_{2}\texttt{\scriptsize)}\in
P}\texttt{S}_{1}\,\texttt{,}\,\bigwedge_{\texttt{\scriptsize(}\mathtt{S}_{1}\texttt{\scriptsize,}\,\mathtt{S}_{2}\texttt{\scriptsize)}\in
P}\texttt{S}_{2}\texttt{)}$ and
$\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{S}_{2}\texttt{)}\setminus\texttt{(}\texttt{T}_{1}\,\texttt{,}\,\texttt{T}_{2}\texttt{)}=\texttt{(}\texttt{S}_{1}\setminus\texttt{T}_{1}\,\texttt{,}\,\texttt{S}_{2}\texttt{)}\texttt{|}\texttt{(}\texttt{S}_{1}\,\texttt{,}\,\texttt{S}_{2}\setminus\texttt{T}_{2}\texttt{)}$
to define an algorithm potentially more efficient. I also leave as an exercise
[EX7] the modification of $\Phi$ and $\Phi^{\prime}$ to implement the
optimization corresponding to the strict containment $P^{\prime}\subsetneq P$
when checking (32).

$\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P)$ is pretty efficient
when the subtyping relation holds, since there is no choice: all strict
subsets of $P$ must be tested. However, it does not perform any test before
emptying the parameter $P$ by a sequence of repeated recursive calls. As a
possible optimization, it may be interesting to perform some checks earlier,
when $P$ is yet not empty, thus possibly avoiding some recursive calls when
the subtyping relation does not hold. A way to do so for a generic call
$\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P^{\circ}\;,\;P^{+}\;,\;P^{-})$ is
first to check formula (32) for $P^{\prime}=P^{\circ}\cup P^{+}$ and, only if
it succeeds, then perform the two recursive calls. This corresponds to
modifying the definition of $\Phi$ as follows:

$\begin{array}[]{l}\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;\varnothing\;,\;\texttt{D}\;,\;\texttt{C})=(\texttt{T}_{1}\texttt{<:}\texttt{D})\textsf{
or }(\texttt{C}\texttt{<:}\texttt{T}_{2})\\\\[5.69054pt]
\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\cup\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\}\;,\;\texttt{D}\;,\;\texttt{C})=\\\
\qquad((\texttt{T}_{1}\texttt{<:}\texttt{S}_{1}^{\circ}\texttt{|}\texttt{D})\textsf{
or }(\bigwedge_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\\!\texttt{S}_{2}\texttt{\&}\texttt{C}\;\texttt{<:}\;\texttt{T}_{2}))\makebox[0.0pt]{\hskip
51.21495pt(*)}\\\ \qquad\textsf{and
}\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\;,\;\texttt{D}\;,\;\texttt{C}\texttt{\&}\texttt{S}_{2}^{\circ})\\\
\qquad\textsf{and
}\Phi(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\;,\;\texttt{D}\texttt{|}\texttt{S}_{1}^{\circ}\;,\;\texttt{C})\end{array}$

which yields the following modification for $\Phi^{\prime}$:

$\begin{array}[]{l}\Phi^{\prime}(\texttt{Empty}\;,\;\texttt{T}_{2}\;,\;\varnothing)=\texttt{true}\\\\[5.69054pt]
\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{Empty}\;,\;\varnothing)=\texttt{true}\\\\[5.69054pt]
\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;\varnothing)=\texttt{false}\hskip
36.98857pt\textrm{otherwise}\\\\[5.69054pt]
\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\;,\;P\cup\\{\texttt{S}_{1}^{\circ}\texttt{-{}->}\texttt{S}_{2}^{\circ}\\})=\\\
\qquad((\texttt{T}_{1}\texttt{<:}\texttt{S}_{1}^{\circ})\textsf{ or
}(\bigwedge_{\mathtt{S}_{1}\,\texttt{\scriptsize-{}->}\,\mathtt{S}_{2}\in
P}\\!\texttt{S}_{2}\texttt{<:}\;\texttt{not(}\texttt{T}_{2}\texttt{)}))\makebox[0.0pt]{\hskip
51.21495pt(*)}\\\ \qquad\textsf{and
}\Phi^{\prime}(\texttt{T}_{1}\;,\;\texttt{T}_{2}\texttt{\&}\texttt{S}_{2}^{\circ}\;,\;P)\\\
\qquad\textsf{and
}\Phi^{\prime}(\texttt{T}_{1}\setminus\texttt{S}_{1}^{\circ}\;,\;\texttt{T}_{2}\;,\;P)\end{array}$

The extra checks performed in the $(*)$-marked lines are interesting in the
case they fail, since this allows us to stop the computation of $\Phi$ and
$\Phi^{\prime}$ even when the parameter $P$ is not empty, thus potentially
saving several recursive calls. The price to pay is that when the subtyping
relation holds, the functions will perform $n$ useless checks (since they will
be done twice) where $n$ is the cardinality of $P$. But in the case of
$\Phi^{\prime}$ these useless checks have a very low cost, since they amount
to checking whether $\texttt{T}_{1}$ of $\texttt{T}_{2}$ are empty types. As
we show in the next section, checking the emptiness of a type just amounts at
checking the content of four fields in a record; this must be contrasted with
the fact that every recursive call requires to perform either an intersection
or a difference of types, which are much costlier operations.

###  4.3. Data structures and their operations

The subtyping algorithm (as well as the typing algorithm I describe further
on) works with types in disjunctive normal form, which are transformed by
applying unions, intersections, and differences. Since I want to avoid to
normalize types at each step of the algorithm, then the algorithm will work
with types stored in disjunctive normal form. Thus I need to find an efficient
representation for disjunctive normal forms and define the operations of
union, intersection, and difference so that they preserve this representation.
Recall that a type in disjunctive normal form can be represented as:

$\bigvee_{i\in I}(\bigwedge_{p\in P_{i}}a_{p}~{}\texttt{\&}\bigwedge_{n\in
N_{i}}\texttt{not(}a_{n}\texttt{)})$ (35)

where $a_{i}$’s are atoms. A naive representation of (35) (such as lists of
pairs of lists) does not fit our needs since it is not compact and makes it
difficult to efficiently implement set-theoretic operations.

##### Binary decision diagrams.

A classic technique to store compactly Boolean functions is to use Binary
Decision Diagrams (BDD). In the context I am studying a BDD is a labeled
binary tree whose nodes are labeled by atoms and whose leaves are labeled by
$\mathbb{0}$ or $\mathbb{1}$. In a BDD every path starting from the root and
terminating by $\mathbb{1}$ represents the intersection of the atoms that