+
+ \begin{center}
+ \begin{tikzpicture}[remember picture, node distance=1.5cm]
+ \begin{pgfonlayer}{foreground}
+ % Place nodes
+ \node (x) {$x$};
+ \node [right of=x] (y) {$y$};
+ \node [right of=y] (z) {$z$};
+ \node [below of=z] (k) {$k$};
+ \node [left of=k] (j) {$j$};
+ %% Lines
+ \path[->]
+ (x) edge node [above] {$<$} (y)
+ (y) edge node [above] {$\le$} (z)
+ (z) edge node [right] {$<$} (k)
+ (k) edge node [below] {$\le$} (j)
+ (j) edge node [left ] {$\le$} (y);
+ \end{pgfonlayer}{foreground}
+ \end{tikzpicture}
+ \begin{tikzpicture}[remember picture, overlay]
+ \begin{pgfonlayer}{background}
+ \fill [red, opacity=0.3, rounded corners]
+ (-2.7,2.6) rectangle (-0.2,0.05)
+ (-4.1,2.4) rectangle (-3.3,1.6);
+ \end{pgfonlayer}{background}
+ \end{tikzpicture}
+ \end{center}
+\end{frame}
+
+\begin{frame}
+ \frametitle{Bidirectional type checking}
+ \[
+ \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
+ \]
+
+ With no type inference, we have explicit types for the constructors:
+ \[
+ \begin{array}{@{}l@{\ }l}
+ \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
+ \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
+ \end{array}
+ \]
+ ...ugh:
+ \[
+ \mydc{cons}\myappsp \mynat\myappsp 1 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 2 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 3 \myappsp (\mydc{nil}\myappsp \mynat)))
+ \]
+ Instead, annotate terms and propagate the type:
+ \[
+ \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
+ \]
+ Conversely, when we use eliminators the type can be inferred.