%% information can also be treated as type information, i.e. whenever
%% the type can be checked (inferred), the execution costs and the
%% relational cost can also be checked (inferred) as well.
% Below, we
% describe {\bitname}'s bidirectional typechecking judgments in which
% the outputs are represented in {\color{red} red} and the inputs are
% represented in {\color{black} black}.

\subsection{Algorithmic typechecking as constraint satisfaction}
% To develop the bidirectional type system, we add some syntactic
% classes and extend the existing ones.

% \[ \begin{array}{@{}l@{~~}l@{~}l@{~}l@{}l}
%     \text{meta~variables} & M & \bnfdef & i,n,m, \cdots \\
%     \text{index~terms} & I,k,t & \bnfdef & \cdots~|~ M \\
%     \text{meta~contexts} & \psi &  \bnfdef & \emptyset~ |~ \psi, M : \sort\\
%     \text{meta~substitutions} & \theta &  \bnfdef & []~ |~ \theta[M \mapsto I]\\
%     \text{constraints} & C &  \bnfdef & \cdots ~ |~ \cforallS{i}{S}{C} ~|~ \cexistsK{i}{S}{C} \\
%     \text{expressions} & e &  \bnfdef & \cdots ~ |~ \eanno{e}{\grt}{k}{t} ~|~ \eannobi{e}{\tau}{t} \\
%     \end{array}\]
% One class of note is the meta variables $i, n, m$, etc. Also known as
% existential variables, meta variables represent unknown index terms
% that appear in types and costs. These meta variables are resolved by
% constraint solving.
In the expression syntax of {\bitname}, we modify the type-annoated
expressions with cost: $\eanno{e}{\grt}{k}{t} $ and
$\eannobi{e}{\tau}{t}$. % Since {\tnamemin} has two typing judgments---a unary judgment and a
% relational judgment---{\bitname} has four mutually recursive
% algorithmic typing judgments: one each to synthesize and check a unary
% type, and one each to synthesize and check a relational type.
relational checking judgment
$\Delta; \psi_a; \Phi_a; \Gamma \chdiff{e_1}{e_2}{\tau}{t}{\Phi}$
% means that, \emph{assuming that the constraint \textcolor{red}{$\Phi$}
%   holds}, $e_1$ and $e_2$ check against the relational input type
% $\tau$ and
takes as input the relative cost $t$. % under the assumption $\Phi_a$.
% All
% index and meta variables must occur in $\Delta$ and $\psi_a$. When the
% judgment is read operationally or is implemented, the constraint
% \textcolor{red}{$\Phi$} is an output; all other components are
% inputs. (As a convention, we write all outputs in \textcolor{red}{red}
% and all inputs in black.)
The relational inference judgment
$\Delta; \psi_a; \Phi_a; \Gamma
\infdiff{e_1}{e_2}{\tau}{\psi}{t}{\Phi}$ % means that, if
% \textcolor{red}{$\Phi$} holds, then it can be inferred that the
% relational type of $e_1$ and $e_2$ is \textcolor{red}{$\tau$} and
outputs the relative cost \textcolor{red}{$t$}%  under the assumption
% $\exists {\color{red} \psi}. {\color{red} \Phi_a}$. Here,
% \textcolor{red}{$\Phi$}, \textcolor{red}{$\tau$},
% \textcolor{red}{$\psi$} and \textcolor{red}{$t$} are all outputs.
meta variable context \textcolor{red}{$\psi$} tracks newly generated
cost variables that may appear in the inferred type or cost. Its
significance will be explained below.

% Intuitively, the checking mode is used when the surrounding
% outer context determines the type and the cost of the expression. This
% happens at all introduction forms and in case-like elimination
% forms. The inference mode is used when there is no outer restriction
% on the type or the cost of an expression. This happens for the
% principal term in all elimination forms.

The unary checking and inference judgments, $\Delta; \psi_a; \Phi_a;
\Omega \chexec{e}{\grt}{k}{t}{\Phi}$ and $\Delta; \psi_a; \Phi_a;
\Omega \infexec{e}{\grt}{\psi}{k}{t}{\Phi}$, are to be understood

% The checking judgment of form
% $\Delta; \psi_a; \Phi_a; \Gamma \chdiff{e_1}{e_2}{\tau}{t}{\Phi}$
% means that $e$ checks against input type $\tau$ and cost $t$ under
% the assumption $\Phi_a$ in which all the index and meta variables
% are declared in $\Delta$ and $\psi_a$, respectively and it generates
% the constraint $\Phi$. Similarly, inference judgment of form
% $\Delta; \psi_a; \Phi_a; \Gamma
% \infdiff{e_1}{e_2}{\tau}{\psi}{t}{\Phi}$ means that $e_1$ and $e_2$
% synthesizes an output type $\tau$ and cost $t$ under the assumption
% $\Phi_a$ in which all the index and meta variables are declared in
% $\Delta$ and $\psi_a$, respectively and it also generates the
% constraint $\Phi$ and a context $\psi$ containing all the newly
% declared meta variables. The meta context $\psi_a$ (denoted on the
% left side of the $\vdash$) contains all the existential meta
% variables that occur in the checked type and cost which is
% determined by the surrounding outer context and $\psi_a$ is always
% given to both the inference and the checking judgments. On the other
% hand, the meta context $\psi$ (denoted on the right side of the
% $\vdash$) contains all the existential meta variables that occur in
% the synthesized type and cost, therefore it is generated only for
% the inference judgment. Their interaction is described below in
% detail in the algorithmic rule \textbf{alg-r-app$\uparrow$}.

% \ezgi{fix here: $\psi_a$ is not universally quantified. Need
%   to explain the purpose of $\psi$ and $\psi_a$.}  The variables in
% the meta context $\psi_a$ (given on the left side of the $\vdash$),
% can be thought as being universally quantified, whereas the
% variables in the meta context $\psi$ (defined only in the inference
% judgment) can be thought as being existentially quantified. The
% distinction will be explained in detail below.

\begin{figure}[t]
% \fbox{$\Delta; \psi_a; \Phi_a   \subtype{\grt_1}{\grt_2}{\Phi}$}~~~checks whether $\grt_1$ is a subtype of $\grt_2$ and generates constraints in $\Phi$\\
\fbox{$\Delta; \psi_a; \Phi_a \jalgeqtype{\tau_1}{\tau_2}{\Phi}$}~~~checks whether $\tau_1$ is equivalent to $\tau_2$ and generates constraints in $\Phi$\\
\begin{mathpar}
\astfunPLDI
\and
\astlistPLDI
\end{mathpar}
% \nocaptionrule

% Definitions at appendix/alg-type-eq-rules-defs.tex
\caption{Selected algorithmic type equivalence rules}
\label{fig:alg-type-eq-rules}
\end{figure}

\paragraph{Algorithmic typing rules}
and~\ref{fig:selected-alg-typing-rules2} list a few selected
algorithmic relational typing rules; algorithmic unary typing rules
follow similar guidelines (except that they track two costs) and,
hence, we omit them here. Since we already explain the main principles
in {\birelref}, we will focus on the principles related to cost and
discuss some selected rules.
% We first explain the main principles behind
% the bidirectional typing rules and then discuss selected rules. While
% some of these principles are standard, those related to cost are
% new.
We also highlight other {\bitname}-specific principles.
\begin{itemize}
% \item Types and costs of variables and elimination forms are inferred
%   (e.g., rules \textbf{alg-r-var}$\uparrow$,
%   \textbf{alg-r-app}$\uparrow$) whereas types and costs of
%   introduction forms are checked (e.g., rules
%   \textbf{alg-r-fix}$\downarrow$, \textbf{alg-r-consC}$\downarrow$).
%   There are a few exceptions to this principle: the type of the
%   branches in case analyses or the continuation in let-bindings is
%   checked.
\item (Specific to {\bitname}) If an expression consists of a
subexpression that must be checked against a type, we generate a
fresh meta variable for the subexpression's cost. This is necessary
since at the point we reach the subexpression, we don't know what
cost to check against. When we check the subexpression, constraints
that determine this meta variable are generated.  If the whole
expression is in checking mode, we existentially quantify over the
freshly generated variable in the constraint (e.g., rule
\textbf{alg-r-consC$\downarrow$}). If the whole expression is in
inference mode, we simply add the meta variable to the inferred cost
and append it to $\psi$ (e.g. rule \textbf{alg-r-app$\uparrow$}).
% \item In checking mode, if no other checking rule matches the given
%   expression, then the rule \textbf{alg-r-$\uparrow\downarrow$} allows
%   switching to inference mode in the premise. The requirement is that
%   the inferred type must be equivalent to the checked type and the
%   inferred cost must be no greater than the checked cost. In the
%   algorithmic system, we have an algorithmic type equivalence relation
%   $\jalgeqtype{\tau}{\tau'}{\Phi}$ whose selected rules are shown in
%   Figure~\ref{fig:alg-type-eq-rules}. The meaning of the judgment is
%   that if \textcolor{red}{$\Phi$} holds, then $\tau \pmb{\equiv}
%   \tau'$. Like other bidirectional systems, this is the only place
%   where type equivalence ({\tnamemin}'s reduct of subtyping) is used.
% \item In inference mode, it is permissible to switch to checking mode
%   when an expression's type and cost have been explicitly annotated by
%   the programmer (rule \textbf{alg-r-anno-$\uparrow$}). It can be shown that it suffices to annotate only at
%   explicit $\beta$-redexes (although there is no prohibition on
%   annotating at other places).
\item (Specific to {\bitname}) The algorithmic version of the rule
\textbf{c-nochange}, called \textbf{alg-r-nochange}, applies in
checking mode since it introduces the type $\tbox{\tau}$. The
algorithmic version of the rule \textbf{c-der}, called
\textbf{alg-r-der}, applies in inference mode since it eliminates
the type $\tbox{\tau}$.
\end{itemize}

% Switching to unary mode in {\bitname} is possible both in checking
% (rule \textbf{alg-r-switch-$\downarrow$}) and inference (rule
% \textbf{alg-r-switch-$\uparrow$}) modes. This is because often we
% switch to the unary mode for elimination forms where the eliminated
% type is of form $\tcho{\grt}$. Hence, since elimination forms can be
% typed both in inference mode (e.g.\ rule \textbf{alg-r-app-$\uparrow$})
% as well as checking mode (e.g.\ rule
% \textbf{alg-r-caseL-$\downarrow$}), to eliminate unnecessary
% annotations, {\bitname} supports two modes for typing $\eswitch$
% expressions.

Functions are typed in checking mode (rule
\textbf{alg-r-fix-$\downarrow$}) by checking the related function
bodies in the checking mode against the relative cost of the function
bodies. Since functions are values, we add the additional constraint
that the total cost of the functions, $t$, is equal to zero.  Dually,
function applications are typed in inference mode (rule
\textbf{alg-r-app-}$\uparrow$). We first infer the type and the cost
of the related functions and then use the (inferred) argument type to
switch to the checking mode for the related argument
expressions. Since we do not know the cost with which to check the
arguments, we also generate a fresh cost variable $t_2$ to check the
arguments. Finally, the result type is the return type of the inferred
function type, and the total cost is sum of the inferred cost for the
function, the relative cost of the bodies of the related functions and
$t_2$, the as-yet unknown cost of the arguments. Note that since all
the newly generated variables, i.e.\ $\psi$ and $t_2$, may occur in
the resulting type and the cost, inference mode passes them to the
surrounding context.

% \wq{consC explained in relref, without cost} The list constructors are typed in the checking mode. We explain only
% the rule \textbf{alg-r-consC-}$\downarrow$ for typing two non-empty
% lists with type $\tlist{n}{\alpha}{\tau}$ where the heads of the two
% lists may differ. The two related tails are checked with type
% $\tlist{i}{\beta}{\tau}$, where $i$ and $\beta$ are newly generated
% meta variables with the constraint that $\alpha=\beta+1$ and
% $n=i+1$. Since we do not know how the total cost $t$ is distributed
% between the heads and the tails, we generate two new cost variables
% $t_1$ and $t_2$ to check the heads and the tails, respectively and
% generate the constraint $t = t_1 + t_2$.

A particularly interesting aspect of bidirectional typing in
{\bitname} is that the effects (costs), both unary and relational, are
constraint-dependent. For example, the relative cost of a function's
body might depend on the sizes of its inputs. In this case, a
constraint will relate the cost and the inputs' sizes. In existing
bidirectional systems with refinement types, similar interactions show
up among the sizes of data structures like

%% What makes bidirectional typing in {\bitname} interesting is that
%% unary and relational effects are constraint-dependent: e.g. the
%% relational cost of a function might depend on the size of its inputs
%% on which constraints get accumulated as the derivation is
%% constructed. Just like in bidirectional systems for refinement
%% types~\cite{xi99:dependent}, things like list sizes are resolved using
%% constrains, here the costs are resolved in the same way.

%% The treatment of the comonadic type $\tbox{\tau}$ in {\bitname} is
%% worth mentioning: since $\enoch e$ is an introduction form, it is
%% typechecked in checking mode (rule
%% \textbf{alg-r-nochange$\downarrow$}) whereas $\eder e$ is an
%% elimination form, hence it is typechecked in the inference mode (rule
%% \textbf{alg-r-der$\uparrow$}).

% In
% addition to two standard judgments, we also have an additional
% judgment of form
% $\Delta; \psi_a; \Phi_a; \Gamma
% \chdiffNC{e_1}{e_2}{\tbox{\tau}}{t}{\Phi}$ which checks against the
% type $\tbox{\tau}$ and requires the cost to be $0$. This judgment
% corresponds to the non-deterministic \textbf{nochange} rule in
% {\tname} and has only a single algorithmic typing rule in
% {\bitname}: rule NC-$\downarrow$ checks that all free variables of
% $e$ are non-changing (by invoking algorithmic subtyping) and makes
% sure that the cost is 0. It is only invoked at specific points in
% {\bitname}: \textbf{caseL1}-$\downarrow$ and
% \textbf{cons}-$\downarrow$ rules.

% Variables are typed in the inference mode with 0 cost and an empty
% meta variable context since there is no generated meta variable
% (rule \textbf{alg-r-var}$\uparrow$). The rule \textbf{alg-r-consC$\downarrow$}

% In {\tname}, the expression
% $\econs(e_1,e_2)$ has two corresponding rules: \textbf{cons1} for
% stable head and \textbf{cons2} for possibly changing head. These two
% cases are handled simultaneously in the algorithmic rule
% \textbf{consCP}-$\downarrow$ by combining the resulting constraints
% with a disjunction. If $e_1$ can not change, then we check $e_1$
% with the nochange judgment and $e_2$ is allowed $\alpha$ changes. If
% $e_1$ can change, then $e_2$ is allowed $\beta$ changes, in which
% $\beta$ is a newly generated meta variable with a constraint
% $\beta+1 = \alpha$. In both cases, we generate a new meta variable
% $m$ for $e_2$'s size and add the constraint $m+1 = n$. For the cost
% of typechecking $e_1$, because we do not know how the total cost $t$
% is divided between two premises, we generate a new meta variable
% $t'$. Then, $e_2$ is checked with $t-t'$ cost. In all the premises,
% corresponding newly generated constraints are appended to the meta
% variable context $\psi_a$ for checking the premises. The final
% constraint quantifies over the generated meta variables
% existentially. % Typechecking $\cons{e_1}{e_2}$ in the $\vfr$ typing
% % mode is simpler since we do not have to care

% Rule $\textbf{caseL-}\downarrow$ typechecks the case analysis on
% lists. This rule looks complicated (/ is technically involved) since
% it incorporates a case analysis on the index domain, in particular
% on $\alpha$, the number of changes of the pattern-matched list of
% type $\tlist{n}{\alpha}{\tau}$. In {\tname}, such case analysis
% on the index domain is non-deterministic and is always used in
% combination with \textbf{nochange} rule. In {\bitname}, we make this
% reasoning deterministic by incorporating it into the
% $\textbf{caseL-}\downarrow$ rule by considering two cases : $\alpha
% = 0$ and $1 \leq \alpha$. For typechecking the body of the case when
% $\alpha=0$, we invoke the nochange checking judgment as well as the
% usual checking judgment; their constraints are combined with
% disjunction. Newly generated existential variables from the
% inference of the pattern-matched list are passed to the assumed meta
% context of body of the case and are quantified existentially in the
% final constraint.

% \ezgi{explain app rule}

% A technical subtlety worth mentioning is the treatment of
% existential variables in {\bitname}. In DML~\cite{xi99:dependent},
% existential variables are collected in a single context that is
% provided as an input for the checking mode and obtained as an output
% for the inference mode. However, whenever there is a switch from
% checking mode (which is given as an existential context $\psi$) to
% inference mode (which infers some existential context $\psi'$), the
% existential context $\psi$ must be adjusted to $\psi'$ by a
% weakening rule. Similarly, whenever inference mode invokes multiple
% inference modes, a similar adjustment is necessary to make sure that
% all free variables of the typing context are defined in the
% existential context. Instead, we employ two existential contexts for
% the inference mode: $\psi_a$ (a for assumed) that is given as an
% input containing all the existential variables from the outer
% context, and generated $\psi$ which is obtained as an output
% containing all the newly generated existential variables. The
% advantage of this approach is that we do not need to do such
% adjustments and our algorithmic typing rules directly correspond to
% the implementation.

% \paragraph{Algorithmic subtyping}
% Figure~% \ref{fig:alg-subtyping-rules}
% lists selected algorithmic
% subtyping rules. Similar to the algorithmic typing, algorithmic
% subtyping also generates a constraint. The algorithmic subtyping
% judgment $\Delta; \psi_a; \Phi_a \jalgeqtype{\tau}{\tau'}{\Phi}$
% means that under the context $\Delta$ and assumption $\Phi_a$ where
% the meta variables are defined in $\psi_a$, type $\tau$ is a subtype
% of $\tau'$ with respect to the subtyping mode $\epsilon$ if the
% constraint $\Phi$ is satisfied. Most of the rules are the same as
% {\tname}'s subtyping rules with additional constraint tracking. For
% list types in change-propagation mode, {\bitname} has a single rule
% \textbf{listCP} that combines \textbf{l1*} and \textbf{l2} rules of
% {\tname} with a disjunction.

\begin{figure*}
\raggedright
\fbox{$\Delta; \psi_a; \Phi_a; \Gamma
\chdiff{e_1}{e_2}{\tau}{t}{\Phi}$} ~$e_1$ and $e_2$ check against
the input type $\tau$
and the cost $t$ under the assumption $\Phi_a$ in which all the meta vars are declared in $\psi_a$ while generating the constraint $\Phi$.\\
\fbox{$\Delta; \psi_a ; \Phi_a; \Gamma
\infdiff{e_1}{e_2}{\tau}{\psi}{t}{\Phi}$} ~ $e_1$ and $e_2$
synthesize the output type $\tau$ and the cost $t$ under the
assumption $\Phi_a$ while generating the constraint $\Phi$ in which
all the newly generated meta vars are declared in $\psi$.

\begin{mathpar}
\infRswitch
\and
\chRswitch
\and
\chRnochange
\and
\infRder
\and
\chRupdown
\and
\chRsplit
% \chRder
% \and
% \infRvar
% \and
% \chRfix
% \and
% \infRapp
% \and
% \chRcons
% \and
% \chRconsbox
% \and
% \chRcaseL
% \and
% \chRsplit
\end{mathpar}

% \nocaptionrule
% Definitions at alg-typing-rules-defs.tex
\caption{Selected algorithmic typing rules (Part 1).}
\label{fig:selected-alg-typing-rules}
\end{figure*}

% \begin{figure*}
%   \begin{mathpar}
%     \chRiLam
%     \and
%     \infRiApp
%     \and
%     \chRcandElim
%     \and
%     \chRupdown
%     \and
%     \infRanno
%     \and
%     \chRsplit
%   \end{mathpar}
% \caption{Selected algorithmic typing rules (Part 2).}
% \label{fig:selected-alg-typing-rules2}
% \end{figure*}

\paragraph{Soundness and completeness}
We prove that the algorithmic type system is sound and complete
w.r.t.\ the type system of {\tnamemin}. Specifically, soundness says
that any inference or checking judgment provable in the algorithmic
type system can be simulated in {\tnamemin} if the output constraints
\textcolor{red}{$\Phi$} are satisfiable. Dually, completeness says
that any typeable {\tnamemin} program can be sufficiently annotated
(with types) to make its type checkable in {\bitname}, with
satisfiable output constraints. We define $\erty{e}$ to be the
function that erases typing annotations from a {\bitname} expression
$e$ to yield a {\tnamemin} expression. Important cases of its
definition are shown in the appendix.

% \begin{thm}[Soundness of algorithmic typechecking]\label{thm:alg-typing-soundness}
% \mbox{}
%   \begin{enumerate}
%   \item Assume $\uctx \chexec{e}{\grt}{k}{t}{\Phi}$ ,
%   \\ and $\fivars{\Phi_a,\Omega,\grt,k, t} \subseteq dom(\Delta,
%   \psi_a) $, \\
%     $\theta_a$ is a valid substitution for $\psi_a$ s.t.
%     $\Delta; \suba{\Phi_a} \sat \suba{\Phi}$ holds. Then,
%     $\Delta; \suba{\Phi_a}; \suba{\Omega}
%     \jtypeM{\suba{k}}{\suba{t}}{\erty{e}}{\suba{\grt}}$.

%   \item Assume that $\uctx \infexec{e}{\grt}{\psi}{k}{t}{\Phi}$ and
%     $\fivars{\Phi_a,\Omega} \subseteq dom(\Delta, \psi_a)$ and
%     $\theta$ and $ \theta_a$ are valid substitutions for $\psi$ and
%     $\psi_a$ such that $\Delta; \suba{\Phi_a} \sat \subta{\Phi}$
%     holds. Then,
%     $\Delta; \suba{\Phi_a}; \suba{\Omega}
%     \jtypeM{\subta{k}}{\subta{t}}{\erty{e}}{\subta{\grt}}$.
%     % and $\Delta; \psi_a; \Phi_a \awfty{\grt} $

% \item Assume that $\bctx \chdiff{e}{e'}{\tau}{t}{\Phi}$ and
%   $\fivars{\Phi_a,\Gamma,\tau,t} \subseteq dom(\Delta, \psi_a)$ and
%   $\theta_a$ is a valid substitution for $\psi_a$ such that
%   $\Delta; \suba{\Phi_a} \sat \suba{\Phi}$ holds. Then,
%   $\Delta; \suba{\Phi_a}; \suba{\Gamma}
%   \jtypediffM{\suba{t}}{\erty{e}}{\erty{e'}}{\suba{\tau}}$.

% \item Assume that $\bctx \infdiff{e}{e'}{\tau}{\psi}{t}{\Phi}$ and
%   $\fivars{\Phi_a,\Gamma} \subseteq dom(\Delta, \psi_a) $ and $\theta$
%   and $ \theta_a$ are valid substitutions for $\psi$ and $\psi_a$
%   such that $\Delta; \suba{\Phi_a} \sat \subta{\Phi}$ holds. Then,
%   $\Delta; \suba{\Phi_a}; \suba{\Gamma}
%   \jtypediffM{\subta{t}}{\erty{e}}{\erty{e'}}{\subta{\tau}}$.
% \end{enumerate}
% \end{thm}
% %
% \begin{proof}
% By simultaneous induction on the given algorithmic typing derivations.
% \end{proof}

% \begin{thm}[Completeness of algorithmic typechecking]\label{thm:alg-typing-completeness}
% \mbox{}
%   \begin{enumerate}
%   \item Assume that $\Delta; \Phi_a; \Omega \jtypeM{k}{t}{e}{\grt}$.
%     Then, there exists $ e'$ such that $\Delta; \cdot; \Phi_a; \Omega
%     \chexec{e'}{\grt}{k}{t}{\Phi}$ and $\Delta; \Phi_a \sat \Phi$ and
%     $\erty{e'} = e$.
%   \item Assume that $\Delta; \Phi_a; \Gamma
%     \jtypediffM{t}{e_1}{e_2}{\tau}$.  Then, there exist $e_1',e_2'$
%     such that $\Delta; \cdot; \Phi_a; \Gamma
%     \chdiff{e_1'}{e_2'}{\tau}{t}{\Phi}$ and $\Delta; \Phi_a \sat \Phi$
%     and $\erty{e_1'} = e_1$ and $\erty{e_2'} = e_2$.
%   \end{enumerate}
% \end{thm}
% %
% \begin{proof}
% By simultaneous induction on the given {\tnamemin} typing derivations.
% \end{proof}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{Implementation}
\label{sec:implementation}

We have implemented a bidirectional typechecker for {\tname} in
OCaml. The typechecker implements the checking and inference judgments
of {\bitname} but, to avoid overburdening the programmer, it works on
the compact terms (expressions) of {\tname} rather than the elaborate,
annotated terms of {\tnamemin}. Hence, the terms do not resolve all
the ambiguities of which (sub)typing rules to apply when. For this,
the typechecker uses heuristics that we designed carefully by looking
at a variety of examples. Conceptually, these heuristics are a sound
but incomplete implementation of the elaboration (embedding) from
{\tname} to {\tnamemin}.

The constraints output by the bidirectional rules are solved using a
combination of a custom procedure to eliminate existential variables
and an off-the-shelf SMT solver. We describe both the heuristics and
the constraint solving below.

Note that {\tname} is a conservative extension of {\relref} and
{\relinfref}. Any derivation in {\relref} or {\relinfref} can be
simulated in {\tname} by adding the trivial cost upper-bound of
$\infty$. As a result, our implementation can also be used for
{\relref} and {\relinfref}.

%% The typechecker uses example-guided heuristics to resolve the
%% nondeterminism in picking rules. In the theoretical development
%% described above, this nondeterminism was resolved in the elaboration
%% from {\tname} to {\tnamemin}, but that elaboration is not an
%% algorithm. After the nondeterminism has been resolved

%% We have implemented in OCaml a bidirectional type checker for \tname
%% (which subsumes all four languages {\relstlc, \relref,
%%   \relinfref}). For the purposes of presentation and also to make the
%% connection to the challenges of the algorithmization clear, we explain
%% relevant parts of the bidirectional typechecker in terms of the
%% respective languages below.

%% Our type checker accepts programs
%% %% not in the elaborate, annotated
%% %%  syntax of the core language \tnamemin (\relrefcore and \relinfrefcore
%% %%  respectively), which is rather inconvenient to use, but instead
%% in the syntax of \tname. Internally, it performs the embeddings
%%  presented in \Cref{sec:relrefcore,sec:relinfrefcore,sec:elab} using
%%  sound but incomplete heuristics to decide when to apply the
%%  nonsyntax-directed typing and subtyping rules. The bidirectional
%%  implementation is sound % in the sense of
%%  % Theorem~\ref{thm:alg-typing-soundness},
%%  and also complete % in the
%%  % sense of Theorem~\ref{thm:alg-typing-completeness}
%%  , modulo the
%%  incompleteness of our heuristics.
%% %% An implementation of {\tname} requires resolving the nondeterminism
%% %% inherent in {\tname} and implementing the
%% %% bidirectional type system, {\bitname}, for {\tnamemin}. In practice,
%% %% we have implemented (in OCaml) a bidirectional type system for
%% %% {\tname} that mimics {\bitname} but uses a set of heuristics to
%% %% resolve the nondeterminism in {\tname}'s rules, mirroring the
%% %% embedding of {\tname} to {\tnamemin}. The implementation is sound and
%% %% complete in the sense of Theorems~\ref{thm:alg-typing-soundness}
%% %% and~\ref{thm:alg-typing-completeness} on the fragment of {\tname}
%% %% corresponding to {\tnamemin}.

%% In the following, we describe our heuristics with respect to the
%% presented intermediate languages, give an overview of our
%% bidirectional implementation, and present the results of an
%% experimental evaluation along with a detailed description of two
%% examples demonstrating how some of the heuristics are useful for type
%% checking.

\paragraph{Heuristics}
We list below the main heuristics we use to reduce the nondeterminism
in picking (sub)typing rules.
%% The heuristics are mainly needed to treat the nondeterminism in the
%% relational typing and subtyping rules of \relref and \relinfref. With
%% the addition of unary and relational costs, heuristics are slightly
%% modified but the main idea stays the same.
%% \footnote{The heuristics are sound but incomplete. Since there is no
%%   standard library of examples for relational cost analysis so far, we
%%   designed our heuristics based on examples that cover a breadth of
%%   applications. The appendix lists all our examples, and our
%%   heuristics suffice for all of them. }
\begin{enumerate}[leftmargin=0cm,itemindent=.5cm,labelwidth=\itemindent,labelsep=0cm,align=left,itemsep=7pt,topsep=7pt]
\item \label{heur:cons} When typing a pair of $\econs$-ed lists, we
apply the bidirectional analogues of both the rules \textbf{rr-cons1}
and \textbf{rr-cons2} (\Cref{fig:relref-ts}) and combine the
resulting constraints via disjunction.
%% If neither of the rules fails, i.e.\ we are able
%% to generate constraints under which they might typecheck, we proceed
%% by combining the resulting constraints via disjunction.
%% Otherwise,
%% there are two cases: a) either both fail, whence we output a type
%% error without needing to solve any constraints, or b) one of them
%% fails, whence we return the constraints of the successful rule.

\item\label{heur:split} When typing a function that takes an argument
of type $\tlist{n}{\alpha}{\tau}$, we immediately apply the
algorithmic analogue of the rule \textbf{rr-split}
(\Cref{fig:relref-ts}) with $C = (\ceq{\alpha}{0})$. For the case
$\ceq{\alpha}{0}$, we first try to complete the typing by invoking
the rule \textbf{alg-r-nochange-$\downarrow$}
(\Cref{fig:selected-alg-typing-rules}). This is because we found
experimentally that many recursive list programs require this
analysis. Moreover, the rule \textbf{rr-split} is \emph{invertible}:
Applying the rule cannot cause backtracking during search.

\item\label{heur:subtyping} Subtyping is only invoked in three places:
(a) for switching from checking to inference mode (rule
\textbf{alg-r-}$\uparrow\downarrow$ in
\Cref{fig:selected-alg-typing-rules}), (b) for the algorithmic
version of the \textbf{nochange} rule
(\Cref{fig:synch-rel-typing-rules}), which checks subtyping on all
variables in the context, and (c) as mentioned in the next point.

\item \label{heur:box}
Relational subtyping rules that mention
$\tbox{}$ are applied lazily at specific elimination points. For
instance, in typing a function application, if the applied
expression's inferred type is $\tbox{(\tau_1 \tarrd{k} \tau_2)}$, we
try to complete the typing by subtyping to $\tbox{\tau_1} \tarrd{0}
\tbox{\tau_2}$ and $\tau_1 \tarrd{k} \tau_2$, in that order.

\item We switch to the unary reasoning (algorithmic analogues of rule
\textbf{switch} from \Cref{fig:synch-rel-typing-rules}) only when
necessary \ie\ when (a) eliminating expressions of the type
$\tch{\grt_1}{\grt_2}$, (b) checking related expressions at type
$\tch{\grt_1}{\grt_2}$, and (c) no other relational rules apply
(this happens when the expressions being related are structurally
dissimilar at the top-level).

% When subtyping $\tbox{\tau_1} \sqsubseteq \tbox{\tbox{\tau_2}}$, we first try to subtype
% $\tbox{\tau_1} \sqsubseteq \tbox{\tau_2}$ and then try
% by making use of $\tpushd{\tau_1} \sqsubseteq \tbox{\tau_1}$ and
% $\tbox{\tpushd{\tau_2}} \sqsubseteq \tbox{\tau_2}$ in combination
% with transitivity of algorithmic subtyping, we subtype
% $\tpushd{\tau_1} \subseteq \tpushd{\tau_2}$.
\end{enumerate}

These heuristics suffice for all the examples we have seen so far. We
list some of these examples later.

%% Although the heuristics we present here are specific to {\tname}, the
%% method of using heuristics to resolve nondeterminism in the context of
%% a practical typechecker is fairly general.

%% \paragraph{Bidirectional type system}
%% %% We implement the bidirectional typing rules of
%% %% Section~\ref{sec:alg-type-system} directly on {\tname}, rather than
%% %% {\tnamemin} (combined with the heuristics listed above).

%% Combined with the heuristics listed above, the four algorithmic typing
%% judgments from \Cref{sec:alg-type-system} can be implemented as
%% mutually recursive functions.\footnote{ Algorithmic subtyping
%%   judgments are implemented as recursive functions by case analysis on
%%   the types. } For instance, the two relational inference and checking
%% judgments are implemented with the following specifications. Here, $\kw{ctx} =
%% \Delta; \psi_a; \Phi_a; \Gamma$.
%% \[ \begin{array}{@{}l@{~~}l@{~}l@{~}l@{}l}
%%   \kw{inf_r}(\kw{ctx}, e_1, e_2) & = & \begin{cases} \tau, t, \Phi, \psi
%%     \quad\mbox{if } \kw{ctx} \infdiff{e_1}{e_2}{\tau}{\psi}{t}{\Phi} \\
%%     \mbox{error} \quad\;\;\;\; \mbox{otherwise} \end{cases} \\
%%   \kw{ch_r}(\kw{ctx}, e_1, e_2, \tau,t) & = &  \begin{cases} \Phi & \quad\;\mbox{if } \kw{ctx} \chdiff{e_1}{e_2}{\tau}{t}{\Phi} \\
%%     \mbox{error} & \quad\;\mbox{otherwise} \end{cases}
%%    \end{array}\]
%%  Function $\kw{inf_r}$ is defined by case analysis on the
%%  expressions $e_1$ and $e_2$ whereas $\kw{ch_r}$ is defined by case
%%  analysis on both the expressions $e_1,e_2$ and the type $\tau$. Both
%%  functions output a constraint \textcolor{red}{$\Phi$}, which, if
%%  satisfied, implies that a typing derivation exists in {\tname}.  Next,
%%  we explain how we solve this constraint.

\paragraph{Constraint solving}
In principle, we could pass the constraints \textcolor{red}{$\Phi$}
output by {\bitname}'s checking and inference judgments to an SMT
solver that understands the domain of integers (for sizes) and real
numbers (for costs). However, the constraint typically contains many
existentially quantified variables and current SMT solvers do not
eliminate such variables well. To solve this problem, we wrote a
simple pre-processing pass that finds candidate substitutions for
existentially quantified variables. For any such variable $n$, we look
for constraints of the form $n = I$ and $n \leq I$. In either case, we
consider $I$ a candidate substitution for $n$. In this way, we
generate a set of candidate substitutions for all existentially
quantified variables. For each such substitution, we try to check the
constraint's satisfiability using an SMT solver. (Our implementation
actually does this lazily: It generates a candidate substitution;
calls SMT; if that fails, generates the next substitution, and so on.)

%% To solve this problem, we wrote our own pre-processing pass that tries
%% to find substitutions for existentially quantified variables. For a
%% constraint of the form $\exists n. \Phi$, we look inside $\Phi$ to
%% find sub-constraints of the form $n = I$ or $n \leq I$. %% In either
%% %% case, $I$ is candidate substitution for $n$. We have to be careful
%% %% that $I$ does not contain variables that are quantified within $\Phi$
%% %% (else the scope of those variables is not respected).
%% Our
%% implementation uses lazy search with backtracking to try all candidate
%% substitutions: The implementation traverses the constraint top-down
%% from the root towards the leaves, finding candidate substitutions for
%% existential quantifiers it encounters. As soon as a substitution for
%% existential variables is found, it is applied and the resulting
%% existential-free formula is sent to an SMT solver (described next). If
%% the SMT solver proves the formula, we are done. If it fails or times
%% out, our search backtracks, looking for the next candidate
%% substitution. This process is potentially expensive, but it terminates
%% very quickly (in less than 1s) on all examples we have tried.

To check the satisfiability of existential-free constraints, we invoke
an SMT solver. Specifically, we use Why3~\cite{Filliatre:2013}, a
common front-end for many SMT solvers. Empirically, we have observed
that only one SMT solver, Alt-Ergo~\cite{bobot2013alt}, can handle our
constraints and, so, our implementation uses this solver behind
Why3. Why3 provides libraries of lemmas for exponentiation, logarithms
and iterated sums, which we use in some of the examples. For typing
programs that use divide-and-conquer over lists (e.g., merge sort), we
have to provide as an axiom one additional lemma that solves a general
recurrence related to costs. This lemma was proved in prior work
(Lemma 2 in the appendix of~\cite{CostIt15}).

\paragraph{Experimental evaluation}
We have used our implementation to typecheck a variety of examples,
including all the examples from the {\tname} paper. Some of the
examples, such as the relational analysis of merge sort
($\kw{msort}$), have rather complex paper proofs. However, in all
cases, the total typechecking time (including existential elimination
and SMT solving) is less than 1s, suggesting that the approach is
practical. Table~\ref{tab:benchmarks} shows the experimental results
over a subset of our example programs (our appendix lists all our
example programs, including their code and experimental results).  A
``-'' indicates a negligible value. Our experiments were performed on
a 3.20GHz 4-core Intel Core i5-6500 processor with 16 GB of RAM.

We briefly describe some of the example programs in
Table~\ref{tab:benchmarks} to highlight their diversity. The program
$\kw{map}$ is the list map function of Section~\ref{sec:relref}. The
program $\kw{comp}$ is a constant-time ($0$ relative cost) comparison
function that checks the equality of two passwords, represented as
lists of bits. The program $\kw{sam}$ (square-and-multiply) computes
the positive powers of a number, represented as a list of bits. The
experiment $\kw{find}$ compares two functions that find a given
element by scanning a list from head to tail and tail to head,
respectively. The program $\kw{2Dcount}$ counts the number of rows of
a matrix, represented as a list of lists in row-major form, that
satisfy a predicate $p$ and contain a key $x$. The program
$\kw{bsplit}$ splits a list into two nearly equal length lists. The
program $\kw{merge}$ merges two sorted lists and the program
$\kw{msort}$ is the standard merge sort function. In all cases except
$\kw{find}$, the goal of the analysis is to find an upper bound on the
relative cost of the function as its input changes. In all cases, the
cost bounds we check are asymptotically tight.

\begin{table}[t]
\centering
\begin{tabular} {| p{1.6cm} | p{1.0cm} | p{1.2cm} | p{1.5cm} |
p{1.5cm} |}
\hline
Benchmark        & Total time(s) & Type-checking & Existential elim.  & Constraint solving \\ \hline
$\kw{filter}$ & 0.13 & - & - & 0.13 \\ \hline
$\kw{append}$ & 0.14 & - & - & 0.13 \\ \hline
$\kw{rev}$ & 0.15 & - & - & 0.15 \\ \hline
$\kw{map}$ & 0.11 & - & - & 0.11 \\ \hline
$\kw{comp}$ & 0.08 & - & - & 0.07 \\ \hline
$\kw{sam}$ & 0.09 & 0.01 & - & 0.08 \\ \hline
$\kw{find}$ & 0.05 & - & - & 0.04 \\ \hline
$\kw{2Dcount}$ & 0.06 & - & - & 0.06 \\ \hline
$\kw{ssort}$ & 0.07 & - & - & 0.07 \\ \hline
$\kw{bsplit}$ & 0.17 & - & - & 0.17 \\ \hline
$\kw{flatten}$ & 0.06 & - & - & 0.05 \\ \hline
$\kw{appSum}$ & 0.10 & - & - & 0.09 \\ \hline
$\kw{merge}$ & 0.12 & - & - & 0.12 \\ \hline
$\kw{zip}$ & 0.13 & - & - & 0.13 \\ \hline
$\kw{msort}$ & 0.40 & 0.01 & 0.02 & 0.36 \\ \hline
$\kw{bfold}$ & 0.77 & - & 0.01 & 0.77 \\ \hline

\end{tabular}
\caption{{\bitname} runtime on benchmarks from the {\tname} paper
and the function $\kw{map}$. All times are in seconds.}
\label{tab:benchmarks}
\end{table}

\paragraph{Annotation effort}
In a traditional bidirectional type system, the programmer's
annotation effort is limited to providing the eliminated type at every
explicit $\beta$-redex and the type of every top-level function
definition in the program. In our setting, the burden is similar,
except that type annotations on functions also include a cost (on the
arrow). In all but one of the examples we have tried, annotations are
only necessary at each top-level function. One example has an explicit
$\beta$-redex (in the form of a let-binding) and needs one additional
annotation. Overall, this shows that the bidirectional approach
extends to the relational setting (even with refinements and effects),
without adding annotation burden.

% \paragraph{Example (map)}
% We describe how the map example from
% \Cref{sec:relcost-overview} type checks in {\bitname}.

% \medskip
% \begin{nstabbing}
%  $\eLam. \efix \kw{map}(f). \eLam. \eLam. \elam l. \ecase l $\=$\eof \enil \rightarrow \enil$ \\
% \>$ |~ h :: tl \rightarrow \econs(f \eapp h, \eapp \kw{map} \eapp f \eApp \eApp \eapp tl) $
% \end{nstabbing}

% \medskip
% Our aim is to type this function relative to itself at the following
% type:
% \begin{equation}
% \forall t. (\tbox{(\tau_1 \tarrd{t} \tau_2)}) \to \forall
%   n,\alpha. \tlist{n}{\alpha}{\tau_1} \tarrd{t \cdot \alpha}
%   \tlist{n}{\alpha}{\tau_2}\label{eq:map}
% \end{equation}
% We start in the checking mode with the above type. Using rule
% \textbf{alg-r-iLam-}$\downarrow$, we introduce the index variable $t$
% into the context. We continue in the checking mode using rule
% \textbf{alg-r-fix-}$\downarrow$. Next, we add the function $f$ and the
% input list $l$ to the typing context and the index variables $n$ and
% $\alpha$ to the sort context. For typechecking the pattern match on
% the list $l$, we use the rule \textbf{alg-r-caseL-}$\downarrow$.
% {\bitname} first infers that the type of $l$ is
% $\tlist{n}{\alpha}{\tau_1}$ using the rule
% \textbf{r-var-$\uparrow$}. The nil-branch is straightforwardly
% typechecked with $0$ cost. We focus here on cons-branch, considering
% the two cases where the heads of the two lists may differ or may not
% differ (third and fourth promises in rule
% \textbf{alg-r-caseL-}$\downarrow$). In both cases, we aim to check
% that $\econs(f \eapp h, \eapp \kw{map} \eapp f \eApp \eApp \eapp tl)$
% can be given type $\tlist{n}{\alpha}{\tau_2}$ using the heuristic (\ref{heur:cons})
% for cons-ed lists.

% In the first case where the heads of the two lists may not differ, we
% have $h:\tbox{\tau_1}$ and $tl:\tlist{i}{\alpha}{\tau_1}$, where $n =
% i+1$ for some freshly-generated meta variable $i$. Following heuristic
% (\ref{heur:cons}), we try to type ``$f \eapp h$'' in checking mode first with type
% $\tbox{\tau_2}$ and then with type $\tau_2$ (corresponding to the
% rules \textbf{alg-r-consNC-}$\downarrow$ and
% \textbf{alg-r-consC-}$\downarrow$). For the sake of brevity, we focus
% on the former, which succeeds and generates constraints that are
% satisfiable.\footnote{The latter case also succeeds here, but it
%   generates constraints that cannot be satisfied.} Since function
% applications (like ``$f \eapp h$'') are typed in inference mode, we
% switch from checking to inference mode using the rule
% \textbf{alg-r-}$\uparrow\downarrow$. Then, we proceed to type the
% function application ``$f \eapp h$'' in inference mode where we can
% infer that $f:\tbox{(\tau_1 \tarrd{t} \tau_2)}$. However, the function
% $f$ cannot be directly applied since it has a $\square$-ed type. At
% this point, using the heuristic (\ref{heur:box}), we subtype $\tbox{(\tau_1
%   \tarrd{t} \tau_2)}$ to $\tbox{\tau_1} \tarrd{0}
% \tbox{\tau_2}$. Then, we can type the argument $h$ in the checking
% mode with type $\tbox{\tau_1}$ successfully and conclude that ``$f
% \eapp h$'' can be given the type $\tbox{\tau_2}$ with relative cost
% $0$. Next, we aim to show that the tail of the cons, i.e.\ ``$
% \kw{map} \eapp f \eApp \eApp \eapp tl$'', can be typed in checking
% mode with type $\tlist{i'}{\alpha}{\tau_2}$ and cost $\alpha\cdot t$
% for some $i'$ such that $n=i'+1$. As in the head case, we use the rule
% \textbf{alg-r-}$\uparrow\downarrow$ to switch from checking to
% inference mode and generate the constraint $i'=i$ (which can be proved
% easily since $n=i'+1 = i+1$). The rest of the typing can be concluded
% by invoking the function and index term application rules multiple
% times.

% In the second case where the heads of the two lists may differ, we
% have $h:\tau_1$ and $tl:\tlist{i}{\beta}{\tau_1}$, where $n = i+1$ and
% $\alpha=\beta+1$ for some $i$ and $\beta$. Similar to above, we try to
% typecheck ``$f \eapp h$'' first at type $\tbox{\tau_2}$ and then at
% type $\tau_2$. This time, only the latter case succeeds and generates
% satisfiable constraints. In this case, like above, the function
% application ``$f \eapp h$'' is typed in inference mode, where we can
% infer that $f:\tbox{(\tau_1 \tarrd{t} \tau_2)}$. However, this time,
% we subtype $\tbox{(\tau_1 \tarrd{t} \tau_2)}$ to $\tau_1 \tarrd{t}
% \tau_2$ (again using heuristic (\ref{heur:box})) and type the argument $h$ in the
% checking mode at type $\tau_1$. The total cost of the application is
% $t$, not $0$. The recursive call to $\kw{map}$ follows a similar
% reasoning as in the previous case, but with cost $\beta\cdot
% t$. Hence, the total cost is $t + \beta \cdot t = (\beta + 1) \cdot t
% = \alpha \cdot t$, as required.

\paragraph{Heuristics illustrated with merge sort}
We explain how our implementation types one example---the standard
merge sort function--- \textit{relationally}. The goal of this
exercise is primarily to illustrate some of our heuristics.  The merge
sort function, $\kw{msort}$, splits a list into two nearly equal-sized
sublists using an auxiliary function we call $\kw{bsplit}$,
recursively sorts each sublist and then merges the two sorted sublists
using another function $\kw{merge}$. In their paper on {\tname},
\citet{Cicek:2017} show that the relative cost of two runs of
$\kw{msort}$ with two input lists of length $n$ that differ in at most
$\alpha$ positions is upper-bounded by $Q(n,\alpha) =
\ssum{i}{\szero}{H}{\smult{h(\sceil{\sdiv{2^i}{2}})}{\smin{\alpha}{2^{\sminus{H}{i}}}}}$,
where $H=\sceil{\slog{n}}$ and $h$ is a specific linear function. This
open-form expression lies in $O(n\cdot(1 +
\slog{\alpha}))$.\footnote{This relative cost $O(n\cdot(1 +
\slog{\alpha}))$ is asymptotically better than the relative cost
$O(n\cdot\slog{n})$ that can be established non-relationally. Also,
this relative cost bound is tight.}  Next, we explain at a
high-level how this relative cost is typechecked bidirectionally. We
show below the code of the top-level merge sort function $\kw{msort}$.
% \begin{tabbing}
% $\efix \kw{msort}(l). \caseof{l}$ \\
% $\ofnil{\enil}$\\
% $\ofcons{$\=$h_1}{tl_1}{} \caseof{tl_1}$\=$\ofnil{\econs(h_1,\enil)}$\\
% \>\>$\ofcons{\_}{\_}{$\=$\elet(z_1,z_2) = (\kw{bsplit} \eapp l) \ein  \kw{merge} \eapp (\kw{msort} \eapp z_1, \kw{msort} \eapp z_2)}$
% \end{tabbing}
\begin{tabbing}
$\efix \kw{msort}(\_). \eLam. \eLam. \elam l. \caseof{l}$
$\ofcons{$\=$h_1}{tl_1}{} \caseof{tl_1}$\=$\ofnil{\econs(h_1,\enil)}$\\
\>$\ofcons{\_}{\_}{$\=$\elet r = \kw{bsplit} \eapp () \eApp \eApp \eapp l \ein$\\
\>\> $ \eunpack r \eas r' \ein $$ \clet r' \eas (z_1,z_2) $\\
\> $\ein \kw{merge} \eapp () \eApp \eApp \eapp (\kw{msort} \eapp () \eApp \eApp \eapp z_1, \kw{msort} \eapp () \eApp \eApp \eapp z_2)}$
\end{tabbing}
We do not show the code of the helper functions $\kw{bsplit}$ and
$\kw{merge}$, but they have the following types (these types are also
checked with {\bitname}; we omit those details here):
\[
\begin{array}{l@{}l}
\kw{bsplit}:~&\tbox{(\trunit \to \tforallN{n,\alpha}
\tlist{n}{\alpha}{\tau} \to \\
&\texistsN{\beta} \tcprod{\beta \leq
\alpha}{(\tlist{\sceil{\sdiv{n}{2}}}{\beta}{\tau} \ttimes
\tlist{\sfloor{\sdiv{n}{2}}}{\sminus{\alpha}{\beta}}{\tau})})}
\end{array}
\]
\[
\begin{array}{l@{}l}
\kw{merge} : ~&
\tbox{(\tcho{(\tunit \to \tforallN{n,m} (\ulist{n}{\tint} \ttimes
\ulist{m}{\tint})  \\
\ulist{n+m}{\tint})})}
\end{array}
\]
Note the $\tbox{}$-es outside the types; their significance will be
clear soon. Our aim is to typecheck $\kw{msort}$ relative to itself at
the following type:
\[\tbox{(\trunit \to \tforallN{n,\alpha} \tlist{n}{\alpha}{(\tcho{\tint})}
\tarrd{Q(n,\alpha)} \tcho{(\ulist{n}{\tint})})}
\]
Here, $Q(n,\alpha)$ is the cost function defined above.  We focus on
the most interesting part where we call $\kw{merge}$ on the results of
the two recursive calls to $\kw{msort}$. At this point, we have $z_1:
\tlist{\sceil{\sdiv{n}{2}}}{\beta}{(\tcho{\tint})}$ and $z_2:
\tlist{\sfloor{\sdiv{n}{2}}}{\alpha-\beta}{(\tcho{\tint})}$ in the
context (from the type of $\kw{bsplit}$). Considering that only the
calls to $\kw{merge}$ and $\kw{msort}$ incur additional costs (all the
remaining operations occur synchronously on both sides and the
relative cost of $\kw{bsplit}$ is $0$ from its type), if we were to
naively establish the bound $Q(n,\alpha)$, we would have to show the
following inequality:
\begin{equation}
h(\sceil{\sdiv{n}{2}}) + Q(\sceil{\sdiv{n}{2}}, \beta) + Q(\sfloor{\sdiv{n}{2}}, \alpha
-\beta) \leq Q(n,\alpha)
\label{eq:msort:arith}
\end{equation}
where the cost $h(\sceil{\sdiv{n}{2}}) = h(n) -
h(min(\sceil{\sdiv{n}{2}},\sfloor{\sdiv{n}{2}}))$ comes from the
relative cost of $\kw{merge}$. However, as observed in the {\tname}
paper, this inequality holds only when $\alpha > 0$. When $\alpha=0$,
the right hand side is $0$ whereas the left hand side is
$h(\sceil{\sdiv{n}{2}})$. Nevertheless, when $\alpha=0$, the two input
lists do not differ at all, so the relative cost of $\kw{merge}$ can
be trivially established as $0$ using the \textbf{nochange} rule.

Consequently, the verification of $\kw{merge}$'s body differs based on
whether $\alpha=0$ or not. In our implementation, this case analysis
is provided for by heuristic (\ref{heur:split}). As soon as the list
$l$ is introduced into the context, we apply the algorithmic analogue
of the rule \textbf{rr-split}, introducing the two cases
$\ceq{\alpha}{0}$ and $\alpha >0$. For the case $\ceq{\alpha}{0}$, the
heuristic immediately invokes the rule
\textbf{alg-r-nochange-$\downarrow$}, which requires us to show that
all the free variables in the context have $\square$-ed types. Since
we know that the functions $\kw{merge}$, $\kw{bsplit}$ and
$\kw{msort}$ all have $\square$-ed types, what remains to be shown is
that $\tlist{n}{\alpha}{\tau_1} \sqsubseteq
\tbox{(\tlist{n}{\alpha}{\tau_1})}$. At this point,
heuristic~(\ref{heur:subtyping}) kicks in and uses the subtyping rules
\textbf{l2}, \textbf{l$\tbox{}$} (\Cref{fig:relref-ts}) and the
case-constraint $\ceq{\alpha}{0}$ to establish this property.  For the
other case ($\alpha > 0$), we type the function body following its
syntax. This eventually generates the satisfiable constraint
(\ref{eq:msort:arith}) that is discharged by the constraint
solver. The verification also uses heuristic~(\ref{heur:box}) to
typecheck the applications of $\kw{bsplit}$ and $\kw{merge}$ despite
their $\tbox{}$-ed types.

%% \paragraph{Other examples} Our appendix lists additional verified examples:
%% some standard list functions (e.g.\ append, reverse, flatten and zip),
%% selection sort, balanced-fold (another divide and conquer program) and
%% an instance of approximate computation.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{Related Work}
\label{sec:related}

There is a lot of literature on implementing various combinations of
refinement types, effect systems, modal types, and subtyping. A
distinctive feature of our work is that it combines all these
aspects in a relational setting.

%\paragraph{Bidirectional typechecking}
The idea of bidirectional type
systems appeared in literature early on. However, the idea was
popularized only more recently by Pierce and
Turner~\cite{Pierce:2000}. The technique has shown great
applicability---it has been used for dependent
types~\cite{Coquand:96}, indexed refinement
types~\cite{xi99:dependent,XiThesis}, intersection and union
types~\cite{Davies:2000,Dunfield:2003}, higher-rank
contextual modal types~\cite{Pientka:2008}, algebraic effect
handlers~\cite{Lindley:2017} and gradual typing~\cite{Toro:2015}. Our
approach is inspired by many of these papers, in particular
DML~\cite{xi99:dependent,XiThesis}, but departs in the technical
design of the algorithmic type system due to new challenges offered by
relational and modal types, and costs. In particular, in %almost
all these works % on bidirectional typechecking,
the reasoning principle is \textit{unary}, i.e.\ a single program is
checked (inferred) in isolation. Moreover, none of these works
consider effects explicitly, i.e.\ as a type and effect system. One
exception is the bidirectional effect system by ~\cite{Toro:2015},
which uses bidirectional typechecking for gradual unary
effects. However, their end goal is different since they infer minimal
effects at compile time and then check dynamic effects at runtime.

% DML~\cite{xi99:dependent,XiThesis} pioneered the practicality of
% refinement types in program verification and design. Our approach and
% the type checking of DML shares several similarities: both use
% bidirectionality, both generate arithmetic constraints, etc. However,
% DML lacks comonadic types, costs, and relational types. The challenges
% we faced in our work come mostly from these components.

%\paragraph{Dependent types}
Numerous other systems use lightweight
dependent types for program verification including, for instance,
F$^*$~\cite{SwamyCFSBY11,SwamyHKRDFBFSKZ16} and
LiquidHaskell~\cite{VazouSJ14}. However, these developments also do
not consider comonadic types and costs.
The DML approach has also been used in combination
with linear types for asymptotic complexity analysis
\cite{lago12,Dallago:13}
and for reasoning about differential
privacy~\cite{gaboardi13:dep, AmorimGAH14}. Besides lightweight dependent types, these
papers also consider the comonadic modality of linear logic. This
modality's structural properties are quite different from those of the
$\tbox{}$ we consider here.
Another way to extend dependent types with cost information is to index a
monad with the execution cost. Gundry considers this approach in a unary setting for a
subset of Haskell with support for bidirectional
None of these papers consider
relational typing.

%\paragraph{Inference systems for resource analysis}
% Resource-aware
% ML~\cite{HoffmannAH12} performs fully automatic type-based analysis of
% worst-case (unary) costs. Their technique is based on the amortized
% cost analysis based on potentials, not bidirectional techniques and
% does not consider relational costs (and modal types).  One limitation
% of the automation technique, but not of the broader technique of
% amortized cost analysis, is that it extends only to polynomial
% bounds. In our examples, we have often seen non-polynomial bounds
% (e.g., merge sort from Section~\ref{sec:implementation}). Nonetheless,
% extending resource-aware ML to relative costs might be an interesting
% research direction.

%\paragraph{Relational verification systems}

Some other type systems
establish relational properties of programs. For
instance,~\citet{BFGSSZ14} consider a relational variant of a fragment
of F$^*$ for the verification of cryptographic implementations, and
similarly \citet{BartheGAHRS15} consider a relational refinement type
system for differential privacy. However, some of the key technical
challenges of our system, including those that arise from the
interaction between unary and relational typing, as well as costs, do
not show up in these settings. Moreover, these systems use
verification condition generation, not bidirectionality.
In the realm of incremental computing, some
work~\cite{CostIt15,DuCostIt16} has proposed declarative type systems
for reasoning about update costs of incremental programs. These
systems share similarities with the systems we considered here and we
believe that the ideas developed in this paper can be applied to
obtain algorithmic versions of these type systems as well.

%\paragraph{Elimination of subtyping}
Prior work has also studied
methods of eliminating subtyping as a way of simplifying type
checking, e.g.~\cite{Breazu-Tannen:1991,Crary:2000}.  While our
approach is similar in motivation, our technical challenges are quite
different. Main difficulties in simplifying subtyping in our work
arise from the interaction of the modalities $\tbox{}$ and $U$ with
other connectives.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{Conclusion}
\label{sec:conclusion}
% We have presented the design and implementation of {\bitname}, an
% algorithmic bidirectional type system for relational cost analysis. We
% have thus shown how to implement a concrete software tool useful for
% proving the relative cost of two programs. In designing {\bitname}, we
% have to hande {\tname}'s non-syntax-directed rules and its
% non-algorithmic relational subtyping. Our implementation handles these
% using sound heuristics that suffice for all our examples. In our
% theory, we establish that bidirectional typechecking is complete
% modulo the completeness of our heuristics. To formalize this, we
% present an embedding from {\tname} to {\tnamemin}, a language with
% only syntax-directed rules and very simple subtyping. While our
% technical development is specific to relational cost analysis,
This paper presented a theoretical study and a concrete implementation
of bidirectional type checking in a setting that combines relational
refinements, comonadic types and relational effects. This rich setting
poses unique challenges: The typing rules are not syntax-directed due
to relational refinements; switching from relational to unary
reasoning adds to the ambiguity; subtyping for (relational) comonads
poses additional problems, as do the relational effects. We resolve
these challenges through a process of elaboration and
subtyping-elimination in the theory and using example-guided
heuristics in the implementation. We validate experimentally that this
approach is practical---it works for many different kinds of programs,
has little annotation burden and typechecking is quick. Although we
have focused here on a specific line of type systems with the features
mentioned above, we believe that our work will help future designers
of other relational type (and effect) systems as well.

%% . We presented the
%% implementation of the system combining all these components and
%% discussed heuristics to make it effective. % We believe that our
%% design will help future designer of
%% % relational type systems .
%% % general and could be used for other systems for relational reasoning
%% % as well.

%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\begin{thebibliography}{45}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[\protect\citeauthoryear{Abadi, Cardelli, and Curien}{Abadi
\bibfield{author}{\bibinfo{person}{Mart{\'{\i}}n Abadi}, \bibinfo{person}{Luca
Cardelli}, {and} \bibinfo{person}{Pierre{-}Louis Curien}.}
\bibinfo{year}{1993}\natexlab{}.
\newblock \showarticletitle{Formal Parametric Polymorphism}. In
\bibinfo{booktitle}{\emph{Conference Record of the Twentieth Annual {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages,
Charleston, South Carolina, USA, January 1993}}. \bibinfo{pages}{157--170}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/158511.158622}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Abel, Vezzosi, and Winterhalter}{Abel
\bibfield{author}{\bibinfo{person}{Andreas Abel}, \bibinfo{person}{Andrea
Vezzosi}, {and} \bibinfo{person}{Th{\'{e}}o Winterhalter}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Normalization by evaluation for sized dependent
\newblock \bibinfo{journal}{\emph{{PACMPL}}} \bibinfo{volume}{1},
\bibinfo{number}{{ICFP}} (\bibinfo{year}{2017}),
\bibinfo{pages}{33:1--33:30}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3110277}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Aguirre, Barthe, Birkedal, Bizjak, Gaboardi,
and Garg}{Aguirre et~al\mbox{.}}{2018}]%
\bibfield{author}{\bibinfo{person}{Alejandro Aguirre}, \bibinfo{person}{Gilles
Barthe}, \bibinfo{person}{Lars Birkedal}, \bibinfo{person}{Ales Bizjak},
\bibinfo{person}{Marco Gaboardi}, {and} \bibinfo{person}{Deepak Garg}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Relational Reasoning for Markov Chains in a
Probabilistic Guarded Lambda Calculus}. In
\bibinfo{booktitle}{\emph{Programming Languages and Systems - 27th European
Symposium on Programming, {ESOP} 2018, Held as Part of the European Joint
Conferences on Theory and Practice of Software, {ETAPS} 2018, Thessaloniki,
Greece, April 14-20, 2018, Proceedings}}. \bibinfo{pages}{214--241}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-89884-1\_8}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Aguirre, Barthe, Gaboardi, Garg, and
Strub}{Aguirre et~al\mbox{.}}{2017}]%
\bibfield{author}{\bibinfo{person}{Alejandro Aguirre}, \bibinfo{person}{Gilles
Barthe}, \bibinfo{person}{Marco Gaboardi}, \bibinfo{person}{Deepak Garg},
{and} \bibinfo{person}{Pierre{-}Yves Strub}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{A relational logic for higher-order programs}.
\newblock \bibinfo{journal}{\emph{{PACMPL}}} \bibinfo{volume}{1},
\bibinfo{number}{{ICFP}} (\bibinfo{year}{2017}),
\bibinfo{pages}{21:1--21:29}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3110265}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Barthe, Fournet, Gr{\'{e}}goire, Strub, Swamy,
and B{\'{e}}guelin}{Barthe et~al\mbox{.}}{2014a}]%
\bibfield{author}{\bibinfo{person}{Gilles Barthe},
\bibinfo{person}{C{\'{e}}dric Fournet}, \bibinfo{person}{Benjamin
Gr{\'{e}}goire}, \bibinfo{person}{Pierre{-}Yves Strub},
\bibinfo{person}{Nikhil Swamy}, {and} \bibinfo{person}{Santiago~Zanella
B{\'{e}}guelin}.} \bibinfo{year}{2014}\natexlab{a}.
\newblock \showarticletitle{Probabilistic relational verification for
cryptographic implementations}. In \bibinfo{booktitle}{\emph{The 41st Annual
{ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages,
{POPL} '14, San Diego, CA, USA, January 20-21, 2014}}.
\bibinfo{pages}{193--206}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2535838.2535847}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Barthe, Fournet, Gr{\'{e}}goire, Strub, Swamy,
and B{\'{e}}guelin}{Barthe et~al\mbox{.}}{2014b}]%
\bibfield{author}{\bibinfo{person}{Gilles Barthe},
\bibinfo{person}{C{\'{e}}dric Fournet}, \bibinfo{person}{Benjamin
Gr{\'{e}}goire}, \bibinfo{person}{Pierre{-}Yves Strub},
\bibinfo{person}{Nikhil Swamy}, {and} \bibinfo{person}{Santiago~Zanella
B{\'{e}}guelin}.} \bibinfo{year}{2014}\natexlab{b}.
\newblock \showarticletitle{Probabilistic relational verification for
cryptographic implementations}. In \bibinfo{booktitle}{\emph{Proceedings of
the 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming
Languages, {POPL}'14}}, \bibfield{editor}{\bibinfo{person}{Suresh
Jagannathan} {and} \bibinfo{person}{Peter Sewell}} (Eds.).
\bibinfo{pages}{193--206}.
\newblock

\bibitem[\protect\citeauthoryear{Barthe, Gaboardi, Arias, Hsu, Roth, and
Strub}{Barthe et~al\mbox{.}}{2015a}]%
\bibfield{author}{\bibinfo{person}{Gilles Barthe}, \bibinfo{person}{Marco
Gaboardi}, \bibinfo{person}{Emilio Jes{\'{u}}s~Gallego Arias},
\bibinfo{person}{Justin Hsu}, \bibinfo{person}{Aaron Roth}, {and}
\bibinfo{person}{Pierre{-}Yves Strub}.} \bibinfo{year}{2015}\natexlab{a}.
\newblock \showarticletitle{Higher-Order Approximate Relational Refinement
Types for Mechanism Design and Differential Privacy}. In
\bibinfo{booktitle}{\emph{Proceedings of the 42nd Annual {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL}
2015, Mumbai, India, January 15-17, 2015}}. \bibinfo{pages}{55--68}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2676726.2677000}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Barthe, Gaboardi, Gallego~Arias, Hsu, Roth,
and Strub}{Barthe et~al\mbox{.}}{2015b}]%
\bibfield{author}{\bibinfo{person}{Gilles Barthe}, \bibinfo{person}{Marco
Gaboardi}, \bibinfo{person}{Emilio~Jes{\'u}s Gallego~Arias},
\bibinfo{person}{Justin Hsu}, \bibinfo{person}{Aaron Roth}, {and}
\bibinfo{person}{Pierre-Yves Strub}.} \bibinfo{year}{2015}\natexlab{b}.
\newblock \showarticletitle{Higher-order approximate relational refinement
types for mechanism design and differential privacy}. In
\bibinfo{booktitle}{\emph{Proceedings of the 42nd Annual {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL}
2015, Mumbai, India, January 15-17, 2015}},
\bibfield{editor}{\bibinfo{person}{Sriram~K. Rajamani} {and}
\bibinfo{person}{David Walker}} (Eds.). \bibinfo{pages}{55--68}.
\newblock

\bibitem[\protect\citeauthoryear{Bierman, Meijer, and Torgersen}{Bierman
\bibfield{author}{\bibinfo{person}{Gavin~M. Bierman}, \bibinfo{person}{Erik
Meijer}, {and} \bibinfo{person}{Mads Torgersen}.}
\bibinfo{year}{2007}\natexlab{}.
\newblock \showarticletitle{Lost in translation: formalizing proposed
extensions to c{\#}}. In \bibinfo{booktitle}{\emph{Proceedings of the 22nd
Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems,
Languages, and Applications, {OOPSLA} 2007, October 21-25, 2007, Montreal,
Quebec, Canada}}. \bibinfo{pages}{479--498}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/1297027.1297063}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Bobot, Conchon, Contejean, Iguernelala,
Lescuyer, and Mebsout}{Bobot et~al\mbox{.}}{2013}]%
\bibfield{author}{\bibinfo{person}{Fran{\c{c}}ois Bobot},
\bibinfo{person}{Sylvain Conchon}, \bibinfo{person}{E Contejean},
\bibinfo{person}{Mohamed Iguernelala}, \bibinfo{person}{St{\'e}phane
Lescuyer}, {and} \bibinfo{person}{Alain Mebsout}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \bibinfo{title}{The Alt-Ergo automated theorem prover, 2008}.
\newblock
\newblock

\bibitem[\protect\citeauthoryear{Bracha, Odersky, Stoutamire, and
Wadler}{Bracha et~al\mbox{.}}{1998}]%
\bibfield{author}{\bibinfo{person}{Gilad Bracha}, \bibinfo{person}{Martin
Odersky}, \bibinfo{person}{David Stoutamire}, {and} \bibinfo{person}{Philip
Wadler}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Making the Future Safe for the Past: Adding
Genericity to the Java Programming Language}. In
\bibinfo{booktitle}{\emph{Proceedings of the 1998 {ACM} {SIGPLAN} Conference
on Object-Oriented Programming Systems, Languages {\&} Applications {(OOPSLA}
'98), Vancouver, British Columbia, Canada, October 18-22, 1998.}}
\bibinfo{pages}{183--200}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/286936.286957}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Breazu-Tannen, Coquand, Gunter, and
Scedrov}{Breazu-Tannen et~al\mbox{.}}{1991}]%
\bibfield{author}{\bibinfo{person}{Val Breazu-Tannen}, \bibinfo{person}{Thierry
Coquand}, \bibinfo{person}{Carl~A. Gunter}, {and} \bibinfo{person}{Andre
Scedrov}.} \bibinfo{year}{1991}\natexlab{}.
\newblock \showarticletitle{Inheritance As Implicit Coercion}.
\newblock \bibinfo{journal}{\emph{Inf. Comput.}} \bibinfo{volume}{93},
\bibinfo{number}{1} (\bibinfo{date}{July} \bibinfo{year}{1991}),
\bibinfo{pages}{172--221}.
\newblock

\bibitem[\protect\citeauthoryear{Brunel, Gaboardi, Mazza, and Zdancewic}{Brunel
\bibfield{author}{\bibinfo{person}{Alo{\"{\i}}s Brunel}, \bibinfo{person}{Marco
Gaboardi}, \bibinfo{person}{Damiano Mazza}, {and} \bibinfo{person}{Steve
Zdancewic}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{A Core Quantitative Coeffect Calculus}. In
\bibinfo{booktitle}{\emph{Programming Languages and Systems - 23rd European
Symposium on Programming, {ESOP} 2014, Held as Part of the European Joint
Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble,
France, April 5-13, 2014, Proceedings}}. \bibinfo{pages}{351--370}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-54833-8\_19}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{\c{C}i\c{c}ek, Barthe, Gaboardi, Garg, and
Hoffmann}{\c{C}i\c{c}ek et~al\mbox{.}}{2017}]%
\bibfield{author}{\bibinfo{person}{Ezgi \c{C}i\c{c}ek}, \bibinfo{person}{Gilles
Barthe}, \bibinfo{person}{Marco Gaboardi}, \bibinfo{person}{Deepak Garg},
{and} \bibinfo{person}{Jan Hoffmann}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Relational Cost Analysis}. In
\bibinfo{booktitle}{\emph{Proceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages}} \emph{(\bibinfo{series}{POPL 2017})}.
\bibinfo{publisher}{ACM}, \bibinfo{pages}{316--329}.
\newblock

\bibitem[\protect\citeauthoryear{{\c{C}}i{\c{c}}ek, Garg, and
Acar}{{\c{C}}i{\c{c}}ek et~al\mbox{.}}{2015}]%
\bibfield{author}{\bibinfo{person}{Ezgi {\c{C}}i{\c{c}}ek},
\bibinfo{person}{Deepak Garg}, {and} \bibinfo{person}{Umut~A. Acar}.}
\bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Refinement Types for Incremental Computational
Complexity}. In \bibinfo{booktitle}{\emph{Programming Languages and Systems -
24th European Symposium on Programming, {ESOP} 2015, London, UK, April 11-18,
2015. Proceedings}}. \bibinfo{pages}{406--431}.
\newblock

\bibitem[\protect\citeauthoryear{{\c{C}}i{\c{c}}ek, Paraskevopoulou, and
Garg}{{\c{C}}i{\c{c}}ek et~al\mbox{.}}{2016}]%
\bibfield{author}{\bibinfo{person}{Ezgi {\c{C}}i{\c{c}}ek},
\bibinfo{person}{Zoe Paraskevopoulou}, {and} \bibinfo{person}{Deepak Garg}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{A Type Theory for Incremental Computational
Complexity With Control Flow Changes}. In
\bibinfo{booktitle}{\emph{Proceedings of the 21st International Conference on
Functional Programming}} \emph{(\bibinfo{series}{ICFP '16})}.
\newblock

\bibitem[\protect\citeauthoryear{Coquand}{Coquand}{1996}]%
\bibfield{author}{\bibinfo{person}{Thierry Coquand}.}
\bibinfo{year}{1996}\natexlab{}.
\newblock \showarticletitle{An algorithm for type-checking dependent types}.
\newblock \bibinfo{journal}{\emph{Science of Computer Programming}}
\bibinfo{volume}{26}, \bibinfo{number}{1} (\bibinfo{year}{1996}),
\bibinfo{pages}{167 -- 177}.
\newblock

\bibitem[\protect\citeauthoryear{Crary}{Crary}{2000}]%
\bibfield{author}{\bibinfo{person}{Karl Crary}.}
\bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{Typed Compilation of Inclusive Subtyping}. In
\bibinfo{booktitle}{\emph{Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming}} \emph{(\bibinfo{series}{ICFP '00})}.
\bibinfo{publisher}{ACM}, \bibinfo{pages}{68--81}.
\newblock
\showISBNx{1-58113-202-6}

\bibitem[\protect\citeauthoryear{Dal~Lago and Gaboardi}{Dal~Lago and
\bibfield{author}{\bibinfo{person}{Ugo Dal~Lago} {and} \bibinfo{person}{Marco
Gaboardi}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Linear Dependent Types and Relative Completeness}.
In \bibinfo{booktitle}{\emph{Proceedings of the 2011 IEEE 26th Annual
Symposium on Logic in Computer Science}} \emph{(\bibinfo{series}{LICS '11})}.
\bibinfo{pages}{133--142}.
\newblock

\bibitem[\protect\citeauthoryear{Dal~Lago and Petit}{Dal~Lago and
\bibfield{author}{\bibinfo{person}{Ugo Dal~Lago} {and} \bibinfo{person}{Barbara
Petit}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{The Geometry of Types}. In
\bibinfo{booktitle}{\emph{Proceedings of the 40th Annual Symposium on
Principles of Programming Languages}} \emph{(\bibinfo{series}{POPL '13})}.
\bibinfo{pages}{167--178}.
\newblock

\bibitem[\protect\citeauthoryear{Davies and Pfenning}{Davies and
\bibfield{author}{\bibinfo{person}{Rowan Davies} {and} \bibinfo{person}{Frank
Pfenning}.} \bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{Intersection Types and Computational Effects}. In
\bibinfo{booktitle}{\emph{Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming}} \emph{(\bibinfo{series}{ICFP '00})}.
\bibinfo{pages}{198--208}.
\newblock

\bibitem[\protect\citeauthoryear{de~Amorim, Gaboardi, Arias, and Hsu}{de~Amorim
\bibfield{author}{\bibinfo{person}{Arthur~Azevedo de Amorim},
\bibinfo{person}{Marco Gaboardi}, \bibinfo{person}{Emilio Jes{\'{u}}s~Gallego
Arias}, {and} \bibinfo{person}{Justin Hsu}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Really Natural Linear Indexed Type Checking}. In
\bibinfo{booktitle}{\emph{Proceedings of the 26th 2014 International
Symposium on Implementation and Application of Functional Languages, {IFL}
'14, Boston, MA, USA, October 1-3, 2014}}. \bibinfo{pages}{5:1--5:12}.
\newblock

\bibitem[\protect\citeauthoryear{Dunfield and Krishnaswami}{Dunfield and
\bibfield{author}{\bibinfo{person}{Joshua Dunfield} {and}
\bibinfo{person}{Neelakantan~R. Krishnaswami}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Complete and Easy Bidirectional Typechecking for
Higher-Rank Polymorphism}. In \bibinfo{booktitle}{\emph{International
Conference on Functional Programming}}.
\newblock
\newblock
\shownote{\url{arXiv:1306.6032 [cs.PL]}.}

\bibitem[\protect\citeauthoryear{Dunfield and Krishnaswami}{Dunfield and
\bibfield{author}{\bibinfo{person}{Joshua Dunfield} {and}
\bibinfo{person}{Neelakantan~R. Krishnaswami}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Sound and Complete Bidirectional Typechecking for
Higher-Rank Polymorphism with Existentials and Indexed Types}.
\newblock \bibinfo{journal}{\emph{CoRR}}  \bibinfo{volume}{abs/1601.05106}
\newblock
\urldef\tempurl%
\url{http://arxiv.org/abs/1601.05106}
\showURL{%
\tempurl}

\bibitem[\protect\citeauthoryear{Dunfield and Pfenning}{Dunfield and
\bibfield{author}{\bibinfo{person}{Joshua Dunfield} {and}
\bibinfo{person}{Frank Pfenning}.} \bibinfo{year}{2003}\natexlab{}.
\newblock \showarticletitle{Type Assignment for Intersections and Unions in
Call-by-value Languages}. In \bibinfo{booktitle}{\emph{Proceedings of the 6th
International Conference on Foundations of Software Science and Computation
Structures and Joint European Conference on Theory and Practice of Software}}
\emph{(\bibinfo{series}{FOSSACS'03/ETAPS'03})}.
\bibinfo{publisher}{Springer-Verlag}, \bibinfo{pages}{250--266}.
\newblock

\bibitem[\protect\citeauthoryear{Felleisen}{Felleisen}{1991}]%
\bibfield{author}{\bibinfo{person}{Matthias Felleisen}.}
\bibinfo{year}{1991}\natexlab{}.
\newblock \showarticletitle{On the Expressive Power of Programming Languages}.
\newblock \bibinfo{journal}{\emph{Science of Computer Programming}}
\bibinfo{volume}{17}, \bibinfo{number}{1-3} (\bibinfo{year}{1991}),
\bibinfo{pages}{35--75}.
\newblock

\bibitem[\protect\citeauthoryear{Filli\^{a}tre and Paskevich}{Filli\^{a}tre and
\bibfield{author}{\bibinfo{person}{Jean-Christophe Filli\^{a}tre} {and}
\bibinfo{person}{Andrei Paskevich}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Why3: Where Programs Meet Provers}. In
\bibinfo{booktitle}{\emph{Proceedings of the 22Nd European Conference on
Programming Languages and Systems}} \emph{(\bibinfo{series}{ESOP'13})}.
\bibinfo{publisher}{Springer-Verlag}, \bibinfo{pages}{125--128}.
\newblock

\bibitem[\protect\citeauthoryear{Gaboardi, Haeberlen, Hsu, Narayan, and
Pierce}{Gaboardi et~al\mbox{.}}{2013}]%
\bibfield{author}{\bibinfo{person}{Marco Gaboardi}, \bibinfo{person}{Andreas
Haeberlen}, \bibinfo{person}{Justin Hsu}, \bibinfo{person}{Arjun Narayan},
{and} \bibinfo{person}{Benjamin~C. Pierce}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Linear Dependent Types for Differential Privacy}.
In \bibinfo{booktitle}{\emph{Proceedings of the 40th Annual Symposium on
Principles of Programming Languages}} \emph{(\bibinfo{series}{POPL '13})}.
\bibinfo{pages}{357--370}.
\newblock

\bibitem[\protect\citeauthoryear{Gundry}{Gundry}{2013}]%
\bibfield{author}{\bibinfo{person}{Adam Gundry}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \emph{\bibinfo{title}{Type Inference, Haskell and Dependent Types}}.
\newblock \bibinfo{thesistype}{Ph.D. Dissertation}. \bibinfo{school}{University
of Strathclyde}.
\newblock
\newblock
\shownote{available as

\bibitem[\protect\citeauthoryear{Lindley, McBride, and McLaughlin}{Lindley
\bibfield{author}{\bibinfo{person}{Sam Lindley}, \bibinfo{person}{Conor
McBride}, {and} \bibinfo{person}{Craig McLaughlin}.}
\bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Do Be Do Be Do}. In
\bibinfo{booktitle}{\emph{Proceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages}} \emph{(\bibinfo{series}{POPL 2017})}.
\bibinfo{publisher}{ACM}, \bibinfo{address}{New York, NY, USA},
\bibinfo{pages}{500--514}.
\newblock

\bibitem[\protect\citeauthoryear{Lucassen and Gifford}{Lucassen and
\bibfield{author}{\bibinfo{person}{J.~M. Lucassen} {and} \bibinfo{person}{D.~K.
Gifford}.} \bibinfo{year}{1988}\natexlab{}.
\newblock \showarticletitle{Polymorphic Effect Systems}. In
\bibinfo{booktitle}{\emph{Proceedings of the 15th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages}}
\emph{(\bibinfo{series}{POPL '88})}. \bibinfo{publisher}{ACM},
\bibinfo{pages}{47--57}.
\newblock

\bibitem[\protect\citeauthoryear{Nielson and Nielson}{Nielson and
\bibfield{author}{\bibinfo{person}{Flemming Nielson} {and}
\bibinfo{person}{HanneRiis Nielson}.} \bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Type and Effect Systems}.
\newblock In \bibinfo{booktitle}{\emph{Correct System Design}}.
\bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{1710}. \bibinfo{publisher}{Springer-Verlag},
\bibinfo{pages}{114--136}.
\newblock

\bibitem[\protect\citeauthoryear{Odersky, Zenger, and Zenger}{Odersky
\bibfield{author}{\bibinfo{person}{Martin Odersky}, \bibinfo{person}{Matthias
Zenger}, {and} \bibinfo{person}{Christoph Zenger}.}
\bibinfo{year}{2001}\natexlab{}.
\newblock \showarticletitle{Colored Local Type Inference}. In
\bibinfo{booktitle}{\emph{Proc. ACM Symposium on Principles of Programming
Languages}}. \bibinfo{pages}{41--53}.
\newblock

\bibitem[\protect\citeauthoryear{Petricek, Orchard, and Mycroft}{Petricek
\bibfield{author}{\bibinfo{person}{Tomas Petricek}, \bibinfo{person}{Dominic~A.
Orchard}, {and} \bibinfo{person}{Alan Mycroft}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Coeffects: Unified Static Analysis of
Context-Dependence}. In \bibinfo{booktitle}{\emph{Automata, Languages, and
Programming - 40th International Colloquium, {ICALP} 2013, Riga, Latvia, July
8-12, 2013, Proceedings, Part {II}}}. \bibinfo{pages}{385--397}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-39212-2\_35}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Peyton~Jones, Vytiniotis, Weirich, and
Shields}{Peyton~Jones et~al\mbox{.}}{2007}]%
\bibfield{author}{\bibinfo{person}{Simon Peyton~Jones},
\bibinfo{person}{Dimitrios Vytiniotis}, \bibinfo{person}{Stephanie Weirich},
{and} \bibinfo{person}{Mark Shields}.} \bibinfo{year}{2007}\natexlab{}.
\newblock \showarticletitle{Practical Type Inference for Arbitrary-rank Types}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{17},
\bibinfo{number}{1} (\bibinfo{date}{Jan.} \bibinfo{year}{2007}),
\bibinfo{pages}{1--82}.
\newblock

\bibitem[\protect\citeauthoryear{{Peyton Jones}, Vytiniotis, Weirich, and
Shields}{{Peyton Jones} et~al\mbox{.}}{2007}]%
\bibfield{author}{\bibinfo{person}{Simon~L. {Peyton Jones}},
\bibinfo{person}{Dimitrios Vytiniotis}, \bibinfo{person}{Stephanie Weirich},
{and} \bibinfo{person}{Mark Shields}.} \bibinfo{year}{2007}\natexlab{}.
\newblock \showarticletitle{Practical type inference for arbitrary-rank types}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{17},
\bibinfo{number}{1} (\bibinfo{year}{2007}), \bibinfo{pages}{1--82}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1017/S0956796806006034}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Pientka}{Pientka}{2008}]%
\bibfield{author}{\bibinfo{person}{Brigitte Pientka}.}
\bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{A Type-theoretic Foundation for Programming with
Higher-order Abstract Syntax and First-class Substitutions}. In
\bibinfo{booktitle}{\emph{Proceedings of the 35th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages}}
\emph{(\bibinfo{series}{POPL '08})}. \bibinfo{pages}{371--382}.
\newblock

\bibitem[\protect\citeauthoryear{Pierce and Turner}{Pierce and Turner}{2000}]%
\bibfield{author}{\bibinfo{person}{Benjamin~C. Pierce} {and}
\bibinfo{person}{David~N. Turner}.} \bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{Local Type Inference}.
\newblock \bibinfo{journal}{\emph{ACM Trans. Program. Lang. Syst.}}
\bibinfo{volume}{22}, \bibinfo{number}{1} (\bibinfo{date}{Jan.}
\bibinfo{year}{2000}), \bibinfo{pages}{1--44}.
\newblock
\showISSN{0164-0925}

\bibitem[\protect\citeauthoryear{Pottier and Simonet}{Pottier and
\bibfield{author}{\bibinfo{person}{Fran\c{c}ois Pottier} {and}
\bibinfo{person}{Vincent Simonet}.} \bibinfo{year}{2003}\natexlab{}.
\newblock \showarticletitle{Information Flow Inference for {ML}}.
\newblock \bibinfo{journal}{\emph{ACM Trans. Prog. Lang. Sys.}}
\bibinfo{volume}{25}, \bibinfo{number}{1} (\bibinfo{date}{Jan.}
\bibinfo{year}{2003}), \bibinfo{pages}{117--158}.
\newblock

\bibitem[\protect\citeauthoryear{Swamy, Chen, Fournet, Strub, Bhargavan, and
Yang}{Swamy et~al\mbox{.}}{2011}]%
\bibfield{author}{\bibinfo{person}{Nikhil Swamy}, \bibinfo{person}{Juan Chen},
\bibinfo{person}{C{\'{e}}dric Fournet}, \bibinfo{person}{Pierre{-}Yves
Strub}, \bibinfo{person}{Karthikeyan Bhargavan}, {and} \bibinfo{person}{Jean
Yang}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Secure distributed programming with value-dependent
types}. In \bibinfo{booktitle}{\emph{Proceeding of the 16th {ACM} {SIGPLAN}
international conference on Functional Programming, {ICFP} 2011, Tokyo,
Japan, September 19-21, 2011}}. \bibinfo{pages}{266--278}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2034773.2034811}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Swamy, Hritcu, Keller, Rastogi,
Delignat{-}Lavaud, Forest, Bhargavan, Fournet, Strub, Kohlweiss,
Zinzindohoue, and B{\'{e}}guelin}{Swamy et~al\mbox{.}}{2016}]%
\bibfield{author}{\bibinfo{person}{Nikhil Swamy}, \bibinfo{person}{Catalin
Hritcu}, \bibinfo{person}{Chantal Keller}, \bibinfo{person}{Aseem Rastogi},
\bibinfo{person}{Antoine Delignat{-}Lavaud}, \bibinfo{person}{Simon Forest},
\bibinfo{person}{Karthikeyan Bhargavan}, \bibinfo{person}{C{\'{e}}dric
Fournet}, \bibinfo{person}{Pierre{-}Yves Strub}, \bibinfo{person}{Markulf
Kohlweiss}, \bibinfo{person}{Jean~Karim Zinzindohoue}, {and}
\bibinfo{person}{Santiago~Zanella B{\'{e}}guelin}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Dependent types and multi-monadic effects in
{F}$^*$}. In \bibinfo{booktitle}{\emph{Proceedings of the 43rd Annual {ACM}
{SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL}
2016, St. Petersburg, FL, USA, January 20 - 22, 2016}}.
\bibinfo{pages}{256--270}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2837614.2837655}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Toro and Tanter}{Toro and Tanter}{2015}]%
\bibfield{author}{\bibinfo{person}{Mat\'{\i}as Toro} {and}
\bibinfo{person}{\'{E}ric Tanter}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Customizable Gradual Polymorphic Effects for
Scala}. In \bibinfo{booktitle}{\emph{Proceedings of the 2015 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems, Languages,
and Applications}} \emph{(\bibinfo{series}{OOPSLA 2015})}.
\bibinfo{publisher}{ACM}, \bibinfo{address}{New York, NY, USA},
\bibinfo{pages}{935--953}.
\newblock

\bibitem[\protect\citeauthoryear{Vazou, Seidel, and Jhala}{Vazou
\bibfield{author}{\bibinfo{person}{Niki Vazou}, \bibinfo{person}{Eric~L.
Seidel}, {and} \bibinfo{person}{Ranjit Jhala}.}
\bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{LiquidHaskell: experience with refinement types in
the real world}. In \bibinfo{booktitle}{\emph{Proceedings of the 2014 {ACM}
{SIGPLAN} symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014}}.
\bibinfo{pages}{39--51}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2633357.2633366}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Xi}{Xi}{1998}]%
\bibfield{author}{\bibinfo{person}{Hongwei Xi}.}
\bibinfo{year}{1998}\natexlab{}.
\newblock \bibinfo{thesistype}{Ph.D. Dissertation}. \bibinfo{school}{Carnegie
Mellon University}.
\newblock
\newblock
\shownote{available as {\url{https://www.cs.cmu.edu/~rwh/theses/xi.pdf}}.}

\bibitem[\protect\citeauthoryear{Xi and Pfenning}{Xi and Pfenning}{1999}]%
\bibfield{author}{\bibinfo{person}{Hongwei Xi} {and} \bibinfo{person}{Frank
Pfenning}.} \bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Dependent Types in Practical Programming}. In
\bibinfo{booktitle}{\emph{Proceedings of the 26th Symposium on Principles of
Programming Languages}} \emph{(\bibinfo{series}{POPL '99})}.
\bibinfo{pages}{214--227}.
\newblock

\end{thebibliography}

%% Appendix

\end{document}