+ Instead of:
+ \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
+ We have a cumulative hierarchy, so that
+ \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
+ For example
+ \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
+
+ But in \mykant, you can forget about levels: the consistency is
+ checked automatically---a mechanised version of what Russell called
+ \emph{typical ambiguity}.
+\end{frame}
+
+\begin{frame}
+ \frametitle{OTT + user defined types}
+
+ For each type, we need to:
+ \begin{itemize}
+ \item Describe when two types formed by the defined type constructors
+ are equal;
+ \item Describe when two values of the defined type are equal;
+ \item Describe how to transport values of the defined type.
+ \end{itemize}
+\end{frame}
+
+\begin{frame}
+ \frametitle{OTT + hierarchy}
+
+ Since equalities reduce to functions abstracting over various things,
+ we need to make sure that the hierarchy is respected.
+
+ For example we have that
+ \[
+ \begin{array}{@{}l}
+ ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\
+ \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\
+ \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp)
+ \end{array}
+ \]
+
+ Subtle point---I discovered a problem in the theory after
+ submitting... but I have a fix.
+\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.
+\end{frame}
+
+\begin{frame}
+ \frametitle{Bidirectional type checking}
+
+ This technique is known as \emph{bidirectional} type checking---some
+ terms get \emph{checked}, some terms \emph{infer} types.
+
+ Usually used for pre-defined types or core calculi, \mykant\ extends
+ to user-defined types.
+\end{frame}
+
+\begin{frame}
+\begin{center}
+{\Huge Demo}
+\end{center}