chap4.tex

\chapter{The Julia approach}

\section{Core calculus}
\label{sec:corecalc}

Julia is based on an untyped lambda calculus augmented with generic functions,
tagged data values, and mutable cells.

\vspace{-3ex}
\begin{singlespace}
\begin{align*}
  e\ ::=\ &\ x                 & \textrm{(variable)} \\
        &\ |\ 0\ |\ 1\ |\ \cdots     & \textrm{(constant)} \\
        &\ |\ x = e          & \textrm{(assignment)} \\
        &\ |\ e_1; e_2       & \textrm{(sequencing)} \\
        &\ |\ e_1(e_2)       & \textrm{(application)} \\
        &\ |\ \texttt{if}\ e_1\ e_2\ e_3 & \textrm{(conditional)} \\
        &\ |\ \texttt{new}(e_{tag}, e_1, e_2, \cdots) & \textrm{(data constructor)} \\
        &\ |\ e_1.e_2        & \textrm{(projection)} \\
        &\ |\ e_1.e_2 = e_3  & \textrm{(mutation)} \\
%        &\ |\ (e)          & \textrm{(grouping)} \\
        &\ |\ \texttt{function}\ x_{name}\ e_{type}\ (x_1, x_2, \cdots)\ e_{body} & \textrm{(method definition)}
\end{align*}
\end{singlespace}

The \texttt{new} construct creates a value from a type tag and some other
values; it resembles the \texttt{Dynamic} constructor
in past work on dynamic typing \cite{Abadi:1991:DTS:103135.103138}.
The tag is determined by evaluating an expression.
%\footnote{Some agree that this qualifies as ``dynamic dependent typing''
%  (personal communication with Jean Yang, 2014). Others contend that this
%  terminology is not sensible.
%}
% TODO: say something about: it seems cumbersome to need to compute 2 parts
% for every value, but in practice it is easy to abstract away.
This means constructing types is part of programming, and types can
contain nearly arbitrary data.\footnote{We restrict this to values that can
be accurately compared by \texttt{===}, which will be introduced shortly.}
In Julia syntax, types are constructed using curly braces; this is shorthand
for an appropriate \texttt{new} expression
(tags are a specific subset of data values whose tag is the built-in value
\texttt{Tag}).
Although type expressions are quite often constants, one might also write
\texttt{MyType\{x+y\}}, to construct a \texttt{MyType} with
a parameter determined by computing \texttt{x+y}.
This provides a desirable trade-off for our intended applications:

\begin{itemize}
\item The compiler cannot always statically determine types.
\item Program behavior does not depend on the compiler's (in)ability to
determine types.
\item The compiler can do whatever it wants in an attempt to determine types.
\end{itemize}

The last point means that if the compiler is somehow able to statically
evaluate \texttt{x+y}, it is free to do so, and gain sharper type information.
This is a general property of dynamic type inference systems
\cite{kaplanullman,TICL,pticl,nimble,rubydust}.
Julia's types are designed to support this kind of inference, but they
are also used for code selection and specialization regardless of the
results of inference.

%This can be used to request specific kinds of objects from an API, or
%used as an implementation detail to tell the compiler which object
%properties to track.
In practice, \texttt{new} is always wrapped in a constructor function,
abstracting away the inconvenience of constructing both a type and a value.
In fact, \texttt{new} for user-defined data types is syntactically
available only within the code block that defines the type.
This provides some measure of data abstraction, since it is not possible
for user code to construct arbitrary instances.

Constants are pre-built tagged values.

Types are a superset of tags that includes values generated by the
special tags \texttt{Abstract}, \texttt{Union}, and \texttt{UnionAll},
plus the special values \texttt{Any} and \texttt{Bottom}:

\vspace{-3ex}
\begin{singlespace}
\begin{align*}
  type\ ::=\ &\ \texttt{Bottom}\ |\ abstract\ |\ var \\
             &\ |\ \texttt{Union}\ type\ type \\
             &\ |\ \texttt{UnionAll}\ type\texttt{<:}var\texttt{<:}type\ type \\
             &\ |\ \texttt{Tag}\ x_{name}\ abstract_{super}\ value* \\
  abstract\ ::=\ &\ \texttt{Any}\ |\ \texttt{Abstract}\ x_{name}\ abstract_{super}\ value* \\
                 &\ |\ \texttt{Abstract}\ \texttt{Tuple}\ \texttt{Any}\ type*\ type\texttt{...}
\end{align*}
\end{singlespace}

\noindent
The last item is the special abstract variadic tuple type.

\subsubsection{Data model}

The language maps tags to data descriptions using built-in rules, and ensures that
the data part of a tagged value always conforms to the tag's description.
Mappings from tags to data descriptions are established by special type
declaration syntax.
Data descriptions have the following grammar:

\vspace{-3ex}
\begin{singlespace}
\begin{align*}
data\ ::=\ &\ bit^n\ |\ ref\ |\ data*
\end{align*}
\end{singlespace}

\noindent
where $bit^n$ represents a string of $n$ bits, and $ref$ represents a reference
to a tagged data value.
Data is automatically laid out according to the platform's application binary
interface (ABI).
Currently all compound types and heterogeneous tuples use the C struct ABI, and
homogeneous tuples use the array ABI.
Data may be declared mutable, in which case its representation is implicitly
wrapped in a mutable cell.
A built-in primitive equality operator \texttt{===} is provided, based on
$egal$ \cite{egal} (mutable objects are compared by address, and immutable objects
are compared by directly comparing both the tag and data parts bit-for-bit, and
recurring through references to other immutable objects).

\subsubsection{Functions and methods}

Functions are generally applied to more than one argument. In the application
syntax $e_1(e_2)$, $e_2$ is an implicitly constructed tuple of all arguments.
$e_1$ must evaluate to a generic function, and its most specific method
matching the tag of argument $e_2$ is called.

We use the keyword \texttt{function} for method definitions for the sake of
familiarity, though \texttt{method} is arguably more appropriate. Method
definitions subsume lambda expressions. Each method definition modifies a
generic function named by the argument $x_{name}$. The generic function to extend is
specified by its name rather than by the value of an expression in order to make it
easier to syntactically
restrict where functions can be extended. This, in turn, allows the language to
specify when new method definitions take effect, providing useful windows of
time within which methods do not change, allowing programs to be optimized more
effectively (and hopefully discouraging abusive and confusing run time
method replacements).

The signature, or specializer, of a method is obtained by evaluating $e_{type}$,
which must result in a type value as defined above. A method has $n$
formal argument names $x_i$. The specializer must be a subtype of the
variadic tuple type of length $n$. When a method is called, its formal argument
names are bound to corresponding elements of the argument tuple. If the
specializer is a variadic type, then the last argument name is bound to a
tuple of all trailing arguments.

% (TODO describe restrictions)

The equivalent of ordinary lambda expressions can be obtained by introducing
a unique local name and defining a single method on it.

Mutable lexical bindings are provided by the usual translation to operations
on mutable cells.

%\subsection{A note on static typing}

% isomorphism between our types T and propositions ``term will be of type T''
% we will elide the difference
% trivially undecidable due to the definition of new()
% it is quite likely a useful static version could be developed. but
% we do not do that here, since our goals are (1) to develop the system
% for specialization & selection, not checking, and (2) to emphasize
% that no amount of ``dynamism'' need be given up.

% static type systems begin with errors we want to exclude, then design
% restrictions to make that possible, then go on to show that, indeed,
% most useful programs can still be written.

% one reason we skip static checking is to reverse this process:
% first see what kinds of type behavior technical users want in their
% programs, then identify and quantify any regularities later.

\section{Type system}
\label{sec:typesystem}

Our goal is to design a type system for describing method applicability,
and (similarly) for describing classes of values for which to specialize code.
Set-theoretic types are a natural basis for such a system.
A set-theoretic type is a symbolic expression that denotes a set of values.
In our case, these correspond to the sets of values methods are intended to apply
to, or the sets of values supported by compiler-generated method specializations.
Since set theory is widely understood, the use of such types tends to be intuitive.

These types
are less coupled to the languages they are used with, since one may design
a value domain and set relations within it without yet considering how types
relate to program terms \cite{1029823, Castagna:2005:GIS:1069774.1069793}.
Since our goals only include
performance and expressiveness, we simply skip the later steps for now, and do
not consider in detail possible approaches to type checking.
A good slogan for this attitude might be ``check softly and carry a big
subtype relation.''

% TODO maybe mention that in some sense being dynamically typed makes the
% requirements on subtyping stricter, because we don't have the option
% of being conservative and giving more compiler errors than necessary.
% at every point, we have to pick some behavior and we can't silently
% do the wrong thing.

%To avoid the dual traps of ``excess power'' and divergence
The system we use
must have a decidable subtype relation, and must be closed under data flow operations
(meet, join, and widen).
It must also lend itself to a reasonable definition of
specificity, so that methods can be ordered automatically (a necessary property for
composability).
These requirements are fairly strict.
%, but still admit many possible designs.
%The one we present here is aimed at providing the minimum level of
%sophistication needed to yield a language that feels ``powerful'' to most modern
%programmers.
Beginning with the simplest possible system, we added features as
needed to satisfy the aforementioned closure properties.
% or to allow us to
%write method definitions that seemed particularly useful (as it turns out, these
%two considerations lead to essentially the same features).
%The presentation that
%follows will partially reproduce the order of this design process.

We will define our types by describing their denotations as sets.
We use the notation $\llbracket T \rrbracket$ for the set denotation of
type expression $T$.
Concrete language syntax and terminal symbols of the type expression grammar
are written in typewriter font, and metasymbols are written in mathematical italic.
First there is a universal type \texttt{Any}, an empty type \texttt{Bottom}, and
a partial order $\leq$:

\vspace{-3ex}
\begin{align*}
  \llbracket \texttt{Any} \rrbracket &= \mathcal{D} \\
  \llbracket \texttt{Bottom} \rrbracket &= \emptyset \\
  T \leq S &\Leftrightarrow \llbracket T \rrbracket \subseteq \llbracket S \rrbracket
\end{align*}

\noindent
where $\mathcal{D}$ represents the domain of all values.
Also note that the all-important array type is written as \texttt{Array\{T,N\}} where
\texttt{T} is an element type and \texttt{N} is a number of dimensions.

Next we add data objects with structured tags.
The tag of a value is accessed with \texttt{typeof(x)}.
Each tag consists of a declared type name and some number of sub-expressions,
written as \texttt{Name\{}$E_1, \cdots, E_n$\texttt{\}}.
The center dots ($\cdots$) are meta-syntactic and represent a sequence of expressions.
Tag types may have declared supertypes (written as \texttt{super(T)}).
Any type used as a supertype must be declared as abstract, meaning it
cannot have direct instances.

\vspace{-3ex}
\begin{align*}
  \llbracket \texttt{Name\{}\cdots\texttt{\}} \rrbracket &= \{ x\mid \texttt{typeof(}x\texttt{)} = \texttt{Name\{}\cdots\texttt{\}} \} \\
  \llbracket \texttt{Abstract\{}\cdots\texttt{\}} \rrbracket &= \bigcup_{\texttt{super(}T\texttt{)} = \texttt{Abstract\{}\cdots\texttt{\}}} \llbracket T \rrbracket
\end{align*}

These types closely resemble the classes of an object-oriented language with
generic types, invariant type parameters, and no concrete inheritance.
We prefer parametric \emph{invariance} partly for reasons that have been addressed in the
literature \cite{Day:1995:SVC:217838.217852}.
Invariance preserves the property that the only subtypes of a concrete type are \texttt{Bottom}
and itself.
This is important given how we map types to data representations: an \texttt{Array\{Int\}}
cannot also be an \texttt{Array\{Any\}}, since those types imply different
representations (an \texttt{Array\{Any\}} is an array of pointers).
%If we tried to use covariance despite this, there would have to be some \emph{other}
%notion of which type a value \emph{really} had, which would be unsatisfyingly
%complex.
Tuples are a special case where covariance works, because each component type need
only refer to single value, so there is no need for concrete
tuple types with non-concrete parameters.
% TODO: important, but maybe conflates subtyping and inheritance too much
%Similarly, concrete inheritance conflicts somewhat with specialization.
%Code cannot be maximally specialized for a given type if instances of that type might
%have different representations.

Next we add conventional product (tuple) types, which are used to represent the
arguments to methods. These are almost identical to the nominal types defined above,
but are different in two ways: they are \emph{covariant} in their parameters, and permit
a special form ending in three dots (\texttt{...}) that denotes any number of trailing
elements:

\vspace{-3ex}
\begin{align*}
  \llbracket \texttt{Tuple\{}P_1,\cdots,P_n\texttt{\}} \rrbracket &= \prod_{1\leq i \leq n} \llbracket P_i \rrbracket \\
  \llbracket \texttt{Tuple\{}\cdots,P_n\texttt{...\}} \rrbracket, n\geq 1 &= \bigcup_{i\geq n-1} \llbracket \texttt{Tuple\{}\cdots,P_n^i\texttt{\}} \rrbracket
  %\llbracket \texttt{Tuple\{}\cdots\texttt{\}} \rrbracket \cup \llbracket \texttt{Tuple\{}\cdots,P_n\texttt{\}} \rrbracket \cup \llbracket \texttt{Tuple\{}\cdots,P_n,P_n\texttt{...\}} \rrbracket \\
\end{align*}

\noindent
$P_n^i$ represents $i$ repetitions of the final element $P_n$ of the type expression.

Abstract tuple types ending in \texttt{...} correspond to variadic methods, which
provide convenient interfaces for tasks like concatenating any number of arrays.
Multiple dispatch has been formulated as dispatch on tuple types before \cite{Leavens1998}.
This formulation has the advantage that \emph{any} type that is a subtype of a
tuple type can be used to express the signature of a method.
It also makes the system simpler and more reflective, since subtype queries can be
used to ask questions about methods.

The types introduced so far would be sufficient for many programs, and are
roughly equal in power to several multiple dispatch systems that have been designed
before.
However, these types are not closed under data flow operations.
For example, when the two branches of a conditional expression yield different types,
a program analysis must compute the union of those types to derive the type of
the conditional.
The above types are not closed under set union.
We therefore add the following type connective:

\vspace{-3ex}
\[
  \llbracket \texttt{Union\{}A,B\texttt{\}} \rrbracket = \llbracket A \rrbracket \cup \llbracket B \rrbracket \\
\]

As if by coincidence, \texttt{Union} types are also tremendously useful for expressing
method dispatch.
For example, if a certain method applies to all 32-bit integers regardless
of whether they are signed or unsigned, it can be specialized for \texttt{Union\{Int32,UInt32\}}.

\texttt{Union} types are easy to understand, but complicate the type system considerably.
To see this, notice that they provide an unlimited number of ways to rewrite any type.
For example a type \texttt{T} can always be rewritten as \texttt{Union\{T,Bottom\}}, or
\texttt{Union\{Bottom,Union\{T,Bottom\}\}}, etc.
Any code that processes types must ``understand'' these equivalences.
Covariant constructors (tuples in our case) also distribute over \texttt{Union} types,
providing even more ways to rewrite types:

\vspace{-3ex}
\[
\texttt{Tuple\{Union\{A,B\},C\}} = \texttt{Union\{Tuple\{A,C\},Tuple\{B,C\}\}}
\]

This is one of several reasons that union types are often considered undesirable.
When used with type inference, such types can grow without bound, possibly leading
to slow or even non-terminating compilation.
Their occurrence also typically corresponds to cases that would fail many static type
checkers.
Yet from the perspectives of both data flow analysis and method specialization, they
are perfectly natural and even essential
\cite{abstractinterp, Igarashi, Smith:2008:JTI:1449764.1449804}.

The next problem we need to solve arises from data flow analysis of
the \texttt{new} construct.
When a type constructor \texttt{C} is applied to a type
$S$ that is known only approximately at compile time, the type \texttt{C\{}$S$\texttt{\}}
does not correctly represent the result.
%if \texttt{C} is invariant.
The correct result would be the union of all types \texttt{C\{}$T$\texttt{\}}
where $T\leq S$.
There is again a corresponding need for such types in method dispatch.
Often one has, for example, a method that applies to arrays of any
kind of integer (\texttt{Array\{Int32\}}, \texttt{Array\{Int64\}}, etc.).
These cases can be expressed using a \texttt{UnionAll} connective, which denotes
an iterated union of a type expression for all values of a parameter within
specified bounds:

\vspace{-3ex}
\[
  \llbracket \texttt{UnionAll }L\texttt{<:T<:}U\ A \rrbracket = \bigcup_{L \leq T \leq U} \llbracket A[T/\texttt{T}] \rrbracket
\]

\noindent
where $A[T/\texttt{T}]$ means $T$ is substituted for \texttt{T} in expression $A$.

% TODO: The inclusion of lower bounds might make subtyping undecidable?
% Note that giving up lower bounds might permit intersections or arrows,
% but we prefer lower bounds.

This is similar to an existential type \cite{boundedquant};
for each concrete subtype of it there exists a corresponding $T$.
Anecdotally, programmers often find existential types confusing.
We prefer the union interpretation because we are describing sets of values;
the notion of ``there exists'' can be semantically misleading since it sounds like
only a single $T$ value might be involved.
However we will still use $\exists$ notation as a shorthand.

%Conjecture: these types are intuitive to dispatch on because they correspond
%to program behavior in the same way that data flow analysis approximates program
%behavior.

% $T=S \longleftrightarrow (T\leq S) \wedge (S\leq T)$.

\subsubsection{Examples}

\texttt{UnionAll} types are quite expressive. In combination with nominal
types they can describe groups of containers such as
\texttt{UnionAll T<:Number Array\{Array\{T\}\}} (all arrays of arrays of
some kind of number) or
\texttt{Array\{UnionAll T<:Number Array\{T\}\}} (an array of arrays of
potentially different types of number).

In combination with tuple types, \texttt{UnionAll} types provide powerful
method dispatch specifications. For example
\texttt{UnionAll T Tuple\{Array\{T\},Int,T\}} matches three arguments:
an array, an integer, and a value that is an instance of the array's
element type. This is a natural signature for a method that assigns a
value to a given index within an array.

\subsubsection{Type system variants}

Our design criteria do not identify a unique type system; some
variants are possible.
The following features would probably be fairly straightforward to add:

\vspace{-3ex}
\begin{singlespace}
\begin{itemize}
\item Structurally subtyped records
\item $\mu$-recursive types (regular trees)
\item General regular types (allowing \texttt{...} in any position)
\end{itemize}
\end{singlespace}

\noindent
The following features would be difficult to add, or possibly break decidability
of subtyping:

\vspace{-3ex}
\begin{singlespace}
\begin{itemize}
\item Arrow types
\item Negations
\item Intersections, multiple inheritance
\item Universal quantifiers
\item Contravariance
%\item arbitrary predicates, theory of natural numbers, etc.
\end{itemize}
\end{singlespace}


\subsection{Type constructors}

It is important for any proposed high-level technical computing language to be
simple and approachable, since otherwise the value over established
powerful-but-complex languages like C++ is less clear.
In particular, type parameters raise usability concerns.
Needing to write parameters along with every type is verbose, and requires users
to know more about the type system and to know more details of particular
types (how many parameters they have and what each one means).
Furthermore, in many contexts type parameters are not directly relevant.
For example, a large amount of code operates on \texttt{Array}s of any
element type, and in these cases it should be possible to ignore type parameters.

Consider \texttt{Array\{T\}}, the type of arrays with element type \texttt{T}.
In most languages with parametric types, the identifier \texttt{Array} would
refer to a type constructor, i.e.\ a type of a different \emph{kind} than
ordinary types like \texttt{Int} or \texttt{Array\{Int\}}.
Instead, we find it intuitive and appealing for \texttt{Array} to refer to
any kind of array, so that a declaration such as \texttt{x::Array} simply
asserts \texttt{x} to be some kind of array.
In other words,

\vspace{-3ex}
\[
\texttt{Array} = \texttt{UnionAll T Array$^\prime$\{T\}}
\]

\noindent
where \texttt{Array$^\prime$} refers to a hidden, internal type constructor.
The \texttt{\{ \}} syntax can then be used to instantiate a \texttt{UnionAll}
type at a particular parameter value.


\subsection{Subtyping}
\label{sec:subtyping}

\begin{figure}[!t]
  \begin{center}
    \def\arraystretch{2}
    \begin{tabular}{|c|}\hline
      \begin{tabular}{ccc}
        \AxiomC{$_A^B X^L, \Gamma\ \vdash\ T \leq S$}
        \UnaryInfC{$\Gamma\ \vdash\ \exists$ $_A^B X\ T\ \leq\ S$}
        \DisplayProof

        \hspace{3ex}

        &

        \AxiomC{$_A^BX^R, \Gamma\ \vdash\ T \leq S$}
        \UnaryInfC{$\Gamma\ \vdash\ T\ \leq\ \exists$ $_A^B X\ S$}
        \DisplayProof

        \hspace{3ex}

        &

        \AxiomC{}
        \UnaryInfC{$\Gamma\ \vdash\ X \leq X$}
        \DisplayProof
      \end{tabular}

      \\[8pt]

      \begin{tabular}{cc}
        \AxiomC{$^BX^L,{} _AY^L,\Gamma\ \vdash\ B \leq Y\ \vee\ X \leq A$}
        \UnaryInfC{$^BX^L,{} _AY^L,\Gamma\ \vdash\ X \leq Y$}
        \DisplayProof

        \hspace{4ex}

        &

        \AxiomC{$_A^BX^R,{} Y^R,\Gamma\ \vdash\ B \leq A$}
        \UnaryInfC{$_A^BX^R,{} Y^R,\Gamma\ \vdash\ X \leq Y$}
        \DisplayProof

        \\[8pt]

        \AxiomC{$_A^BX^R,\Gamma\ \vdash\ T \leq B$}
        \UnaryInfC{$_{A \cup T}^{\ \ \ B}X^R,\Gamma\ \vdash\ T \leq X$}
        \DisplayProof

        \hspace{4ex}

        &

        \AxiomC{$_A^BX^R,\Gamma\ \vdash\ A \leq T$}
        \UnaryInfC{$_A^TX^R,\Gamma\ \vdash\ X \leq T$}
        \DisplayProof

        \\[8pt]

        \AxiomC{$_AX^L,\Gamma\ \vdash\ T \leq A$}
        \UnaryInfC{$_AX^L,\Gamma\ \vdash\ T \leq X$}
        \DisplayProof

        \hspace{3ex}

        &

        \AxiomC{$^BX^L,\Gamma\ \vdash\ B \leq T$}
        \UnaryInfC{$^BX^L,\Gamma\ \vdash\ X \leq T$}
        \DisplayProof

        \\[8pt]
      \end{tabular}
      \\
      \hline
    \end{tabular}
  \end{center}
  \caption[Subtyping algorithm]{
\small{
    Subtyping algorithm for \texttt{UnionAll} ($\exists$) and variables.
    $X$ and $Y$ are variables, $A$, $B$, $T$, and $S$ are types or variables.
    $_A^BX$ means $X$ has lower bound $A$ and upper bound $B$.
    $^R$ and $^L$ track whether a variable originated on the right or on the left of
    $\leq$.
    Rules are applied top to bottom.
    Summary of the sequent notation used:
    $\Gamma\vdash x$ means that $x$ is true in environment $\Gamma$.
    Given the premises above a horizontal line, we can derive the conclusion
    below it.
}
  }
  \label{subtvars}
\end{figure}

Computing the subtype relation is the key algorithm in our system.
It is used in the following cases:

\begin{itemize}
\item Determining whether a tuple of arguments matches a method signature.
\item Comparing method signatures for specificity and equality.
\item Source-level type assertions.
\item Checking whether an assigned value matches the declared type of a
location.
\item Checking for convergence during type inference.
\end{itemize}

Deciding subtyping for base types is straightforward: \texttt{Bottom} is
a subtype of everything, everything is a subtype of \texttt{Any}, and
tuple types are compared component-wise.
The invariant parameters of tag types are compared in both directions: to check
$\texttt{A\{B\}}\leq \texttt{A\{C\}}$, check $\texttt{B}\leq\texttt{C}$ and
then $\texttt{C}\leq\texttt{B}$.
In fact, the algorithm depends on these checks being done in this order, as we
will see in a moment.

Checking union types is a bit harder. When a union $A\cup B$ occurs in the
algorithm, we need to non-deterministically replace it with either $A$ or
$B$. The rule is that for all such choices on the left of $\leq$, there
must exist a set of choices on the right such that the rest of the
algorithm accepts. This can be implemented by keeping a stack of
decision points, and looping over all possibilities with an outer
for-all loop and an inner there-exists loop. We speak of ``decision points''
instead of individual unions, since in a type like \texttt{Tuple\{Union\{A,B\}...\}}
a single union might be compared many times.

The algorithm for \texttt{UnionAll} and variables is shown in figure~\ref{subtvars}.
The first row says to handle a \texttt{UnionAll} by extending the environment
with its variable, marked according to which side of $\leq$ it came from,
and then recurring into the body.
In analogy to union types, we need to check that for all variable values on
the left, there exists a value on the right such that the relation holds.
The for-all side is relatively easy to implement, since we can just use
a variable's bounds as proxies for its value (this is shown in
the last row of the figure).
We implement the there-exists side by narrowing a variable's bounds
(raising the lower bound and lowering the upper bound, in figure row 3).
The relation holds
as long as the bounds remain consistent (i.e.\ lower bound $\leq$
upper bound).
The algorithm assumes that all input types are well-formed,
which includes variable lower bounds always being less than or equal to
upper bounds.

The rules in the second row appear asymmetric.
This is a result of exploiting the lack of contravariant constructors.
No contravariance means that every time a
right-side variable appears on the \emph{left} side of a comparison,
it must be because it occurs in invariant position, and the steps outlined
in the first paragraph of this section have ``flipped'' the order
(comparing both $\texttt{B}\leq\texttt{C}$ and $\texttt{C}\leq\texttt{B}$).
This explains the odd rule for comparing two right-side variables:
this case can only occur with differently nested \texttt{UnionAll}s and
invariant constructors, in which case the relation holds only if
all involved bounds are equal.
By symmetry, one would expect the rule in row 3, column 2 to
update $X$'s upper bound to $B\cap T$. But because of invariance,
$T\leq B$ has already been checked by rule in row 3, column 1.
Therefore $B\cap T = T$. This is the reason the ``forward''
direction of the comparison needs to be checked first: otherwise,
we would have updated $B$ to equal $T$ already and the $T\leq B$
comparison would become vacuous. Alternatively, we could actually
compute $B\cap T$. However there is reason to suspect that
trouble lies that way. We would need to either add intersection types
to the system, or compute a meet without them. Either way, the
algorithm would become much more complex and, judging by past
results, likely undecidable.

% worth asking why we go through such contortions, only to end up
% setting X's bounds both to T exactly. the reason is that this
% handles covariant and invariant position together, and also
% automatically handles ``degrees of freedom'' mismatches like
% Pair{T,T} < Pair{T,S}, which by the way doesn't hold if the
% variables have equal upper and lower bounds.

%TODO: termination and correctness.

\subsubsection{Complexity}

These subtyping rules are likely $\Pi_2^{\textrm{P}}$-hard.
Checking a subtype relation with unions requires checking that for all choices
on the left, there exists a choice on the right that makes the relation hold.
This matches the quantifier structure of 2-TQBF problems of the form
$\forall x_i \exists y_i F$ where $F$ is a boolean formula.
If the formula is written in conjunctive normal form, it corresponds to subtype
checking between two tuple types, where the relation must hold for each pair of
corresponding types.
Now use a type \texttt{N\{}$x$\texttt{\}} to represent $\neg x$.
The clause $(x_i \vee y_i)$ can be translated to
$x_i\ \texttt{<:\ Union\{N\{}y_i\texttt{\}, True\}}$ (where the $x_i$ and
$y_i$ are type variables bound by \texttt{UnionAll} on the left and right,
respectively).
We have not worked out the details, but this sketch is reasonably
convincing.
$\Pi_2^{\textrm{P}}$ is only the most obvious reduction to try; it is possible our
system equals PSPACE or even greater, as has often been the case for subtyping
systems like ours.

\subsubsection{Implementation}

Appendix~\ref{appendix:subtyping} gives a Julia implementation of this
algorithm.
This also serves as a good example of Julia type and method definition
syntax.
Translating the code into other languages should be straightforward.

\subsubsection{Example deductions}

We will briefly demonstrate the power of this algorithm through examples of
type relationships it can determine.
In these examples, note that $<$ means less than but not equal.
\texttt{Pair} is assumed to be a tag type with two parameters.

\noindent
The algorithm can determine that a type matches constraints specified by another:

\vspace{-5ex}
\[
\texttt{Tuple}\{\texttt{Array}\{\texttt{Integer},1\}, \texttt{Int}\}\ <\ 
  (\exists\ T<:\texttt{Integer}\ \exists\ S<:T\ \texttt{Tuple}\{\texttt{Array}\{T,1\},S\})
\]

\vspace{-1ex}
\noindent
It is not fooled by redundant type variables:

\vspace{-2ex}
\[
\texttt{Array}\{\texttt{Int},1\}\ =\ 
  \texttt{Array}\{(\exists\ T<:\texttt{Int}\ T), 1\} \]

\noindent
Variables can have non-trivial bounds that refer to other variables:

\vspace{-3ex}
\begin{singlespace}
\begin{align*}
&\texttt{Pair}\{\texttt{Float32},\texttt{Array}\{\texttt{Float32},1\}\}\ <\ \\
&\hspace{4ex}\exists\ T<:\texttt{Real}\ \exists\ S<:\texttt{AbstractArray}\{T,1\}\ \texttt{Pair}\{T,S\}
\end{align*}
\end{singlespace}

%  @test !issub(Ty((Float32,Array{Float64,1})),
%               @UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))

\noindent
In general, if a variable appears multiple times then its enclosing type is
more constrained than a type where variables appear only once:

\vspace{-3ex}
\[
\exists\ T\ \texttt{Pair}\{T,T\}\ <\ \exists\ T\ \exists\ S\ \texttt{Pair}\{T,S\}
\]

\noindent
However with sufficiently tight bounds that relationship no longer holds
(here $x$ is any type):

\vspace{-3ex}
\[
\exists\ x<:T<:x\ \exists\ x<:S<:x\ \texttt{Pair}\{T,S\}\ <\ \exists\ T\ \texttt{Pair}\{T,T\}
\]

%    @test issub_strict((@UnionAll T @UnionAll S<:T inst(PairT,T,S)),
%                       (@UnionAll T @UnionAll S    inst(PairT,T,S)))

\noindent
Variadic tuples of unions are particularly expressive (``every argument is
either this or that''):

\vspace{-3ex}
\begin{singlespace}
\begin{align*}
&\texttt{Tuple\{Vector\{Int\},Vector\{Vector\{Int\}\},Vector\{Int\},Vector\{Int\}\}}\ <\ \\
&\hspace{4ex}\exists\ S<:\texttt{Real}\ \texttt{Tuple\{Union\{Vector\{}S\}\texttt{,Vector\{Vector\{}S\texttt{\}\}\}...\}}
\end{align*}
\end{singlespace}

\noindent
And the algorithm understands that tuples distribute over unions:

\vspace{-3ex}
\[
\texttt{Tuple\{Union\{A,B\},C\}}\ =\ \texttt{Union\{Tuple\{A,C\},Tuple\{B,C\}\}}
\]

\subsubsection{Pseudo-contravariance}

Bounded existential types are normally contravariant in their lower bounds.
However, the set denotations of our types give us
$(\exists\ T>:X\ T) = \texttt{Any}$.
By interposing an invariant constructor, we obtain a kind of contravariance:
\[
(\exists\ T>:X\ \texttt{Ref}\{T\}) \leq (\exists\ T>:Y\ \texttt{Ref}\{T\}) \implies Y\leq X
\]
\noindent
Types like this may be useful for describing nominal arrow types
(see section~\ref{sec:nominalarrows}).
This ability to swap types between sides of $\leq$ is one of the keys to
the undecidability of subtyping with bounded quantification~\cite{Pierce1994131}.
Nevertheless we conjecture that our system is decidable, since we treat
left- and right-side variables asymmetrically.
The bounds of left-side variables do not change, which might be sufficient to
prevent the ``re-bounding'' process in system $F_{<:}$ from continuing.
%We conjecture that the presence of the invariant constructor blocks
%undecidability in our case.


\subsubsection{Related work}

Our algorithm is similar to some that have been investigated for Java
generics (\cite{wehr2008subtyping, Cameron:2009:SWE:1557898.1557902,
Tate:2011:TWJ:1993316.1993570}).
In that context, the primary difficulty is undecidability due to
circular constraints such as \texttt{class Infinite<P extends Infinite<?>>}
and circularities in the inheritance hierarchy such as
\texttt{class C implements List<List<?\ super C>>} (examples from
\cite{Tate:2011:TWJ:1993316.1993570}).
We have not found a need for such complex declarations.
Julia disallows mentioning a type in the constraints of its own parameters.
When declaring type $T$ a subtype of $S$, only the direct parameters of
$T$ or $S$ can appear in the subtype declaration.
We believe this leads to decidable subtyping.

Dynamic typing provides a useful loophole: it is never truly
necessary to declare constraints on a type's parameters, since
the compiler does not need to be able to prove that those
parameters satisfy any constraints when instances of the type are
used.
In theory, an analogous problem for Julia would be spurious method
ambiguities due to an inability to declare sufficiently strong
constraints.
More work is needed to survey a large set of Julia libraries to see
if this might be a problem in practice.

Past work on subtyping with regular
types~\cite{hosoya2000regular, xtatic} is also related, particularly
to our treatment of union types and variadic tuples.


\section{Dispatch system}

% TODO \cite{Dubois:1995:EP:199448.199473}

Julia's dispatch system strongly resembles the multimethod systems
found in some object-oriented languages
\cite{closspec,closoverview,dylanlang,cecil,cecilspec,chambers2006diesel}.
However we prefer the term type-based dispatch, since our system
actually works by dispatching a \emph{single tuple type} of arguments.
The difference is subtle and in many cases not noticeable, but has
important conceptual implications.
It means that methods are not necessarily restricted to specifying
a type for each argument ``slot''.
For example a method signature could be
\texttt{Union}\{\texttt{Tuple}\{\texttt{Any},\texttt{Int}\}, \texttt{Tuple}\{\texttt{Int},\texttt{Any}\}\},
which matches calls where either, but not necessarily both, of two
arguments is an \texttt{Int}.
\footnote{Our implementation of Julia does not yet have syntax for such methods.}

\subsection{Type and method caches}

The majority of types that occur in practice are \emph{simple}.
A simple type is a tag, tuple, or abstract type, all of whose parameters
are simple types or non-type values.
For example \texttt{Pair\{Int,Float64\}} is a simple type.
Structural equality of simple types is equivalent to type equality,
so simple types are easy to compare, hash, and sort.
Another important set of types is the \emph{concrete} types, which
are the direct types of values.
Concrete types are hash-consed in order to assign a unique integer
identifier to each.
These integer identifiers are used to look up methods efficiently
in a hash table.

Some types are concrete but not simple, for example
\texttt{Array\{Union\{Int,String\},1\}}.
The hash-consing process uses linear search for these types.
Fortunately, such types tend to make up less than 10\% of the total
type population.
On cache misses, method tables also use linear search.

%this can work especially well for tuple types.
%by writing (1, 2.0) you immediately obtain an efficient ``struct'' type.
%cases like protocol compilers require generating code in advance.
%this generates it on the fly, but can pick up and reuse any cached
%code that might happen to exist for a particular tuple type.

\subsection{Specificity}

Sorting methods by specificity is a crucial feature of a generic
function system.
It is not obvious how to order types by specificity, and our
rules for it have evolved with experience.
The core of the algorithm is straightforward:

\begin{itemize}
\item If $A$ is a strict subtype of $B$, then it is more specific than $B$.
\item If $B\leq A$ then $A$ is not more specific than $B$.
\item If some element of tuple type $A$ is more specific than its corresponding
element in tuple type $B$, and no element of $B$ is more specific than its
corresponding element in $A$, then $A$ is more specific.
\end{itemize}

%tuples: if an elt of a is more specific than its corresponding elt in b,
%and no elt of b is more specific than its corresponding elt in a.

This is essentially the same specificity rule used by Dylan~\cite{dylanlang}
for argument lists.
Julia generalizes this to tuple types; it is applied recursively to tuple
types wherever they occur.
We then need several more rules to cover other features of the type system:

\begin{itemize}
\item A variadic type is less specific than an otherwise equal non-variadic type.
\item Union type $A$ is more specific than $B$ if some element of $A$ is
more specific than $B$, and $B$ is not more specific than any
element of $A$.
\item Non-union type $A$ is more specific than union type $B$ if it is more specific
than some element of $B$.
\item A tag type is more specific than a tag type strictly above it in the
hierarchy, regardless of parameters.
%(this embeds a moderate amount of ``class based'' dispatch, compatible
%with programmer intuition)
\item A variable is more specific than type $T$ if its upper bound is more specific
than $T$.
\item Variable $A$ is more specific than variable $B$ if $A$'s upper bound is
more specific than $B$'s, and $A$'s lower bound is not more specific than $B$'s.
\end{itemize}

So far, specificity is clearly a less formal notion than subtyping.

Specificity and method selection implicitly add a set difference operator to
the type system.
When a method is selected, all more specific definitions have not been, and
therefore the more specific signatures have been subtracted.
For example, consider the following definitions of a string concatenation
function:

\begin{singlespace}
\begin{lstlisting}[language=julia]
strcat(strs::ASCIIString...) = # an ASCIIString

strcat(strs::Union{ASCIIString,UTF8String}...) = # a UTF8String
\end{lstlisting}
\end{singlespace}

Inside the second definition, we know that at least one argument must be a
\texttt{UTF8String}, since otherwise the first definition would have
been selected.
This encodes the type behavior that ASCII strings are closed under
concatenation, while introducing a single UTF-8 string requires the result
to be UTF-8 (since UTF-8 can represent strictly more characters than ASCII).
The effect is that we obtain some of the power of set intersection and
negation without requiring subtyping to reason explicitly about such types.
%The tradeoff is a slight loss of type precision when analyzing such
%definitions.


\subsection{Parametric dispatch}

We use the following syntax to express methods whose signatures
are \texttt{UnionAll} types:

\begin{singlespace}
\begin{lstlisting}[language=julia]
func{T<:Integer}(x::Array{T}) = ...
\end{lstlisting}
\end{singlespace}

\noindent
This method matches any \texttt{Array} whose element type is some subtype
of \texttt{Integer}.
The value of \texttt{T} is available inside the function.
This feature largely overcomes the restrictiveness of parametric invariance.
Methods like these are similar to methods with ``implicit type parameters''
in the Cecil language~\cite{cecilspec}.
However, Cecil (along with its successor, Diesel~\cite{chambers2006diesel})
does not allow methods to differ only in type parameters.
In the semantic subtyping framework we use, such definitions have a
natural interpretation in terms of sets, and so are allowed.
In fact, they are used extensively in Julia (see section~\ref{sec:callingblas}
for an example).

The system $\textrm{ML}_{\leq}$~\cite{Bourdoncle:1997:TCH:263699.263743} combined
multiple dispatch with parametric polymorphism, however the parametricity
appeared in types assigned to entire generic functions.
This has benefits for program structure and type safety, but is a bit
restrictive.
In fact Julia does not directly use the concept of parametricity.
Like Fortress~\cite{fortressmodular}, we allow more flexibility in method
definitions.
Our formulation of method signatures as existential types for purposes of
applicability and specificity is similar to that used in Fortress.
However unlike Fortress all of our types are first-class: all types
(including union types) can be dispatched on and used in declarations.


\subsection{Diagonal dispatch}
\label{sec:diagonal}

\texttt{UnionAll} types can also express constraints between arguments.
The following definition matches two arguments of the same concrete
type:

\begin{singlespace}
\begin{lstlisting}[language=julia]
func{T}(x::T, y::T) = ...
\end{lstlisting}
\end{singlespace}

\noindent
Section~\ref{sec:conversion} discusses an application.

This feature is currently implemented only in the dispatch system;
we have not yet formalized it as part of subtyping.
For example, the subtyping algorithm presented here concludes that
\texttt{Tuple\{Int,String\}} is a subtype of
\texttt{UnionAll T Tuple\{T,T\}}, since \texttt{T} might equal
\texttt{Any} or \texttt{Union\{Int,String\}}.
We believe this hurts the accuracy of static type deductions, but
not their soundness, as long as we are careful in the compiler to
treat all types as over-estimates of run time types.
In any case, we plan to fix this by allowing some type variables
to be constrained to concrete types.
This only affects type variables that occur only in covariant
position; types such as \texttt{UnionAll T Tuple\{Array\{T\},T\}}
are handled correctly.

\subsection{Constructors}
\label{sec:constructors}

Generic function systems (such as Dylan's) often implement value
constructors by allowing methods to be specialized for classes
themselves, instead of just instances of classes.
We extend this concept to our type system using a construct similar
to singleton kinds~\cite{Stone:2000:DTE:325694.325724}:
\texttt{Type\{T\}} is the type of any type equal to \texttt{T}.
A constructor for a complex number type can then be written as follows:

\begin{singlespace}
\begin{lstlisting}[language=julia]
call{T}(::Type{Complex{T}}, re::Real, im::Real) =
    new(Complex{T}, re, im)
\end{lstlisting}
\end{singlespace}

\noindent
This requires a small adjustment to the evaluation rules: in the application
syntax $e_1(e_2)$ when $e_1$ is not a function,
evaluate $\texttt{call}(e_1,e_2)$ instead, where \texttt{call} is
a particular generic function known to the system.
This constructor can then be invoked by writing e.g.\ \\
\texttt{Complex\{Float64\}(x,y)}.

Naturally, \texttt{Type} can be combined arbitrarily with other types,
adding a lot of flexibility to constructor definitions.
Most importantly, type parameters can be omitted in constructor calls
as long as there is a \texttt{call} method for the ``unspecialized'' version
of a type:

\begin{singlespace}
\begin{lstlisting}[language=julia]
call{T<:Real}(::Type{Complex}, re::T, im::T) =
    Complex{T}(re, im)
\end{lstlisting}
\end{singlespace}

This definition allows the call \texttt{Complex(1.0,2.0)} to
construct a \texttt{Complex\{Float64\}}.
This mechanism subsumes and generalizes the ability to ``infer''
type parameters found in some languages.
It also makes it possible to add new parameters to types without
changing client code.

\subsection{Ambiguities}

As in any generic function system, method ambiguities are possible.
Two method signatures are ambiguous if neither is more specific than
the other, but their intersection is non-empty.
For arguments that are a subtype of this intersection, it is not
clear which method should be called.

Some systems have avoided this problem by resolving method
specificity left to right, i.e.\ giving more weight to the leftmost
argument.
With dispatch based on whole tuple types instead of sequences of
types, this idea seems less defensible.
One could extract a sequence of types by successively
intersecting a method type with \texttt{UnionAll T Tuple\{T,Any...\}},
then \texttt{UnionAll T Tuple\{Any,T,Any...\}}, etc. and taking the
inferred \texttt{T} values.
However our experience leads us to believe that the left to right
approach is a bit too arbitrary, so we have stuck with ``symmetric''
dispatch.

In the Julia library ecosystem, method ambiguities are unfortunately
common.
Library authors have been forced to add many tedious and redundant
disambiguating definitions.
Most ambiguities have been mere nuisances rather than serious
problems.
A representative example is libraries that add new array-like
containers.
Two such libraries are Images and DataArray (an array designed to
hold statistical data, supporting missing values).
Each library wants to be able to interoperate with other array-like
containers, and so defines e.g.\ \texttt{+(::Image, ::AbstractArray)}.
This definition is ambiguous with \texttt{+(::AbstractArray, ::DataArray)}
for arguments of type \texttt{Tuple\{Image, DataArray\}}.
However in practice Images and DataArrays are not used together, so
worrying about this is a bit of a distraction.
Giving a run time error forcing the programmer to clarify intent
seems to be an acceptable solution (this is what Dylan does;
currently Julia only prints a warning when the ambiguous definition
is introduced).

\section{Generic programming}

Modern object-oriented languages often have special support for ``generic''
programming, which allows classes, methods, and functions to be reused
for a wider variety of types.
This capability is powerful, but has some usability cost as extra
syntax and additional rules must be learned.
We have found that the combination of our type system and generic functions
subsumes many uses of generic programming features.

For example, consider this C++ snippet, which shows how a template
parameter can be used to vary the arguments accepted by methods:

\begin{singlespace}
\begin{lstlisting}[language=c++,style=ttcode]
template <typename T>
class Foo<T> { int method1(T x); }
\end{lstlisting}
\end{singlespace}

\noindent
The method \texttt{method1} will only accept \texttt{int} when applied to
a \texttt{Foo<int>}, and so on.
This pattern can be expressed in Julia as follows:

\begin{singlespace}
\begin{lstlisting}[language=julia]
method1{T}(this::Foo{T}, x::T) = ...
\end{lstlisting}
\end{singlespace}

%template <>
%class Foo<int> { int method1(int x) { … } }
% becomes
% method1(this::Foo{Int}, x::Int) = …

%Multiple dispatch systems have often only dispatched on the classes of
%arguments.
%This makes it appear necessary to introduce a separate
%template system to handle other kinds of parameterization.
%Our type system makes it easy to match the expressive features of
%templates using dispatch.

\subsubsection{Associated types}

When dealing with a particular type in a generic program, it is often
necessary to mention other types that are somehow related.
For example, given a collection type the programmer will want to
refer to its element type, or given a numeric type one might want to
know the next ``larger'' numeric type.
Such associated types can be implemented as generic functions:

\begin{singlespace}
\begin{lstlisting}[language=julia]
eltype{T}(::AbstractArray{T}) = T

widen(::Type{Int32}) = Int64
\end{lstlisting}
\end{singlespace}

\subsubsection{Simulating multiple inheritance}

It turns out that external multiple dispatch is sufficiently powerful
to simulate a kind of multiple inheritance.
At a certain point in the development of Julia's standard library,
it become apparent that there were object properties that it would be
useful to dispatch on, but that were not reflected in the type hierarchy.
For example, the array type hierarchy distinguishes dense and sparse
arrays, but not arrays whose memory layout is fully contiguous.
This is important for algorithms that run faster using a single
integer index instead of a tuple of indexes to reference array elements.

Tim Holy pointed out that new object properties can be added
externally~\cite{timholytrait}, and proposed using it for this purpose:

\begin{singlespace}
\begin{lstlisting}[language=julia]
abstract LinearIndexing

immutable LinearFast <: LinearIndexing; end
immutable LinearSlow <: LinearIndexing; end

linearindexing(A::Array) = LinearFast()
\end{lstlisting}
\end{singlespace}

\noindent
This allows describing the linear indexing performance of a type by adding
a method to \texttt{linearindexing}.
An algorithm can consume this information as follows:

\begin{singlespace}
\begin{lstlisting}[language=julia]
algorithm(a::AbstractArray) = _algorithm(a, linearindexing(a))

function _algorithm(a, ::LinearFast)
    # code assuming fast linear indexing
end

function _algorithm(a, ::LinearSlow)
    # code assuming slow linear indexing
end
\end{lstlisting}
\end{singlespace}

\noindent
The original author of a type like \texttt{Array} does not need to know
about this property, unlike the situation with multiple inheritance or
explicit interfaces.
Adding such properties after the fact makes sense when new algorithms
are developed whose performance is sensitive to distinctions not
previously noticed.


\section{Staged programming}
\label{sec:stagedprogramming}

An especially fruitful use of types in Julia is as input to code that
generates other code, in a so-called ``staged'' program.
This feature is accessed simply by annotating a method definition
with a macro called \texttt{@generated}:

\begin{singlespace}
\begin{lstlisting}[language=julia]
@generated function getindex{T,N}(a::Array{T,N}, I...)
    expr = 0
    for i = N:-1:1
        expr = :( (I[$i]-1) + size(a,$i)*$expr )
    end
    :(linear_getindex(a, $expr + 1))
end
\end{lstlisting}
\end{singlespace}

\noindent
Here the syntax \texttt{:(  )} is a quotation: a representation of the
expression inside is returned, instead of being evaluated.
The syntax \texttt{quote ... end} is an alternative for quoting multi-line
expressions.
The value of an expression can be interpolated into a quotation using
prefix \texttt{\$}.

% where the rest of the language is about running code efficiently,
% this is about running code not at all.

This simple example implements indexing with \texttt{N} arguments
in terms of linear indexing, by generating a fully unrolled expression
for the index of the element.
Inside the body of the method, argument names refer to the types of
arguments instead of their values.
Parameter values \texttt{T} and \texttt{N} are available as usual.
The method returns a quoted expression.
This expression will be used, verbatim, as if it were the body of
a normal method definition for these argument types.

As a more realistic example, the \texttt{SubArray} type mentioned in
section~\ref{sec:chap3subtyping} is implemented using this technique.
A \texttt{SubArray}'s tuple of index types is examined to generate
efficient implementations of indexing functions.

The remarkable thing about this is how seamlessly it integrates into
the language.
The method is selected like any other; the only difference is that
the method's expression-generating code is invoked on the argument types
just before type inference.
The optimized version of the user-generated code is then stored in the method
cache, and can be selected in the future like any other specialization.
The generated code can even be inlined into call sites in library clients.
The caller does not need to know anything about this, and the author
of the function does not need to do any bookkeeping.

One reason this works so well is that the amount of information
available at this stage is well balanced.
If, for example, only the \emph{classes} of arguments in a traditional
object-oriented language were available, there would not be much
to base the generated code on.
If, on the other hand, details of the contents of values were needed,
then it would be difficult to reuse the existing dispatch system.

The types of arguments say something about their \emph{meaning},
and so unlike syntax-based systems (macros) are independent of how
the arguments are computed.
A staged method of this kind is guaranteed to produce the
same results for arguments \texttt{2+2} and \texttt{4}.

Another advantage of this approach is that the expression-generating
code is purely functional.
Staged programming with \texttt{eval}, in contrast, requires arbitrary
user code to be executed in all stages.
This has its uses; one example mentioned in \cite{DeVito:2014:FRG:2594291.2594307}
is reading a schema from a database in order to generate code for it.
But with \texttt{@generated}, code is a pure function of type information,
so when possible it can be invoked once at compile time and then
never again.
This preserves the possibility of full static compilation, but due to
dynamic typing the language cannot guarantee that all code generation
will occur before run time.

\subsubsection{Trade-offs of staged programming}

Code that generates code is more difficult to write, read, and debug.
At the same time, staged programming is easy to overuse, leading to obscure
programs that could have been written with basic language constructs
instead.

This feature also makes static compilation more difficult.
If an unanticipated call to a staged method occurs in a statically
compiled program, two rather poor options are available: stop with an
error, or run the generated code in an interpreter (we could compile
code at run time, but presumably the purpose of static compilation was
to avoid that).
Ordinarily, the worst case for performance is to dynamically dispatch
every call.
Constructing expressions and evaluating them with an interpreter is
even worse, especially considering that performance is the only reason
to use staged programming in the first place.
This issue will need to be addressed through enhanced static analysis
and error reporting tools.

It would be nice to be able to perform staging based on any types,
including abstract types.
This would provide a way to generate fewer specializations, and could
aid static compilation (by generating code for the most general type
\texttt{Tuple\{Any...\}}).
Unfortunately this appears to be impractical, due to the need for
functions to be monotonic in the type domain.
The soundness and termination of data flow analysis depend on the
property that given lattice elements $a$ and $b$, we must have
$a\subseteq b\ \implies\ f(a)\subseteq f(b)$ for all $f$.
Since staged methods can generate arbitrarily different code for
different types, it is easy to violate this property.
For the time being, we are forced to invoke staging only on concrete
types.

\subsubsection{Related work}

Our approach is closely related to Exotypes~\cite{DeVito:2014:FRG:2594291.2594307},
and to generation of high-performance code using lightweight modular staging
(LMS)~\cite{Rompf:2010:LMS:1868294.1868314,Ofenbeck:2013:SST:2517208.2517228}.
The primary difference is that in our case code generation is invoked
implicitly, and integrated directly with the method cache.
Unlike LMS, we do not do binding time analysis, so expression generation itself
is more ``manual'' in our system.
% we have not yet extended it to generating data types, only methods?

% spiral in scala:
% - uses types to do binding time analysis to decide what is staged
% - still uses explicit code generation
% our novelty: totally implicit, integrated with generic function method cache


\section{Higher-order programming}

Generic functions are first-class objects, and so can be passed as arguments
just as in any dynamically typed language with first-class functions.
However, assigning useful type tags to generic functions and deciding how
they should dispatch is not so simple.
Past work has often described the types of generic functions using the
``intersection of arrows'' formalism
\cite{RonchiDellaRocca:1988:PTS:55079.55086, Dunfield:2012:EIU:2364527.2364534,
boundedquant, Castagna:1995:COF:203496.203510}.
Since an ordinary function has an arrow type $A\rightarrow B$ describing how it
maps arguments $A$ to results $B$, a function with multiple definitions can
naturally be considered to have multiple such types.
For example, a \texttt{sin} function with the following two definitions:

\begin{singlespace}
\begin{lstlisting}[language=julia]
sin(x::Float64) = # compute sine of x in double precision
sin(v::Vector) = map(sin, v)
\end{lstlisting}
\end{singlespace}

\noindent
could have the type $(\texttt{Float64}\rightarrow\texttt{Float64})\cap(\texttt{Vector}\rightarrow\texttt{Vector})$.
The intuition is that this \texttt{sin} function can be
used both where a $\texttt{Float64}\rightarrow\texttt{Float64}$ function
is expected and where a $\texttt{Vector}\rightarrow\texttt{Vector}$ function is expected,
and therefore its type is the intersection of these types.

This approach is effective for statically checking uses of generic
functions: anywhere a function goes, we must keep track of which arrow
types it ``contains'' in order to be sure that at least one matches
every call site and allows the surrounding code to type check.
However, despite the naturalness of this typing of generic functions,
this formulation is quite problematic for dispatch and code specialization
(not to mention that it might make subtyping undecidable).

\subsection{Problems for code selection}

Consider what happens when we try to define an integration function:

\begin{singlespace}
\begin{lstlisting}[language=julia]
# 1-d integration of a real-valued function
integrate(f::Float64->Float64, x0, x1)

# multi-dimensional integration of a vector-valued function
integrate(f::Vector->Vector, v0, v1)
\end{lstlisting}
\end{singlespace}

\noindent
The \texttt{->} is not real Julia syntax, but is assumed for the sake of
this example.
Here we wish to select a different integration routine based on what
kind of function is to be integrated.
However, these definitions are ambiguous with respect to the \texttt{sin}
function defined above.
Of course, the potential for method ambiguities existed already.
However this sort of ambiguity is introduced \emph{non-locally} ---
it cannot be detected when the \texttt{integrate} methods are defined.

%re: selection:
%- feels like the wrong abstraction. GFs are the means of selecting behavior,
%- changes over time
%- might depend on inference results

Such a non-local introduction of ambiguity is a special case of the
general problem that a generic function's type would change depending
on what definitions have been added, which depends e.g.\ on which libraries
have been loaded.
This does not feel like the right abstraction:
type tags are supposed to form a ``ground truth'' about objects against
which program behavior can be selected.
Though generic functions change with the addition of methods, it would be more
satisfying for their types to somehow reflect an intrinsic, unchanging
property.

An additional minor problem with the intersection of arrows
interpretation is that we have found, in practice, that Julia methods
often have a large number of definitions.
For example, the \texttt{+} function in Julia v0.3.4 has 117 definitions,
and in a more recent development version with more functionality, it has
150 methods.
An intersection of 150 types would be unwieldy, even if only
inspected when debugging the compiler.

A slightly different approach we might try would be to imitate
the types of higher-order functions in traditional
statically typed functional languages.
Consider the classic \texttt{map} function, which creates a new container
by calling a given function on every element of a given container.
This is a general pattern that occurs in ``vectorized'' functions in
technical computing environments, e.g.\ when a function like \texttt{+}
or \texttt{sin} operates on arrays elementwise.
We might wish to write \texttt{map} as follows:

\begin{singlespace}
\begin{lstlisting}[language=julia]
map{A,B}(f::A->B, x::List{A}) =
  isempty(x) ? List{B}() : List{B}(f(head(x)), map(f, tail(x)))
\end{lstlisting}
\end{singlespace}

The idea is for the first argument to match any function, and not use
the arrow type for dispatch, thereby avoiding ambiguity problems.
Instead, immediately after method selection, values for \texttt{A} and
\texttt{B} would be determined using the element type of \texttt{x}
and the table of definitions of \texttt{f}.

Unfortunately it is not clear how exactly \texttt{B} should be
determined. We could require return type declarations on every method,
but this would adversely affect usability (such declarations would also
be helpful if we wanted to dispatch on arrow types, though they would
not solve the ambiguity problem). Or we could use type inference
of \texttt{f} on argument type \texttt{A}. This would not work very
well, since the result would depend on partly arbitrary heuristics.
Such heuristics are fine for analyzing a program, but
are not appropriate for determining the value of a user-visible
variable, as this would make program behavior unpredictable.

\subsection{Problems for code specialization}

For code specialization to be effective, it must eliminate as many
irrelevant cases as possible. Intersection types seem to be naturally
opposed to this process, since they have the ability to
generate infinite descending chains of ever-more-specific function
types by tacking on more terms with $\cap$. There would be no such
thing as a maximally specific function type. In particular, it would be
hard to express that a function has exactly one definition,
which is an especially important case for optimizing code.

For example, say we have a definition \texttt{f(g::String->String)},
and a function \texttt{h} with a single $\texttt{Int}\rightarrow\texttt{Int}$ definition.
Naturally, \texttt{f} is not applicable to \texttt{h}.
However, given the call site \texttt{f(h)}, we are forced to conclude
that \texttt{f} might be called with a function of type
\mbox{$(\texttt{Int}\rightarrow\texttt{Int})\cap(\texttt{String}\rightarrow\texttt{String})$},
since in general $\texttt{Int}\rightarrow\texttt{Int}$ might be only an
approximation of the true type of the argument.
% TODO so? wouldn't be able to exclude the method

%re: specialization:
%specialization wants to exclude irrelevant cases, and intersections
%*manufacture* irrelevant cases!
%- GFs have many methods and no two are the same in practice
%- there is no way to restrict a function to one definition

The other major concern when specializing code is whether, having generated code
for a certain type, we would be able to reuse that code often enough for the
effort to be worthwhile.
In the case of arrow types, this equates to asking how often generic functions
share the same set of signatures.
This question can be answered empirically.
Studying the Julia \texttt{Base} library as of this writing, there are 1059
generic functions. We examined all 560211 pairs of functions; summary
statistics are shown in table~\ref{tab:matchingfuncs}.
Overall, it is rare for functions to share type signatures.
Many of the 85 functions with matches (meaning there exists some other function
with the same type) are predicates, which all have types similar to
$\texttt{Any}\rightarrow \texttt{Bool}$. The mean of 0.23 means that if we
pick a function uniformly at random, on average 0.23 other functions will
match it.
The return types compared here depend on our heuristic type inference algorithm,
so it useful to exclude them in order to get an upper bound.
If we do that, and only consider arguments, the mean number of matches rises to 1.73.

\begin{table}
  \begin{center}
    \begin{tabular}{|l|r|r|r|}\hline
    &  \textbf{matching pairs} & \textbf{GFs with matches} & \textbf{mean} \\
      \hline \hline
arguments only             & 1831 (0.327\%)  &   329       &          1.73 \\
\hline
arguments and return types &  241 (0.043\%)  &   85        &          0.23 \\
\hline
\end{tabular}
\end{center}
  \caption[Sharing of function types]{
\small{
    Number and percentage of pairs of functions with matching arguments, or
    matching arguments and return types. The second column gives the number of
    functions that have matches. The third column gives the
    mean number of matches per function.
}
  }
  \label{tab:matchingfuncs}
\end{table}

The specific example of the \texttt{sin} and \texttt{cos} functions provides
some intuition for why there are so few matches.
One would guess that the type behavior of these functions would be identical,
however the above evaluation showed this not to be the case.
The reason is that the functions have definitions to make them operate
elementwise on both dense and sparse arrays.
\texttt{sin} maps zero to zero, but \texttt{cos} maps zero to one,
so \texttt{sin} of a sparse array gives a sparse array, but
\texttt{cos} of a sparse array gives a dense array.
This is indicative of the general ``messiness'' of convenient real-world
libraries for technical computing.
% todo conclusion


\subsection{Possible solutions}
\label{sec:nominalarrows}

%identity-typing
The general lack of sharing of generic function types suggests the first
possible solution: give each generic function a new type that is uniquely
associated with it. For example, the type of \texttt{sin} would be
\texttt{GenericFunction\{sin\}}. This type merely identifies the function
in question, and says nothing more about its behavior. It is easy to read,
and easily specific enough to avoid ambiguity and specialization
problems. It does \emph{not} solve the problem of
determining the result type of \texttt{map}. However there are
corresponding performance benefits, since specializing code for a
specific function argument naturally lends itself to inlining.

% todo: note that this is just a special case of specializing on a
% constant. however this analysis argues for specializing on constant
% functions by default, where specializing on other values by default
% is less surely a good idea.

%nominal function types
Another approach that is especially relevant to technical computing is to use
nominal function types.
In mathematics, the argument and return types of a function are often not
its most interesting properties.
In some domains, for example, all functions can implicitly be assumed
$\mathbb{R}\rightarrow\mathbb{R}$, and the interesting property might be
what order of integrable singularity is present (see section~\ref{sec:BEM} for
an application), or what dimension of linear operator the function represents.
The idea of nominal function types is to describe the properties of interest
using a data object, and then allow that data object to be treated as a
function, i.e.\ ``called''. Some object-oriented languages call such an object
a \emph{functor}.

Julia accommodates this approach with the \texttt{call} mechanism used for
constructors (see section \ref{sec:constructors}).

As an example, we can define a type for polynomials of order $N$ over ring
$R$:

\begin{singlespace}
\begin{lstlisting}[language=julia]
immutable Polynomial{N,R}
    coeffs::Vector{R}
end

function call{N}(p::Polynomial{N}, x)
    v = p.coeffs[end]
    for i = N:-1:1
        v = v*x + p.coeffs[i]
    end
    return v
end
\end{lstlisting}
\end{singlespace}

\noindent
Now it is possible to use a \texttt{Polynomial} just like a function, while
also dispatching methods on the relevant properties of order and ring
(or ignoring them if you prefer).
It is also easy to examine the polynomial's coefficients, in contrast to
functions, which are usually opaque.

% nominal types that classify algorithms, e.g. whether a sort is stable

Another possible use of this feature is to implement automatic vectorization
of scalar functions, as found in Chapel~\cite{chamberlain2007parallel}.
Only one definition would be needed to lift any declared subtype of
\texttt{ScalarFunction} to arrays:

\begin{singlespace}
\begin{lstlisting}[language=julia]
call(f::ScalarFunction, a::AbstractArray) = map(f, a)
\end{lstlisting}
\end{singlespace}

It is even possible to define a ``nominal arrow'' type, which uses this
mechanism to impose a classification on functions based on argument and
return types:

\begin{samepage}
\begin{singlespace}
\begin{lstlisting}[language=julia]
immutable Arrow{A,B}
    f
end

call{A,B}(a::Arrow{A,B}, x::A) = a.f(x)::B
\end{lstlisting}
\end{singlespace}
\end{samepage}

\noindent
Calling an \texttt{Arrow} will yield a no-method error if the argument
type fails to match, and a type error if the return type fails to
match.

% TODO
%It is worth examining the differences and tradeoffs between nominal
%functions and ``real'' arrow types.

% tradeoffs: arrows group all functions together, which is flexible,
% but nominal functions let you make more distinctions.

% arrow types without intersections, used to ``slice'' generic functions

% (generic functions with declared overall types)

\subsection{Implementing \texttt{map}}
\label{sec:implementingmap}

So, given typed containers and no arrow types, how do you implement
\texttt{map}? The answer is that the type of container to return must
also be computed. This should not be too surprising, since it is implied by
the definition of \texttt{new} at the beginning of the chapter: each
value is created by computing a type part and a content part.
% also recall the vandermonde example in chapter 2 explicitly
% computed the result type. this is common in T.C.

\begin{singlespace}
\begin{figure}[!t]
\begin{lstlisting}[language=julia]
function map(f, A::Array)
    isempty(A) && return Array(Bottom, 0)
    el = f(A[1]); T = typeof(el)
    dest = Array(T, length(A))
    dest[1] = el
    for i = 2:length(A)
        el = f(A[i]); S = typeof(el)
        if !(S <: T)
            T = typejoin(T, S)
            new = similar(dest, T)
            copy!(new, 1, dest, 1, i-1)
            dest = new
        end
        dest[i] = el::T
    end
    return dest
end
\end{lstlisting}
  \caption[An implementation of \texttt{map}]{
\small{
    A Julia implementation of \texttt{map}.
    The result type depends only on the actual values computed, made
    efficient using an optimistic assumption.
}
  }
  \label{fig:mapimpl}
\end{figure}
\end{singlespace}

A possible implementation of \texttt{map} for arrays is shown in
figure~\ref{fig:mapimpl}.
The basic strategy is to try calling the argument function \texttt{f}
first, see what it returns, and then optimistically assume that it
will always return values of the same type.
This assumption is checked on each iteration.
If \texttt{f} returns a value that does not fit in the current output
array \texttt{dest}, we re-allocate the output array to a larger
type and continue.
The primitive \texttt{typejoin} computes a union-free join of types.
For uses like \texttt{map}, this does not need to be a true least
upper bound; any reasonable upper bound will do.

This implementation works well because it completely ignores the
question of whether the compiler understands the type behavior of
\texttt{f}.
However, it \emph{cooperates} with the compiler by making the
optimistic assumption that \texttt{f} is well-behaved.
This is best illuminated by considering three cases.
In the first case, imagine \texttt{f} always returns \texttt{Int},
and that the compiler is able to infer that fact.
Then the test \texttt{!(S <:\ T)} disappears by specialization,
and the code reduces to the same simple and efficient loop we
might write by hand.
In the second case, imagine \texttt{f} always returns \texttt{Int},
but that the compiler is \emph{not} able to infer this.
Then we incur the cost of an extra type check on each iteration,
but we return the same efficiently stored \texttt{Int}-specialized
\texttt{Array} (\texttt{Array\{Int\}}).
This leads to significant memory savings, and allows subsequent
operations on the returned array to be more efficient.
The third case occurs when \texttt{f} returns objects of different
types.
Then the code does not do anything particularly efficient, but is
not much worse than a typical dynamically typed language manipulating
heterogeneous arrays.

Overall, the resulting behavior is quite similar to a dynamic
language that uses storage strategies \cite{Bolz2013} for its
collections.
The main difference is that the behavior is implemented at the
library level, rather than inside the runtime system.
This can be a good thing, since one might want a \texttt{map} that
works differently.
For example, replacing \texttt{typejoin} with \texttt{promote\_type}
would collect results of different numeric types into a
homogeneous array of a single larger numeric type.
Other applications might not want to use typed arrays at all, in
which case \texttt{map} can be much simpler and always return an
\texttt{Array\{Any\}}.
Still other applications might want to arbitrarily mutate the result
of \texttt{map}, in which case it is difficult for any automated
process to predict what type of array is wanted.

It must be admitted that this \texttt{map} is more complex than
what we are used to in typical functional languages.
However, this is at least partly due to \texttt{map} itself
being more complex, and amenable to more different interpretations,
than what is usually considered in the context of those languages.

% while ML gets the type of the map function itself totally right,
% programmers often care more about the type of container it returns at
% run time.


\section{Performance}

\subsection{Type inference}

Our compiler performs data flow type inference~\cite{kaplanullman,abstractinterp}
using a graph-free algorithm~\cite{graphfree}.
Type inference is invoked on a method cache miss, and recursively follows the
call graph emanating from the analyzed function.
The first non-trivial function examined tends to cause a large fraction of
loaded code to be processed.

The algorithmic components needed for this process to work are subtyping
(already covered), join (which can be computed by forming a union type),
meet ($\sqcap$), widening operators, and type domain implementations
(also known as transfer functions) of core language constructs.

Meets are challenging to compute, and we do not yet have an algorithm for
it that is as rigorously developed as our subtyping.
Our current implementation traverses two types, recursively applying the
rules

\vspace{-3ex}
\begin{singlespace}
\begin{align*}
T\leq S  \implies &\ T\sqcap S = T \\
S\leq T  \implies &\ T\sqcap S = S \\
         otherwise\ &\ T\sqcap S = \bot
\end{align*}
\end{singlespace}

\noindent
As this is done, constraints on all variables are accumulated, and then
solved.
$(A\cup B)\sqcap C$ is computed as $(A\sqcap C) \cup (B\sqcap C)$.
Due to the way meet is used, it is safe for it to over estimate its
result.
That will only cause us to conclude that more methods are applicable
than really are, leading to coarser but still sound type inference.
Note that for concrete type $T$, the rule
$T\leq S \implies T\sqcap S = T$ suffices.

Widening is needed in three places:

\begin{itemize}
\item Function argument lists that grow in length moving down the call stack.
\item Computing the type of a field. Instantiating field types builds up
other types, potentially leading to infinite chains.
\item When types from two control flow paths are merged.
\end{itemize}

\noindent
Each kind of type has a corresponding form of widening.
A type nested too deeply can be replaced by a \texttt{UnionAll} type
with variables replacing each component that extends beyond a certain
fixed depth.
A union type can be widened using a union-free join of its components.
A long tuple type is widened to a variadic tuple type.

Since the language has few core constructs, not many transfer functions
are needed, but the type system requires them to be fairly sophisticated.
For example accessing an unknown index of \texttt{Tuple\{Int...\}} can
still conclude that the result type is \texttt{Int}.
The most important rule is the one for generic functions:

\[
T(f,t_{arg}) = \bigsqcup_{(s,g) \in f}T(g,t_{arg} \sqcap s)
\]

\noindent
where $T$ is the type inference function.
$t_{arg}$ is the inferred argument tuple type.
The tuples $(s,g)$ represent the signatures $s$ and their associated
definitions $g$ within generic function $f$.


\subsection{Specialization}

It might be thought that Julia is fast because our compiler is well
engineered, perhaps using ``every trick in the book''.
At risk of being self-deprecating, this is not the case.
After type inference we apply standard optimizations: static method
resolution, inlining, specializing variable storage, eliminating tuples
that do not escape local scope, unboxing function arguments, and
replacing known function calls with equivalent instruction sequences.

The performance we manage to get derives from language design.
Writing complex functions with many behaviors as generic functions
naturally encourages them to be written in a style that is easier to
analyze statically.
% the dispatch specs are the things we can analyze

Julia specializes methods for nearly every combination of concrete
argument types that occurs.
This is undeniably expensive, and past work has often sought to avoid
% user-directed type-based specialization in scala
or limit specialization (e.g.\ \cite{Dragos:2009:CGT:1565824.1565830}).
% we find it is the right default
However, in our case specialization is a key feature of the performance
model.

Specialization is directed by the method cache; a specialization of a
method is generated when a corresponding entry is added to the
cache.
In general, the purpose of the method cache is to implement a lookup
table keyed by a subset of the type system that can support fast
lookup.
A basic implementation would support only concrete types.
However this would imply specializing on every type signature
without exception.
We have found it effective to apply a carefully designed widening operator
to type signatures to reduce the amount of specialization.
The core of the idea is to enhance the method cache with support for
variadic tuples and the types \texttt{Any} and \texttt{Type}.
With this, we are able to avoid specializing methods for argument lists
of every length and for all types \texttt{Type\{T\}}.
Details of the heuristics and measurements of their effectiveness are
given in \cite{bezansonmsthesis}.

% it's interesting to note that java generics did not originally support
% types like int and float as parameters. in T.C. those are practically
% the only types you want to support!

\iffalse
\subsection{Method changes}
% TODO
You can always specialize on constants, but you might want to specialize
on the current state of something that changes.
This is really difficult to do.
A system for adding methods as code is loaded provides this.
Method tables can be seen as elaborate mutable hash tables that come with
a protocol for keeping the system consistent under changes.
\fi


\subsection{Performance predictability}

Performance predictability is one of the main sacrifices of our design.
There are three traps: widening (which is heuristic), changing the type
of a variable, and heterogeneous containers (e.g.\ arrays of \texttt{Any}).
These can cause significant slowdowns for reasons that may be unclear to
the programmer.
To address this, we provide a sampling profiler as well as the ability to
examine the results of type inference.
The package \texttt{TypeCheck.jl}~\cite{typecheckjl} can also be used to
provide warnings about poorly-typed code.

%- use dispatch wherever possible
%- the values of parameters are specialized on


\section{Dispatch utilization}

\begin{table}[!t]
\begin{center}
\begin{tabular}{|l|r|r|r|}\hline
\textbf{Language} & \textbf{DR} & \textbf{CR} & \textbf{DoS} \\
\hline \hline
Gwydion    & 1.74 & 18.27 & 2.14 \\
\hline
OpenDylan  & 2.51 & 43.84 & 1.23 \\
\hline
CMUCL      & 2.03 &  6.34 & 1.17 \\
\hline
SBCL       & 2.37 & 26.57 & 1.11 \\
\hline
McCLIM     & 2.32 & 15.43 & 1.17 \\
\hline
Vortex     & 2.33 & 63.30 & 1.06 \\
\hline
Whirlwind  & 2.07 & 31.65 & 0.71 \\
\hline
NiceC      & 1.36 &  3.46 & 0.33 \\
\hline
LocStack   & 1.50 &  8.92 & 1.02 \\
\hline
Julia      & 5.86 & 51.44 & 1.54 \\
\hline
Julia Operators & 28.13 & 78.06 & 2.01 \\
\hline
\end{tabular}
\end{center}
\caption[Multiple dispatch use statistics]{
\small{
Comparison of Julia (1208 functions exported from the \texttt{Base} library)
to other languages with multiple dispatch, based on dispatch ratio (DR),
choice ratio (CR), and degree of specialization (DoS) \cite{multipledispatch}.
The ``Julia Operators'' row describes 47 functions with special syntax
(binary operators, indexing, and concatenation).
}
}
\label{dispatchratios}
\end{table}

To evaluate how dispatch is actually used in our application domain,
we applied the following metrics \cite{multipledispatch}:

\begin{enumerate}
\item Dispatch ratio (DR): The average number of methods in a generic function.
\item Choice ratio (CR): For each method, the total number of methods over all
generic functions it belongs to, averaged over all methods.
This is essentially the sum of the squares of the number of methods in each
generic function, divided by the total number of methods.
The intent of this statistic is to give more weight to functions with a large
number of methods.
\item Degree of specialization (DoS): The average number of type-specialized
arguments per method.
\end{enumerate}

Table~\ref{dispatchratios} shows the mean of each metric over the entire Julia
\code{Base} library, showing a high degree of multiple dispatch compared with
corpora in other languages \cite{multipledispatch}.
Compared to most multiple dispatch systems, Julia functions tend to have a large
number of definitions.
To see why this might be, it helps to compare results from a biased sample of
only operators.
These functions are the most obvious candidates for multiple dispatch, and as
a result their statistics climb dramatically.
Julia has an unusually large proportion of functions with this character.
% this gives us some confidence that we picked the right abstraction