intro.tex

%Subtyping is utilized by many static type systems.
%Informally, a subtyping relation \jltype{T $<:$ S} states that
%a value of type~\jltype{T} can be safely used
%in a context that expects a value of type~\jltype{S}.
%For example, if class \jltype{Rectangle} is a subtype of class \jltype{Shape},
%then a function with an argument of type \jltype{Shape}
%can be safely called with an instance of \jltype{Rectangle}. 

In static type systems, subtyping is used to determine
when a value of one type can be safely used at another type.
It is often convenient to think of subtyping \jltype{T $<:$ S}
in terms of the set inclusion: ``the elements of~\jltype{T} are a subset
of the elements of~\jltype{S}''~\cite{bib:Pierce:2002:TAPL}.
This intuition is not always correct, but, in the case of
\emph{semantic subtyping}~\cite{bib:Hosoya:2003:XDuce,
	bib:Frisch:2008:sem-sub, bib:Ancona:2016:sem-sub-oo}, 
subtyping is defined exactly as the subset relation. % on values.
Under semantic subtyping, types are interpreted as sets
$\interpty{\ty} = \{\nu \Alt \vdash \nu : \ty \}$, 
and subtyping $\ty_1 <: \ty_2$ is defined as inclusion 
of the interpretations
$\interpty{\ty_1} \subseteq \interpty{\ty_2}$.

Subtyping can also be used for run-time dispatch of function calls.
For example, object-oriented languages
usually support single dispatch~--- the ability to dispatch a method call 
based on the run-time type of the receiver object.
A more complex form of dispatch is \emph{multiple dispatch}
(MD)~\cite{bib:Chambers:1992:Cecil,bib:Clifton:2000:MultiJava},
which takes into account run-time types of \emph{all} arguments
when dispatching a function call.
One way to implement MD is to interpret both function signatures
and function calls
as tuple types~\cite{bib:Leavens:1998:mddtuples}
and then use subtyping on these types.

Dynamic dispatch is not limited to statically typed languages,
with multiple dispatch being even more widespread among 
\emph{dynamically} typed ones, e.g., CLOS, Julia, Clojure.
Unlike statically typed languages, 
which conservatively prevent type errors at compile-time, %with static checking,
dynamic languages detect type errors at run-time:
whenever an operator is restricted to certain kinds of values,
the run-time system checks \emph{type tags} associated 
with the operator's arguments
to determine whether it can be safely executed.
A type tag indicates the run-time type of a value.
Thus, any class that can be instantiated induces a tag~--- 
the name of the class~--- 
whereas an abstract class or interface does not.
Some structural types also give rise to tags, 
e.g., tuples and sums (tagged unions).

While dynamically typed languages do use subtyping,
semantic subtyping is not applicable in this case,
for the semantic definition refers to a static typing relation.
To enable semantic reasoning in the context of dynamic languages,
we propose \emph{tag-based semantic} subtyping
where a type is interpreted as a set of run-time type tags 
instead of values. % but is otherwise similar to semantic subtyping.

We define tag-based semantic subtyping for a fragment 
of the Julia language~\cite{bezanson2017julia}
that includes nominal types, tuples, and unions.
Tuples and unions are rather typical for semantic subtyping systems;
they have a clear set-theoretic interpretation 
and make up an expressive subtyping relation
where tuples distribute over unions.
At the same time, to the best of our knowledge,
the interaction of unions with \emph{nominal} types has not been studied before
in the context of semantic subtyping.
This interaction introduces
an unusual subtyping rule between abstract nominal types and unions,
with implications for multiple dispatch.
Note that the combination of unions and nominal types is not unique to Julia;
for instance, it also appears in the statically typed language 
Ceylon~\cite{bib:CeylonSpec:1:3}.

Our contributions are as follows:
\begin{enumerate}
  \item A definition of tag-based semantic subtyping for 
    nominal types, tuples, and unions (\secref{sec:semsub}).
  \item Two syntactic definitions of subtyping, 
    declarative (\secref{sec:declsub}) and reductive (\secref{sec:redsub}),
    along with Coq-mechanized proofs that these definitions are equivalent
    and coincide with the semantic definition (\secref{sec:proofs}). 	
  \item Proof of decidability of reductive subtyping (\appref{app:proofs}).
  \item Discussion of the implications of using semantic subtyping
    for multiple dispatch, as well as an alternative semantic interpretation
    of nominal types (\secref{sec:discussion}).
\end{enumerate}