\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{bidirectional typechecking}

\hypertarget{bidirectional_typechecking}{}\section*{{Bidirectional typechecking}}\label{bidirectional_typechecking}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{for_dependent_types}{For dependent types}\dotfill \pageref*{for_dependent_types} \linebreak
\noindent\hyperlink{other_type_theories}{Other type theories}\dotfill \pageref*{other_type_theories} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\emph{Bidirectional typechecking} is both a style of mathematical presentation of a [[type theory]] and a kind of [[algorithm]] for implementing one. The idea is that the basic [[judgment]] $t:A$ that a [[term]] $t$ belongs to a [[type]] $A$ is split into two judgments:

\begin{itemize}%
\item $t \Leftarrow A$: the term $t$ can be \emph{checked} to have the type $A$.
\item $t \Rightarrow A$: from the term $t$ we can \emph{infer}, or \emph{synthesize}, the type $A$ that it has.

\end{itemize}
The difference is that in $t\Leftarrow A$ we regard both $t$ and $A$ as ``given'' or ``inputs'', whereas in $t\Rightarrow A$ we regard only $t$ as an ``input'' and $A$ as an ``output'' that is ``computed'' from $t$. When presented as a pure [[deductive system]], these ``input/output modes'' do not mean anything, but when implemented as an algorithm they mean that we have two mutually recursive functions:

\begin{itemize}%
\item $check(t,A)$ which simply succeeds or fails.
\item $infer(t)$ which either returns a type $A$ or fails.

\end{itemize}
See [[logic programming]].

For example, from an un-annotated $\lambda$-abstraction such as the identity function $\lambda x.x$ we cannot infer its type: the variable $x$, and hence the result, could have any type. But we can \emph{check} that it has any given endomorphism type: $(\lambda x.x) \Leftarrow (A\to A)$ for any type $A$. On the other hand, if we can infer a type for the function $f$, i.e. $f\Rightarrow (A\to B)$ (for instance, $f$ could be a variable, since variables are declared with their types), and we can check that an argument $a$ has type $A$ (that is, $a\Leftarrow A$), then we can also infer that the application $f(a)$ has type $B$, that is $f(a) \Rightarrow B$. These observations correspond to bidirectional refinements of the usual typing rules for abstractions and applications:

\begin{displaymath}
\frac{\Gamma,x:A \vdash M \Leftarrow B}{\Gamma\vdash (\lambda x.M) \Leftarrow (A\to B)} \qquad \frac{\Gamma\vdash f \Rightarrow (A\to B) \qquad \Gamma\vdash a \Leftarrow A }{\Gamma \vdash f(a) \Rightarrow B}.
\end{displaymath}
Bidirectional typechecking is closely related to ``canonical forms only'' presentations of type theories (such as [[logical frameworks]]) that involve [[hereditary substitution]]. For instance, because we infer a type for an application $f(a)$ by inferring a type for $f$, but we can only \emph{check} the type of an un-annotated abstraction $\lambda x.M$, an un-augmented bidirectional theory cannot typecheck a $\beta$-[[redex]] $(\lambda x.M)(a)$. Thus it is a natural system in which to describe a type theory in which only canonical forms (no redexes) exist. But it is also easy to augment a bidirectional system with [[type ascription]], which mediates between the two modes and allows typechecking redexes: if we can check $t\Leftarrow A$, then we can \emph{infer} the same type of the \emph{ascribed} term $(t:A)\Rightarrow A$, allowing a redex to be written as $(\lambda x.M : A\to B)(a)$.

\begin{uremark}
There are many different notations used in the literature for the bidirectional typing judgments. Sometimes one finds $t\rightrightarrows A$ and $t\leftleftarrows A$ in place of our $t\Rightarrow A$ and $t\Leftarrow A$. Other times the order of the term and the type is reversed, for instance writing $t\in A$ for inferring and $A\ni t$ for checking. Sometimes upwards and downwards-pointing arrows are used instead of leftwards and rightwards ones (e.g. $t \uparrow A$ and $t \downarrow A$, or maybe $t :^\uparrow A$ and $t :^\downarrow A$ or a dozen other variants) --- but unfortunately there is no consensus on which judgment points up and which points down! It seems to be somewhat more common for checking to point up and inference to point down, as this matches the direction that ``information flows through the derivation tree'', but the opposite convention is found in plenty of papers too. (It could be that there is a ``modern'' consensus that only older papers violate.)

\end{uremark}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

\begin{itemize}%
\item Joshua Dunfield, Neel Krishnaswami, \emph{Bidirectional Typing} (Survey), 2019, (\href{https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf}{pdf})


\item Pierce, B. C., Turner, D. N.: \emph{Local Type Inference}, ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, 1998, Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1–44, (\href{http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf}{pdf}). This is usually cited as the ``original'' paper on bidirectional typechecking.


\item [[Frank Pfenning]], \emph{Lecture Notes on Bidirectional Type Checking}, \href{https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf}{pdf}


\item [[Conor McBride]], \emph{Basics of bidirectionality}, \href{https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/}{blog post}


\item David Christiansen, \emph{Bidirectional typing rules: a tutorial}, \href{http://www.davidchristiansen.dk/tutorials/bidirectional.pdf}{pdf}



\end{itemize}
\hypertarget{for_dependent_types}{}\subsubsection*{{For dependent types}}\label{for_dependent_types}

\begin{itemize}%
\item [[Thierry Coquand]], \emph{An algorithm for type-checking dependent types}, 1996, \href{https://core.ac.uk/download/pdf/82345314.pdf}{pdf}


\item Thierry Coquand and Makoto Takeyama, \emph{An Implementation of Type:Type}, 2002, \href{https://link.springer.com/chapter/10.1007/3-540-45842-5_4}{springerlink}


\item Ulf Norell, \emph{Towards a practical programming language based on dependent type theory}. PhD thesis, Chalmers University of Technology and Göteborg University, 2007. \href{http://www.cse.chalmers.se/~ulfn/papers/thesis.html}{web}


\item Andreas Abel, Thierry Coquand, Peter Dybjer \emph{Verifying a Semantic $\beta\eta$-Conversion Test for Martin-L\"o{}f Type Theory (extended version)}, 2008 \href{https://www.semanticscholar.org/paper/Verifying-a-Semantic-%CE%B2%CE%B7-Conversion-Test-for-Type-(-Abel-Coquand/ea73f57e4f1111b136cb9f0659c627dba25e53c8}{semantic scholar (includes pdf)}


\item Andreas Abel and Thorsten Altenkirch, \emph{A partial type checking algorithm for $Type:Type$}, 2008, \href{http://www.cs.nott.ac.uk/~psztxa/publ/msfp08.pdf}{pdf}


\item Andres L\"o{}h, Conor McBride and Wouter Swierstra, \emph{A Tutorial Implementation of a Dependently Typed Lambda Calculus}, 2009, \href{https://www.andres-loeh.de/LambdaPi/}{web} (includes Haskell code)


\item Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. \emph{A bi-directional refinement algorithm for the calculus of (co)inductive constructions}, 2012, \href{https://arxiv.org/abs/1202.4905}{arxiv}


\item Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. \emph{A concurrent logical framework I: Judgments and properties}. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003, \href{http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf}{pdf}



\end{itemize}
\hypertarget{other_type_theories}{}\subsubsection*{{Other type theories}}\label{other_type_theories}

\begin{itemize}%
\item Rowan Davies and Frank Pfenning. \emph{Intersection types and computational effects}. In P. Wadler, editor, Proceedings of the Fifth International Conference on Functional Programming (ICFP'00), pages 198-208, Montreal, Canada, September 2000. ACM Press. \href{http://www.cs.cmu.edu/~fp/papers/icfp00.pdf}{pdf}


\item Joshua Dunfield and Frank Pfenning. \emph{Tridirectional typechecking}. In X.Leroy, editor, Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL'04), pages 281-292, Venice, Italy, January 2004. ACM Press. Extended version available as Technical Report CMU-CS-04-117, March 2004. \href{http://www.cs.cmu.edu/~fp/papers/popl04.pdf}{pdf}


\item Joshua Dunfield, Neelakantan R. Krishnaswami, \emph{Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism}, 2013, \href{https://arxiv.org/abs/1306.6032}{arxiv}


\item Francisco Ferreira and Brigitte Pientka, \emph{Bidirectional Elaboration of Dependently Typed Programs}, 2014, \href{https://www.cs.mcgill.ca/~fferre8/papers/BidirectionalElaboration.pdf}{pdf}. Despite the name, this paper is not about full [[dependent type theory]] but only has one level of dependency.


\item Joshua Dunfield, Neelakantan R. Krishnaswami, \emph{Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types}, 2016, \href{https://arxiv.org/abs/1601.05106}{arxiv}



\end{itemize}
[[!redirects bidirectional type checking]] [[!redirects bidirectional type-checking]] [[!redirects type inference]] [[!redirects type synthesis]]



\end{document}