\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\definecolor{slidelightblue}{rgb}{.8,.8,1}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightblue#1{\textcolor{slidelightblue}{#1}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\large\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-5em}$}

\def\tto{\to\hspace{-5pt}\!\!\to}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large dependent types}

\red{logical verification} \\
week 8 \\
2004 11 03

\end{slide}

\begin{slide}
\sectiontitle{where are we?}
\slidetitle{Curry-Howard-de Bruijn continued}
\vspace{0pt}

\begin{center}
$\hspace{-1em}$\begin{tabular}{rcl}
propositional logic &$\leftrightarrow$& \textbf{simple} type theory \\
&& {$\qquad\lambda{\to}$} \\
\noalign{\medskip}
predicate logic &\red{$\leftrightarrow$}& \red{type theory with \textbf{dependent types}} \\
&& \red{$\qquad\lambda P$} \\
\noalign{\medskip}
\gray{2nd order propositional logic} &\gray{$\leftrightarrow$}& \gray{\textbf{polymorphic} type theory} \\
&& \gray{$\qquad\lambda 2$}
\end{tabular}$\hspace{-1em}$
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Barendregt's lambda cube}

$$
\xymatrix@!{
 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
   & & \green{\lambda C} \ar@{-}[dd]
\\
 \gray{\lambda2} \ar@{-}[ur]\ar@{-}[rr]\ar@{<-}[dd]|-{\mbox{\small\gray{polymorphism}}}
 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
\\
 & \lambda\underline\omega \ar@{-}'[r][rr]
 & & \lambda P\underline\omega
\\
 \red{\lambda{\to}} \ar@{->}[rr]|-{\mbox{\small\red{$\,$dependence$\,$}}}
   \ar@{-}[ur]
 & & \red{\lambda P} \ar@{-}[ur]
}
\vspace{-8pt}
$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{recap predicate logic}
\slidetitle{syntax}
\begin{tabular}{ll}
\parbox{14em}{
\medskip
\textbf{terms}
\begin{itemize}
\item[$\bullet$]
$\red{\green{f}(M_1, \dots, M_n)}$
\item[$\bullet$]
$\red{x}$
\end{itemize}
\vspace{12.3em}}
\parbox{12em}{
\medskip
\textbf{formulas}
\begin{itemize}
\item[$\bullet$]
$\red{\green{P}(M_1, \dots, M_n)}$
\item[$\bullet$]
$\top$
\item[$\bullet$]
$\bot$
\item[$\bullet$]
$\neg A$
\item[$\bullet$]
$\red{A \to B}$
\item[$\bullet$]
$A \land B$
\item[$\bullet$]
$A \lor B$
\item[$\bullet$]
$\red{\forall x.\, A}$
\item[$\bullet$]
${\exists x.\, A}$
\end{itemize}
}
\end{tabular}
\vspace{-7pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules}
\begin{center}
\begin{tabular}{cc}
\llap{\textbf{introduction rules}\hspace{-1.5em}} & \rlap{\hspace{-1.5em}\textbf{elimination rules}} \\
$I\top$ & \\
& $E\bot$ \\
$I[x]\neg$ & $E\neg$ \\
$\red{I[x]{\to}}$ & $\red{E{\to}}$ \\
$I\land$ & $El\land \quad Er\land$ \\
$Il\lor \quad Ir\lor$ & $E\lor$ \\
$\red{I\forall}$ & $\red{E\forall}$ \\
${I\exists}$ & ${E\exists}$ \\
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example}

$$\red{(\forall x.\, P(x)) \to \neg\exists y.\,\neg P(y)}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{dependent types}
\slidetitle{\texttt{natlist}}
\begin{alltt}
Inductive \red{natlist} : Set :=
    \green{nil} : natlist
  | \green{cons} : nat -> natlist -> natlist.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{append} \& \texttt{reverse}}
\begingroup
\def\{{\char`\{}%
\def\}{\char`\}}%
\begin{alltt}
Fixpoint \red{append} (k l : natlist) \{struct k\} : natlist :=\toolong
  match k with
    nil => l
  | cons h t => cons h (\red{append} t l)
  end.
\end{alltt}
\medskip
\begin{alltt}
Fixpoint \red{reverse} (k : natlist) : natlist :=
  match k with
    nil => nil
  | cons h t => \green{append} (\red{reverse} t) (cons h nil)
  end.
\end{alltt}
\endgroup
\vfill
\end{slide}

\begin{slide}
\slidetitle{lists of a given length}
\begin{alltt}
Fixpoint \red{zeroes} (n : nat) : natlist :=
  match n with
    O => nil
  | S n' => cons \green{0} (\red{zeroes} n')
  end.
\end{alltt}
\bigskip
\begin{eqnarray*}
0 &\red{\mapsto}&  \\
1 &\red{\mapsto}& \green{0} \\
2 &\red{\mapsto}& \green{0},\green{0} \\
3 &\red{\mapsto}& \green{0},\green{0},\green{0} \\
4 &\red{\mapsto}& \green{0},\green{0},\green{0},\green{0}
\end{eqnarray*}
\vspace{-15pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{dependent lists}
we will define a type for \red{lists of a given length}
\medskip

\begin{center}
\texttt{\ \ \ \ \ \ \ \ \ \ \ \ \ \green{a} :\ \red{(natlist\char`\_dep \black{6})}\ } \\
\end{center}
\medskip

this corresponds in normal programming languages to something like

\begin{center}
\texttt{\red{int} \green{a}\red{[\black{6}]}\ \ \ \ \ \ \ }
\end{center}
\bigskip

the type of \green{\texttt{a}} is called a \textbf{dependent} type \\
it \textbf{depends} on the natural number \texttt{6}
\medskip
\begin{center}
\texttt{\ \ \ \red{natlist\char`\_dep} :\ nat -> \blue{Set}\ \ \ \ \ \ \ } \\
\texttt{\ \red{natlist\char`\_dep} 6 :\ \blue{Set}\ \ \ \ \ \ \ \ \ \ \ \ \ \ }
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{natlist\char`\_dep}}
\begin{alltt}
Inductive natlist_dep : \advirecord{a1}{\red{nat ->}} Set :=
    nil : natlist_dep \advirecord{a2}{\red{O}}
  | cons : \advirecord{a3}{\blue{forall n : nat,}}
      \green{nat} -> natlist_dep \advirecord{a4}{\red{n}} -> natlist_dep \advirecord{a5}{\red{(S n)}}.
\end{alltt}
\adviwait
\adviplay{a1}
\adviplay{a2}
\adviplay{a4}
\adviplay{a5}
\adviwait
\adviplay{a3}
\adviwait
\medskip

$$\green{3, 1, 4, 1, 5, 9}$$
\begin{center}
\vspace{-\smallskipamount}
$\green{\downarrow}$
\vspace{-\smallskipamount}
\end{center}
\begingroup
\small
\begin{alltt}
cons 5 \green{3} (cons 4 \green{1} (cons 3 \green{4} (cons 2 \green{1} (cons 1 \green{5} (cons 0 \green{9} nil))))\medskip\toolong
                                                : (natlist_dep \red{6})\toolong
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{zeroes} for dependent lists}
\begin{alltt}
Fixpoint zeroes (n : nat) : natlist_dep \advirecord{c1}{\red{n}} :=
  match n \advirecord{c2}{\green{return natlist_dep n}} with
    O => nil
  | S n' => cons \advirecord{c3}{\red{n'}} O (zeroes n')
  end.
\end{alltt}
\adviwait
\adviplay{c1}
\adviplay{c3}
\adviwait
\adviplay{c2}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the type of dependent zeroes}
\vspace{0pt}

\begin{center}
\strut\rlap{\raisebox{3.45pt}{\hbox{\advirecord{e}{\blue{\underbar{\phantom{\texttt{zeroes :\ \red{nat ->} natlist\char`\_dep ?}}}}}}}}\texttt{zeroes :\ \red{nat ->} natlist\char`\_dep \red{?}\ \ \ \ \ \ \ \ \ \ }
\end{center}
\adviwait
\adviplay{e}

\begin{center}
\texttt{zeroes :\ \red{forall n :\ \red{nat},} natlist\char`\_dep \red{n}}
\end{center}
\bigskip
\bigskip
\adviwait

\blue{\textbf{dependent product}}
\medskip

\textbf{generalizes} the notion of \blue{function type}
\vfill
\end{slide}

\begin{slide}
\slidetitle{function types and dependent products}

$$A \to B$$
$$\gray{\downarrow}$$
$$\red{\Pi x : A.\, B}\bigskip\bigskip$$

\begin{center}
\texttt{A -> B}
\vspace{-.5\smallskipamount}

$\gray{\downarrow}$
\vspace{-.5\smallskipamount}

\texttt{\red{forall x :\ A, B\ }}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{append} for dependent lists}
\begingroup
\def\{{\char`\{}%
\def\}{\char`\}}%
\begin{alltt}
Fixpoint append \advirecord{b1}{\red{(n m : nat)}}
  (k : natlist_dep \advirecord{b2}{\red{n}}) (l : natlist_dep \advirecord{b3}{\red{m}}) \{struct k\} :
    natlist_dep \advirecord{b4}{\red{(plus n m)}} :=
  match k
    \advirecord{b5}{\green{in natlist_dep n return natlist_dep (plus n m)}}
  with
    nil => l
  | cons \advirecord{b6}{\red{n'}} h t => cons \advirecord{b7}{\red{(plus n' m)}} h (append \advirecord{b8}{\red{n' m}} t l)
  end.
\end{alltt}
\adviwait
\adviplay{b1}
\adviplay{b2}
\adviplay{b3}
\adviplay{b4}
\adviplay{b6}
\adviplay{b7}
\adviplay{b8}
\adviwait
\adviplay{b5}
\endgroup
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{reverse} for dependent lists}
\begingroup
\def\{{\char`\{}%
\def\}{\char`\}}%
\begin{alltt}
Fixpoint reverse
  (n : nat) (k : natlist_dep n) \{struct k\} :
    natlist_dep n :=
  match k in natlist_dep n return natlist_dep n with
    nil => nil
  | cons n' h t =>
      \advirecord{f1}{\red{eq_rec (plus n' 1) (fun n => natlist_dep n)}}
        \green{(append n' 1 (reverse n' t) (cons 0 h nil))}
        \advirecord{f2}{\red{(S n') (\blue{plus_one} n')}}
  end.
\end{alltt}
\bigskip
\endgroup
\adviwait
has type \green{\texttt{natlist\char`\_dep (plus n' 1)}}

but should have type \red{\texttt{natlist\char`\_dep (S n')}}
\adviwait
\adviplay{f1}
\adviplay{f2}
\vspace{-8pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{reduction of dependent types}
\begin{eqnarray*}
\texttt{append nil l} &:& \red{\texttt{natlist\char`\_dep (plus O m)}} \\
&& \qquad \red{\rlap{\raisebox{-2pt}{$\downarrow$}}\mathord{\downarrow}\strut_{\beta\delta\iota}} \\
\noalign{\smallskip}
\texttt{l} &:& \red{\texttt{natlist\char`\_dep m}}
\end{eqnarray*}
\vfill
\end{slide}

\begin{slide}
\slidetitle{equality and dependent types}
\begin{eqnarray*}
\texttt{reverse (cons n' h t)} &:& \red{\texttt{natlist\char`\_dep (S n')}} \\
\noalign{\medskip}
&& \red{\mbox{is not interchangable with}} \\
\noalign{\medskip}
\texttt{append (reverse n' t)} &:& \red{\texttt{natlist\char`\_dep (plus n' 1)}} \\
\noalign{\vspace{-\smallskipamount}}
\texttt{(cons 0 h nil)}
\end{eqnarray*}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{Curry-Howard-de Bruijn for predicate logic}
\slidetitle{Brouwer-Heyting-Kolmogorov for implication}
\vspace{0pt}

\begin{center}
proof of $\red{A \to B}$
\bigskip

\green{is defined to be}
\bigskip

\red{function} that maps proofs of $A$ to proofs of $B$
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Brouwer-Heyting-Kolmogorov for universal quantification}
\vspace{0pt}

\begin{center}
proof of $\red{\forall x.\, P(x)}$
\bigskip

\green{is defined to be}
\bigskip

\red{function} that maps objects $x$ to proofs of $P(x)$
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the proper type system $\lambda P$}
\slidetitle{unification of terms and types}
\vspace{0pt}
\begin{center}
\begin{tabular}{rcl}
$\blue{\lambda{\to}}$ && terms and types are separate worlds \\
\noalign{$$\green{\lambda x.\,x}$$ $$\red{A \to B}$$}
\noalign{\bigskip}
$\blue{\lambda P}$ && terms and types are the same kind of expression \\
\noalign{$$\green{\lambda x.\,} \red{A \to B}$$}
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{syntax}
\begin{itemize}
\item[$\bullet$]
\textbf{variables}

$x$, $y$, $z$, \dots
\item[$\bullet$]
\textbf{lambda abstraction}

$\lambda x : M.\, N$
\item[$\bullet$]
\textbf{function application}

$M N$
\item[$\bullet$]
%\adviwait
\textbf{dependent product}

$\red{\Pi x : M.\, N}$
\item[$\bullet$]
\textbf{two `sorts'}

$\red{*}$ and $\red{\Box}$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules}
\bigskip

\begin{center}
\blue{\textbf{next week}}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{different notations for dependent products}
syntactic alternatives

$$\red{\Pi} x : M.\, N$$
$$\red{\forall} x : M.\, N\medskip$$

just different ways of writing exactly the same term
\bigskip

\blue{coq syntax}
$$
\texttt{\ \red{forall} x :\ M, N}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Prop}, \texttt{Set} and \texttt{Type} in $\lambda P$}
\vspace{0pt}

\begin{center}
\begin{tabular}{rcl}
\texttt{Prop} &${\to}$& $\red{*}$ \\
\texttt{Set} &${\to}$& $\red{*}$ \\
\texttt{Type} &${\to}$& $\green{\Box}$ \\
\noalign{\bigskip\bigskip}
\texttt{Prop :\ Type} &${\to}$& $\red{*} : \green{\Box}$ \\
\texttt{Set :\ Type} &${\to}$& $\red{*} : \green{\Box}$ \\
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{terms and formulas of minimal predicate logic in $\lambda P$}
\begin{center}
\begin{tabular}{rcl}
$f(M_1,\dots,M_n)$ &{$\to$}& $\red{f} M_1 \dots M_n$ \\
$x$ &{$\to$}& $x$ \\
\noalign{\bigskip}
$P(M_1,\dots,M_n)$ &{$\to$}& $\red{P} M_1 \dots M_n$ \\
$A \to B$ &{$\to$}& ${\Pi} {u} : A.\, B$
\\ % \qquad is the same as \quad $A \to B$ \\
$\forall x. A$ &{$\to$}& ${\Pi} x : \texttt{\green{Terms}}.\, A$
\end{tabular}
\end{center}
\bigskip
where
\vspace{-\medskipamount}
\begin{eqnarray*}
\texttt{\green{Terms}} &\hspace{-.6em}:\hspace{-.6em}& * \\
\noalign{\smallskip}
\red{f} &\hspace{-.6em}:\hspace{-.6em}& \Pi x_1 : \texttt{Terms}.\, \dots\, \Pi x_n : \texttt{Terms}.\, \texttt{Terms} \\
\red{P} &\hspace{-.6em}:\hspace{-.6em}& \Pi x_1 : \texttt{Terms}.\, \dots\, \Pi x_n : \texttt{Terms}.\, *
\end{eqnarray*}
\vspace{-17pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{proofs in $\lambda P$: implication}
$$
\hspace{2em}
{
\begin{array}{c}
[\green{A}^u] \\
\blue{\vdots} \\
\green{B}
\end{array}
\over
\strut
\red{A \to B}
}
\enskip
{I[{u}]{\to}}
\hspace{5em}
{
%\strut
%\Gamma,\, {u} : \green{A} \,\vdash\, \blue{M} : \green{B}
%\over
\strut
%\Gamma \,\vdash\,
\lambda {u} : \green{A}.\, \blue{M} \;:\; \red{\Pi u : A.\, B}
}
\vspace{-.7\bigskipamount}
$$
\rightline{with\quad $\blue{M} \;:\; \rlap{\green{$B$}}\phantom{\Pi u : A.\, B}$}

$$
\hspace{2em}
{
\begin{array}{c}
\blue{\vdots} \\
\green{A \to B}
\end{array}
\qquad
\begin{array}{c}
\blue{\vdots} \\
\green{A}
\end{array}
\over
\strut
\red{B}
}
\enskip
{E{\to}}
\hspace{5.7em}
{
%\strut
%\Gamma \,\vdash\, {t} : \green{A \to B}
%\qquad
%\Gamma \,\vdash\, {u} : \green{A}
%\over
\strut
%\Gamma \,\vdash\,
\blue{M N} \;:\; \red{B}
}\hspace{5.3em}
\vspace{-.7\bigskipamount}
$$
\rightline{with\quad
$\blue{M} \;:\; \green{\Pi u : A.\, B}$}
\rightline{$\blue{N} \;:\; \rlap{\green{$A$}}\phantom{\Pi u : A.\, B}$}
\vfill
\end{slide}

\begin{slide}
\slidetitle{proofs in $\lambda P$: universal quantification}
$$
\hspace{2em}
{
\begin{array}{c}
\blue{\vdots} \\
\green{A}
\end{array}
\over
\strut
\red{\forall x.\, A}
}
\enskip
I\forall
\hspace{5em}
{
\strut
\lambda {x} : \texttt{Terms}.\, \blue{M} \;:\; \red{\Pi x : \texttt{Terms}.\, A}
}
\vspace{-.7\bigskipamount}
$$
\rightline{with\quad $\blue{M} \;:\; \rlap{\green{$A$}}\phantom{\Pi x : \texttt{Terms}.\, A}$}

$$
\hspace{2.6em}
{
\begin{array}{c}
\vdots \\
\green{\forall x.\, A}
\end{array}
\over
\strut
\red{A[x:={N}]}
}
\enskip
E\forall
\hspace{7.8em}
{
%\strut
%\Gamma \,\vdash\, {M} : \green{A \to B}
%\qquad
%\Gamma \,\vdash\, {N} : \green{A}
%\over
\strut
%\Gamma \,\vdash\,
\blue{M N} \;:\; \red{A[x:={N}]}
}\hspace{3.2em}
\vspace{-.7\bigskipamount}
$$
\rightline{with\quad
$\blue{M} \;:\; \green{\Pi x : \texttt{Terms}.\, A}$}
\rightline{$\blue{N} \;:\; \rlap{{\texttt{Terms}}}\phantom{\Pi x : \texttt{Terms}.\, A}$}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{examples}
\slidetitle{example 1}

$$\red{\forall x.\, (P(x) \to (\forall y.\, P(y) \to A) \to A)}$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{example 2}

$$\red{(\forall x.\, P(x) \to Q(x)) \to (\forall x.\, P(x)) \to \forall y.\, Q(y)}$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{dependent types in programming}
\slidetitle{\texttt{printf}}
what is the type of \red{\texttt{printf}}\exclspace?

$$\begin{array}{rcl}
\texttt{printf}\rlap{\texttt{("hello\char`\\n")}} \\
\noalign{\vspace{-\smallskipamount}}
\texttt{printf}\rlap{\texttt{("\char`\%d\char`\\n", 3)}} \\
\noalign{\vspace{-\smallskipamount}}
\texttt{printf}\rlap{\texttt{(}\rlap{$s$\texttt{, }\dots\texttt{)}}} \\
\noalign{\bigskip}
\adviwait
\texttt{printf} &:& \texttt{string} \to \texttt{unit} \\
\noalign{\vspace{-\smallskipamount}}
\texttt{printf} &:& \texttt{string} \to \texttt{int} \to \texttt{unit} \\
\noalign{\vspace{-\smallskipamount}}
\texttt{printf} &:& \adviwait\red{\Pi s : \texttt{string}\,.\; \texttt{printftype}\;s} \\
\noalign{\bigskip}
\green{\texttt{printftype}} &:& \green{\texttt{string} \to \texttt{Set}}
\end{array}$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{printftype}}
\begingroup
\def\xdots{\textsf{\dots}}
\begin{alltt}
Fixpoint printftype (s : \green{string}) : Set :=
  match s with
    nil => \green{unit}
  | cons \red{'%'} (cons \red{'d'} t) => \green{int} -> printftype t
  | cons \red{'%'} (cons \red{'c'} t) => \green{char} -> printftype t
  | cons \red{'%'} (cons \red{'f'} t) => \green{float} -> printftype t
  | cons \red{'%'} (cons \red{'s'} t) => \green{string} -> printftype t
  | \xdots
  | cons _ t => printftype t
  end.
\end{alltt}
\endgroup
\vfill
\end{slide}

\begin{slide}
\slidetitle{dependently typed functional programming languages}
\begin{itemize}
\item[$\bullet$]
\textbf{cayenne}

`dependent haskell'

\green{Lennart Augustsson}
\item[$\bullet$]
\textbf{dependent ML}

\green{Hongwei Xi}
\item[$\bullet$]
\red{\textbf{epigram}}

\green{Conor McBride}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the religion of dependent types}
\vspace{0pt}

\begin{quote}
Why do dependent types matter? Types matter. That's what they're for -- to classify data with respect to criteria which matter: how they should be stored in memory, whether they can be safely passed as inputs to a given operation, even who is allowed to see them. Dependent types are types expressed in terms of data, explicitly relating their inhabitants to that data. As such, \red{they enable you to express more of what matters about data}. Dependent types are better at mattering on your behalf, and that is why I hope they might matter to you.
\end{quote}
\bigskip

\rightline{-- \green{Conor McBride}}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{summary}
\slidetitle{the three main things we have seen today}
\begin{itemize}
\item[$\bullet$]
\textbf{dependent types in programming}
\item[$\bullet$]
\textbf{generalizing function types to dependent products}
$$A \to B\vspace{-\smallskipamount}$$
$${\downarrow}\vspace{-\smallskipamount}$$
$$\red{\Pi x : A.\, B}$$
\item[$\bullet$]
\textbf{Curry-Howard-de Bruijn for predicate logic}
\end{itemize}
\vfill
\end{slide}

\end{document}