declsub.tex

While the semantic approach does enable intuitive set-theo\-re\-tic
reasoning about subtyping,
a subtyping relation also needs to be computable.
However, the semantic definition~\eqref{eq:truesemsub-def}
does not suit this purpose,
as it operates on interpretations.
In the general case, the interpretation of a type 
can be an infinite set, and as such, it cannot be computed.
In the finite case, generating the interpretation sets
and checking the subset relation on them would be inefficient.
Therefore, we provide an alternative, \emph{syntactic} definition of subtyping 
that is equivalent to~\eqref{eq:truesemsub-def}
and straightforward to implement.

We do this in two steps. 
First, we give an inductive \emph{declarative} definition
that is handy to reason about 
and prove it equivalent to the semantic definition.
Second, we provide a \emph{reductive} analytic\footnote{Inference rules
	are called \emph{analytic}~\cite{bib:Martin-Lof1994} 
	if there is a finite number of rules applicable to a judgment,
    and the premises of each rule are comprised of the subcomponents 
	of its conclusion. Such rules give rise to a straightforward 
	bottom-up algorithm.
	If there is always only one rule applicable to a judgment,
	analytic rules are called \emph{syntax-directed}.}
definition of subtyping
and prove it equivalent to the declarative one 
(and, hence, the semantic definition as well).
We prove that the reductive subtyping relation is decidable, 
i.e. for any two types $\ty_1$ and $\ty_2$,
it is possible to prove that either $\ty_1$ is a subtype of $\ty_2$ 
or it is not.
The proofs are mechanized in Coq, and since Coq logic is constructive,
the decidability proof is also a subtyping algorithm.
The algorithm can also be implemented as a straightforward recursive function.

\subsection{Declarative Subtyping}\label{sec:declsub}
%% -----------------------------------------------------------------------------

The declarative syntactic definition of subtyping is provided in~\figref{fig:bjsem-decl-sub}.
It comprises most of the standard rules
of syntactic subtyping for unions and pairs:
reflexivity and transitivity (\RD{Refl} and \RD{Trans}), 
subtyping of pairs (\RD{Pairs}),
and subtyping of unions (\RD{UnionL}, \RD{UnionR1}, \RD{UnionR2}).
Though \RD{UnionR*} rules are seemingly very strict 
(they require the left-hand side type to be syntactically equivalent
to a part of the right-hand side type), 
transitivity allows us to derive judgments such as
$\bjsub{\tyint}{(\tyunion{\tystr}{\tyreal})}$ via
$\bjsub{\tyint}{\tyreal}$ and $\bjsub{\tyreal}{\tyunion{\tystr}{\tyreal}}$.

Note that all rules from~\figref{fig:bjsem-decl-sub} \emph{are essential} 
for the definition to be equivalent to semantic subtyping.
Thus, for example, the syntactic definition needs to be
{reflexive} and {transitive} because so is the subset relation,
which is used to define semantic subtyping.
Semantic subtyping also forces us to add rules 
for distributing pairs over unions, \RD{Distr1} and \RD{Distr2}. 
For instance, consider two types,
\typair{\tystr}{(\tyunion{\tyint}{\tyflt})}
and \tyunion{(\typair{\tystr}{\tyint})}{(\typair{\tystr}{\tyflt})}.
They have the same semantic interpretation~---
$\{\typair{\tystr}{\tyint}, \typair{\tystr}{\tyflt}\}$~---
so they are equivalent.
Therefore, we should also be able to derive their equivalence
using the declarative definition,
i.e. declarative subtyping should hold in both directions.
One direction is trivial:
\begin{mathpar}{\small
\inferrule*[right=]
{ \inferrule*[right=]
  { \bjsub{\tystr}{\tystr} \\ \bjsub{\tyint}{\tyunion{\tyint}{\tyflt}} }
  { \bjsub{\typair{\tystr}{\tyint}}
  	  {\typair{\tystr}{(\tyunion{\tyint}{\tyflt})}} } \\
  \inferrule*[right=]
  { \ldots }
  { \bjsub{\typair{\tystr}{\tyflt}}
  	  {\ldots} } }
{ \bjsub{\tyunion{(\typair{\tystr}{\tyint})}{(\typair{\tystr}{\tyflt})}}
	{\typair{\tystr}{(\tyunion{\tyint}{\tyflt})}} }.
}\end{mathpar}
But the other direction,  
\[
\bjsub{\typair{\tystr}{(\tyunion{\tyint}{\tyflt})}}
  {\tyunion{(\typair{\tystr}{\tyint})}{(\typair{\tystr}{\tyflt})}},
\]
cannot be derived without \RD{Distr2} rule. 
%\typair{\tystr}{(\tyunion{\tyint}{\tyflt})} is 
%not a subtype of either \typair{\tystr}{\tyint} or \typair{\tystr}{\tyflt},
%so we cannot apply \RD{UnionR*} rules\footnote{Transitivity
%  does not help in this case.}.

The novel part of the definition resides in subtyping of nominal types.
There are four obvious rules coming directly 
from the nominal hierarchy, for instance, \RD{RealNum} mirrors the fact 
that $\bjdeclsub{\tyreal}{\tynum} \in \NomH$.
%Using these rules, judgments such as $\bjsub{\tyint}{\tynum}$ 
%can be derived by transitivity.
But the rules \RD{RealUnion} and \RD{NumUnion}
(\colorbox{light-gray}{highlighted} in~\figref{fig:bjsem-decl-sub})
are new, dictated by semantic subtyping.
Thus, \RD{RealUnion} allows us to prove the equivalence
of types \tyunion{\tyint}{\tyflt} and \tyreal, 
which are both interpreted as $\{\tyint, \tyflt\}$.

%Before we define an inductive declarative relation $\bjsub{\ty_1}{\ty_2}$.

%Besides, the ability to reason about types directly,
%without appealing to all their value subtypes.
%Therefore, we provide  definitions of subtyping
%in the form of inductive rule

\begin{figure}
	\begin{mathpar}
		\fbox{$\bjsub{\ty}{\ty'}$}\\
		
		\inferrule*[right=SD-Refl]
		{ }
		{ \bjsub{\ty}{\ty} }
		
		\inferrule*[right=SD-Trans]
		{ \bjsub{\ty_1}{\ty_2} \\ \bjsub{\ty_2}{\ty_3} }
		{ \bjsub{\ty_1}{\ty_3} }		
		\\
		
		\inferrule[SD-IntReal]
		{ }
		{ \bjsub{\tyint}{\tyreal} }
		
		\inferrule[SD-FltReal]
		{ }
		{ \bjsub{\tyflt}{\tyreal} }
		\\
		
		\inferrule[{SD-RealNum}]
		{ }
		{ \bjsub{\tyreal}{\tynum} }
	
		\inferrule[{SD-CmplxNum}]
		{ }
		{ \bjsub{\tycmplx}{\tynum} }
		\\
		
		\colorbox{light-gray}{$
		\inferrule[SD-RealUnion]
		{ }
		{ \bjsub{\tyreal}{\tyunion{\tyint}{\tyflt}} }
		$}
		
		\colorbox{light-gray}{$
		\inferrule[SD-NumUnion]
		{ }
		{ \bjsub{\tynum}{\tyunion{\tyreal}{\tycmplx}} }
		$}
		\\
		
		\inferrule*[right=SD-Pair]
		{ \bjsub{\ty_1}{\ty'_1} \\ \bjsub{\ty_2}{\ty'_2} }
		{ \bjsub{\typair{\ty_1}{\ty_2}}{\typair{\ty'_1}{\ty'_2}} }
		\\
		
		\inferrule[SD-UnionL]
		{ \bjsub{\ty_1}{\ty'} \\ \bjsub{\ty_2}{\ty'} }
		{ \bjsub{\tyunion{\ty_1}{\ty_2}}{\ty'} }
		
		\inferrule[{SD-UnionR1}]
		{ }
		{ \bjsub{\ty_1}{\tyunion{\ty_1}{\ty_2}} }
		
		\inferrule[{SD-UnionR2}]
		{ }
		{ \bjsub{\ty_2}{\tyunion{\ty_1}{\ty_2}} }
		\\
		
		\inferrule*[right=SD-Distr1]
		{ }
		{ \bjsub{\typair{(\tyunion{\ty_{11}}{\ty_{12}})}{\ty_2}}
			{\tyunion{(\typair{\ty_{11}}{\ty_2})}{(\typair{\ty_{12}}{\ty_2})}} }
		
		\inferrule*[right=SD-Distr2]
		{ }
		{ \bjsub{\typair{\ty_1}{(\tyunion{\ty_{21}}{\ty_{22}})}}
			{\tyunion{(\typair{\ty_1}{\ty_{21}})}{(\typair{\ty_1}{\ty_{22}})}} }
	\end{mathpar}
	\caption{Declarative subtyping for \BetaJulia}
	\label{fig:bjsem-decl-sub}
\end{figure}