SlidesCharla.tex

\documentclass[xcolor=dvipsnames]{beamer} % en min\'uscula!
\usefonttheme{professionalfonts} % fuentes de LaTeX
\usetheme{Warsaw} % tema escogido en este ejemplo
\usecolortheme[named=blue]{structure}
%%%% packages y comandos personales %%%%
\usepackage[latin1]{inputenc}
\usepackage{latexsym,amsmath,amssymb} % S\'imbolos
\usepackage{xcolor}
\usepackage{MnSymbol}

\usepackage{bussproofs} 

\newcommand{\cf}[1]{\textcolor{blue}{#1}}
\newcommand{\ct}[1]{\textcolor{blue}{#1}}
\newcommand{\cc}[1]{\textcolor{ForestGreen}{#1}}
\newcommand{\ck}[1]{\textcolor{orange}{#1}}

\newcommand{\N}{\ct{\mathbb{N}}}
\newcommand{\ra}{\rightarrow}
\newcommand{\T}{ \ \ \ \ }

 \newcommand{\tjud}[2]
  {\ensuremath{#1\,:\,#2}}
 \newcommand{\depFun}[3] {
  {\ensuremath{\Pi_{(\tjud{#1}{#2})}\,#3\,#1}}
 }
 \newcommand{\cprod}[2]
  {\ensuremath{#1 \times #2}
 }
 \newcommand{\depPair}[3]
 {\ensuremath{\Sigma_{(\tjud{#1}{#2})}\,#3\,#1}
 }

\begin{document}
\beamertemplatenavigationsymbolsempty
\title{Programación certificada con lenguajes con tipos dependientes}
\author{{Alejandro Gadea, Emmanuel Gunther}\\
\vspace*{0.5cm}}
\date{14 de Noviembre de 2014}
\frame{\titlepage}

\section{Introducción}

\begin{frame}

\begin{block}{ }
 En el desarrollo de software los programas se escriben esperando que
 satisfaga una especificación.
\end{block}

\pause

\begin{exampleblock}{Especificación de head}
 La función \cf{head} toma una lista de elementos no vacía y retorna el primero de ellos.
\end{exampleblock}

\pause

\begin{block}{}
 En la práctica en general no se asegura que un programa cumpla con la especificación.
\end{block}


\end{frame}

\begin{frame}

\begin{block}{ }
 Los sistemas de tipos agregan expresividad a los programas, permitiendo expresar propiedades que deben satisfacer.
\end{block}

\pause

\begin{exampleblock}{head en python}
  \ck{def} \cf{head} (l):
  
  \T \ck{return} l[0]
\end{exampleblock}

\pause

\begin{block}{}
  Podríamos tener en un programa la línea \cf{head} (\cc{true}) (lo cual no cumple una precondición) 
  y tendríamos un error en tiempo de ejecución.
\end{block}

\end{frame}

\begin{frame}
  \begin{block}{}
   En un lenguaje con sistema de tipos fuerte podemos especificar que la función \cf{head} 
   toma como argumento una lista y retorna un elemento:
  \end{block}

  \pause
  
  \begin{exampleblock}{head en haskell}
    \cf{head} :: [a] $\rightarrow$ a
    
    \cf{head} (x : xs) = x
  \end{exampleblock}  

  \pause
  
  \begin{block}{}
    Sin embargo podríamos hacer \cf{head} $[]$, lo cual violaría la precondición de que la lista no sea vacía.
     y tendríamos un error en tiempo de ejecución.
  \end{block}
  

\end{frame}

\begin{frame}
  \begin{block}{}
    Fortaleciendo el sistema de tipos podemos agregar información sobre lo que se espera de un programa:
  \end{block}

  \pause
  
  \begin{exampleblock}{head en agda}
    \cf{head} : \{a : Set\}  $\rightarrow$ (xs : List a) $\rightarrow$ 0 $<$ length xs $\rightarrow$ a \\
    \cf{head} $[]$ ()\\
    \cf{head} (x $ :: $ xs) \_ = x
  \end{exampleblock}  

  \pause
  
  \begin{block}{}
    La función \cf{head} ahora espera una lista de elementos y una \textit{prueba} de que tiene más de un elemento.
  \end{block}

  \pause
  
  \begin{block}{}
    Ahora nunca podría llamarse \cf{head} con una lista vacía ya que no se podría \textit{construir} 0 $<$ length $[]$.
  \end{block}

\end{frame}

\section{Teoría de tipos}

\begin{frame}
  \begin{block}{}
   La teoría que permite tener un sistema de tipos con esta expresividad es la \textbf{Teoría de Tipos}.
  \end{block}
  
  \pause
  
  \begin{block}{}
   Surge como una teoría fundacional de la matemática. Es alternativa a la clásica teoría de conjuntos que
   conocemos.
  \end{block}  

  \pause
    
  \begin{block}{}
    En vez de tener proposiciones lógicas y conjuntos de elementos, en la teoría de tipos sólo existen los \textbf{tipos}. 
  \end{block}

\end{frame}

\begin{frame}

    \begin{block}{}
     Un \textbf{tipo} puede interpretarse como un conjunto de elementos, pero también como una proposición
     lógica, y los elementos del mismo serán \textbf{pruebas} de su validez.
    \end{block}
    
    \pause

    \begin{block}{}
     Para que exista un elemento, debe tener un tipo. De esta manera no podremos expresar algo como ``sea
     $x$ tal que ...'' Sino que sólo podemos hablar de $x\,:\,A$ ($x$ tiene tipo $A$).
    \end{block}
    

\end{frame}

\begin{frame}

    \begin{block}{}
     Puesto que todo elemento debe tener un tipo, también los tipos mismos deberán tenerlo. A los tipos de tipos
     se les suele llamar \textit{universos}.
    \end{block}
    
    \pause

    \begin{block}{}
     Para evitar paradojas se introduce una jerarquía en los universos:
     \begin{align*}
      \tjud{U_0}{\tjud{U_1}{\tjud{U_2}{...}}}
     \end{align*}
    \end{block}
    
    \pause
    
    \begin{block}{}
     Si no es necesario saber a qué nivel pertenece un tipo, simplemente escribimos $U$ para referirnos al universo.
    \end{block}
    
\end{frame}


\begin{frame}
  
  \begin{block}{Definición de tipos}
   \begin{itemize}
    \item Reglas de formación.
    \item Constructores o reglas de introducción.
    \item Eliminadores y regla de computación.
   \end{itemize}

  \end{block}

  \pause
  
  \begin{block}{Funciones}
   \begin{itemize}
    \item Dados $\tjud{A}{U}$, $\tjud{B}{U}$ se define el tipo $A \rightarrow B$.
    \item Para \textbf{introducir} una función se puede realizar una definición o utilizar
    el constructor $\lambda\,(\tjud{x}{A}).E$
    \item El \textbf{eliminador} en las funciones es la \textbf{aplicación}:
      \begin{align*}
        (\lambda\,x.E)\,a\;\equiv\;E\,[x \longrightarrow a]
      \end{align*}
   \end{itemize}

  \end{block}

\end{frame}

\begin{frame}
    \begin{block}{}
     Con el tipo de las funciones, se puede definir una función que retorne un tipo, a lo que solemos
     llamar \textbf{familias de tipos} (o familias indexadas en algún tipo):
    \end{block}

    \pause
   
   \begin{block}{Familias de tipos}
      Si $\tjud{A}{U}$, a la función $\tjud{B}{A \rightarrow U}$ se le llama familia indexada por $A$.
  \end{block}

\end{frame}

\begin{frame}
    \begin{block}{}
     Se pueden definir funciones más generales que las habituales donde el valor de retorno puede depender
     del valor del dominio:
    \end{block}
  
   \pause

    \begin{block}{Funciones dependientes}
      \begin{itemize}
       \item Dados $\tjud{A}{U}$ y $\tjud{B}{A \rightarrow U}$ se define el tipo $\depFun{a}{A}{B}$. Otra notación para
             este tipo podría ser $(\tjud{a}{A}) \rightarrow B\,a$.
       \item Las reglas de introducción y eliminación son las mismas que para las funciones normales.
      \end{itemize}
    \end{block}
    
    \pause
    
    \begin{block}{}
     Observemos que con un elemento de $\depFun{a}{A}{B}$ se puede obtener un elemento de $B\,a$ \textbf{para cada}
     $\tjud{a}{A}$.
    \end{block}

\end{frame}

\begin{frame}
    \begin{block}{Producto}
      \begin{itemize}
       \item Dados dos tipos $\tjud{A}{U}$ y $\tjud{B}{U}$, introducimos el tipo $\tjud{\cprod{A}{B}}{U}$, al cual comunmente llamamos
             \textit{producto cartesiano}. 
       \item A partir de dos elementos $\tjud{a}{A}$ y $\tjud{b}{B}$, podemos construir el elemento $\tjud{(a,b)}{\cprod{A}{B}}$ del producto
       cartesiano.
       \item Los eliminadores del producto obtienen un elemento de $A$ o uno de $B$ a partir de $\tjud{\cprod{A}{B}}{U}$:
            \begin{align*}
              &\tjud{pr_1}{\cprod{A}{B} \rightarrow A}\\
              &pr_1\,(a,b)\,=\,a\\              
              &\tjud{pr_2}{\cprod{A}{B} \rightarrow B}\\
              &pr_2\,(a,b)\,=\,b\\
            \end{align*}
      \end{itemize}
    \end{block}
\end{frame}

\begin{frame}
    \begin{block}{}
     De la misma forma que generalizamos las funciones, podemos generalizar el producto:
    \end{block}
    
    \pause
    
    \begin{block}{Pares dependientes}
      \begin{itemize}
       \item Dados un tipo $\tjud{A}{U}$ y una familia $\tjud{B}{A \rightarrow U}$ definimos el tipo de pares dependientes
              \begin{align*}
              \depPair{a}{A}{B}
              \end{align*}
       \item El constructor y los eliminadores son los mismos que para el producto, solo que teniendo en cuenta que el tipo
             del segundo elemento de un par depende del primer elemento.
      \end{itemize}
    \end{block}
    \pause
    \begin{block}{}
     Observemos que para poder construir un elemento de $\depPair{a}{A}{B}$ debe \textbf{existir} un $\tjud{a}{A}$.
    \end{block}

\end{frame}

\begin{frame}
    \begin{block}{}
     Otros tipos importantes que definimos son los siguientes:
    \end{block}
    
    \pause
    
    \begin{block}{}
      \begin{itemize}
       \item \textbf{Coproducto}. A partir $\tjud{A}{U}$, $\tjud{B}{U}$, se define el tipo $\tjud{A + B}{U}$. Podemos representar
                                  la unión disjunta de dos tipos.
      \pause
      
       \item \textbf{Tipo vacío}. El tipo que no contiene ningún elemento. Lo notamos con $\bot$. 
       \pause
       \item \textbf{Tipo unario}. El tipo que tiene exactamente un elemento. Lo notamos con $\top$.
      \end{itemize}
    \end{block}
\end{frame}

\begin{frame}
    \begin{block}{}
     Podemos observar una analogía entre los tipos que definimos previamente y los conectivos de la lógica proposicional:
    \end{block}
    
    \pause
    
    \begin{block}{Reglas para el $\wedge$}
      \AxiomC{$p$}
      \AxiomC{$q$}
      \LeftLabel{Introducción de $\wedge$:}
      \BinaryInfC{$p \wedge q$}
      \DisplayProof
      \quad
      \AxiomC{$p \wedge q$}
      \LeftLabel{Eliminación de $\wedge$:}
      \UnaryInfC{$p$}
      \DisplayProof
      \quad
      \AxiomC{$p \wedge q$}
      \UnaryInfC{$q$}
      \DisplayProof
    \end{block}
    
    \pause
    
    \begin{block}{Reglas del producto}
      \AxiomC{$\tjud{a}{A}$}
      \AxiomC{$\tjud{b}{B}$}
      \BinaryInfC{$\tjud{(a,b)}{\cprod{A}{B}}$}
      \DisplayProof
      \quad
      \AxiomC{$\tjud{t}{\cprod{A}{B}}$}
      \UnaryInfC{$\tjud{pr_1\,t}{A}$}
      \DisplayProof
      \quad
      \AxiomC{$\tjud{t}{\cprod{A}{B}}$}
      \UnaryInfC{$\tjud{pr_2\,t}{B}$}
      \DisplayProof
    \end{block}
    
\end{frame}

\begin{frame}
 \begin{block}{}
  Podemos hacer la misma correspondencia con el resto de los conectivos:
 \end{block}

 \pause
 
 \begin{block}{Lógica proposicional y teoría de tipos}
  \begin{itemize}
  \item $\mathbf{True}$ se corresponde con $\mathbf{\top}$.
  \item $\mathbf{False}$ se corresponde con $\mathbf{\bot}$.
  \item $\mathbf{A \wedge B}$ se corresponde con $\cprod{A}{B}$.
  \item $\mathbf{A \vee B}$ se corresponde con $A + B$.
  \item $\mathbf{A \Rightarrow B}$ se corresponde con $A \rightarrow B$.
  \item $\mathbf{A \Leftrightarrow B}$ se corresponde con $\cprod{(A \rightarrow B)}{(B \rightarrow A)}$.
  \item $\mathbf{\neg A}$ se corresponde con $A \rightarrow \mathbf{\bot}$.
\end{itemize}
 \end{block}

\end{frame}

\begin{frame}
  \begin{block}{}
    Con la lógica de predicados tenemos la siguiente correspondencia:
  \end{block}
  
  \pause
  
  \begin{block}{Lógica de predicados y teoría de tipos}
   \begin{itemize}
    \item ($\forall x$, $P\,x$) se corresponde con $\depFun{x}{A}{P}$.
    \item ($\exists x$, $P\,x$) se corresponde con $\depPair{x}{A}{P}$.
    \end{itemize}
  \end{block}

  \pause
  
  \begin{block}{}
   Gracias a esta correspondencia podemos tener un lenguaje de programación con un sistema
   de tipos que permita expresar proposiciones lógicas.
  \end{block}

  
\end{frame}

\section{Introducción a Agda}
 
\begin{frame}

\begin{block}{}
Utilizando ejemplos presentemos las diferentes características que
mencionamos antes sobre los sistema de tipos dependientes, utilizando
Agda y cómo éstas nos permite expresar propiedades y diferentes tipos.
\end{block}

\pause

\begin{block}{}
\begin{itemize}

\item Entender por qué \textit{funciona} el \cf{head} presentado anteriormente.\\
\item Presentar una implementación más adecuada utilizando vectores.\\
\item Implementar algunas cosas interesantes aprovechando la definición de los
vectores.
\end{itemize}
\end{block}

\end{frame}

\begin{frame}

\begin{block}{}
Empecemos introduciendo las listas y los naturales.
\end{block}

\pause

\begin{block}{Listas de A}

\ck{data} \ct{List} (A : \ct{Set}) : \ct{Set} \ck{where}\\
\T \cc{$[]$} : \ct{List} A\\
\T \cc{$\_::\_$} : A $\ra$ \ct{List} A $\ra$ \ct{List} A

\end{block}

\pause

\begin{block}{Naturales}

\ck{data} $\N$ : \ct{Set} \ck{where}\\
\T \cc{zero} : $\N$\\
\T \cc{suc}  : $\N$ $\ra$ $\N$

\end{block}

\end{frame}

\begin{frame}
\begin{block}{}
Recordando el tipo del \cf{head}:\\

\

\{A : \ct{Set}\} $\ra$ 
(xs : \ct{List} A) $\ra$ \cc{zero} $<$ \cf{length} xs $\ra$ A\\

\

Nos falta definir el tipo $<$. Es interesante mencionar que para
este tipo podemos empezar a pensar a los valores que se pueden construir
como si fueran pruebas en el sentido matemático.
\end{block}

\pause

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\pause

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \pause
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) p$_{::}$ = ¿?
  \end{block}  

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) p$_{::}$ = x
  \end{block}  

\pause

\begin{block}{}
Podemos preguntarnos que valores (o pruebas) podrían ser p$_{[]}$ y p$_{::}$
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) p$_{::}$ = x
  \end{block}  

\begin{block}{}
El tipo de p$_{::}$ : \cc{zero} $<$ \ct{length} (x \cc{$::$} xs)
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) p$_{::}$ = x
  \end{block}  

\begin{block}{}
El tipo de p$_{::}$ : \cc{zero} $<$ \cc{suc} (\cf{length} xs)
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) p$_{::}$ = x
  \end{block}  

\begin{block}{}
El tipo de p$_{::}$ : \cc{suc} \cc{zero} $\leq$ \cc{suc} (\cf{length} xs)
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) p$_{::}$ = x
  \end{block}  

\begin{block}{}
El tipo de p$_{::}$ = \cc{s$\leq$s} p'\\
El tipo de p' : \cc{zero} $\leq$ \cf{length} xs
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) (\cc{s$\leq$s} \cc{zero}) = x
  \end{block}  

\pause

\begin{block}{}
¿Podremos hacer lo mismo ahora para p$_{[]}$ ?\\ \pause
El tipo de p$_{[]}$ : \cc{zero} $<$ \ct{length} $[]$
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) (\cc{s$\leq$s} \cc{zero}) = x
  \end{block}  

\begin{block}{}
El tipo de p$_{[]}$ : \cc{zero} $<$ \cc{zero}
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} p$_{[]}$ = ¿?\\
    \cf{head} (x \cc{$::$} xs) (\cc{s$\leq$s} \cc{zero}) = x
  \end{block}  

\begin{block}{}
El tipo de p$_{[]}$ : \cc{suc} \cc{zero} $\leq$ \cc{zero}
\end{block}

\end{frame}

\begin{frame}

\begin{block}{Orden entre naturales}

\ck{data} \ct{\_$\leq$\_} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set} \ck{where}\\
\ \ \ \ \cc{z$\leq$n} : \{n : $\N$\}                 $\ra$ \cc{zero}  \ct{$\leq$} n\\
\ \ \ \ \cc{s$\leq$s} : \{m n : $\N$\} $\ra$ (m$\leq$n : m \ct{$\leq$} n) $\ra$ \cc{suc} m \ct{$\leq$} \cc{suc} n

\end{block}

\begin{block}{Orden estricto entre naturales}
\cf{$\_<\_$} : $\N$ $\ra$ $\N$ $\ra$ \ct{Set}\\
m \cf{$<$} n = \cc{suc} m \cf{$\leq$} n
\end{block}

\begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} ()\\
    \cf{head} (x \cc{$::$} xs) (\cc{s$\leq$s} \cc{zero}) = x
\end{block}  

\end{frame}

\begin{frame}

  \begin{block}{head en Agda}
    \cf{head} : \{A : \ct{Set}\}  $\ra$ (xs : \ct{List} A) $\ra$ 
    \cc{zero} $<$ \ct{length} xs $\rightarrow$ A \\
    \cf{head} \cc{$[]$} ()\\
    \cf{head} (x \cc{$::$} xs) $\_$ = x
  \end{block}
  
\begin{block}{Pattern absurdo}

El pattern absurdo nos permite decir que un caso nunca puede
ocurrir cuando es imposible construir un valor del tipo requerido y por
lo tanto nos salvamos de tener que dar una definición de la función
para ese caso.

\end{block}

\end{frame}

\begin{frame}

\begin{block}{Replanteando el problema}
Las listas funcionan muy bien para muchas cosas. Pero tal vez
podamos crear un nuevo tipo de dato aprovechando el sistema de tipos
de Agda de manera tal de tener un tipo lista que no solo lleve la
información acerca del tipo de los elementos, sino además de su
tamaño.\\

De esta manera podemos definir un \cf{head} nuevo que no necesite
ninguna prueba para ser \textit{usado}.
\end{block}

\pause

\begin{block}{Vectores}

\ck{data} \ct{Vec} (A : \ct{Set}) : $\N$ $\ra$ \ct{Set} \ck{where}\\
\pause
\T \cc{$[]$}     : \ct{Vec} A \cc{zero}\\
\pause
\T \cc{\_$::$\_} : \{n : $\N$\} $\ra$ A $\ra$ \ct{Vec} A n $\ra$ \ct{Vec} A (\cc{suc} n)

\end{block}

\end{frame}

\begin{frame}

\begin{block}{Vectores}

\ck{data} \ct{Vec} (A : \ct{Set}) : $\N$ $\ra$ \ct{Set} \ck{where}\\
\T \cc{$[]$}     : \ct{Vec} A \cc{zero}\\
\T \cc{\_$::$\_} : \{n : $\N$\} $\ra$ A $\ra$ \ct{Vec} A n $\ra$ \ct{Vec} A (\cc{suc} n)

\end{block}

\begin{block}{Reimplementando el head}
Podemos pensar ahora cómo utilizar el tipo vector para realizar una
nueva implementación del \cf{head}
\end{block}

\pause

\begin{block}{head en Agda utilizando vectores}
    \cf{head} : \{A : \ct{Set}\} \{n : $\N$\} $\ra$ \ct{Vec} A (\cc{suc} n) $\ra$ A \\
    \pause
    \cf{head} (x \cc{$::$} xs) = x
\end{block}

\pause

\begin{block}{}
¿Donde quedó el caso de pattern matching para la lista vacia, \cc{$[]$}?
\end{block}

\end{frame}

\begin{frame}

  \begin{block}{}
  Aprovechando la implementación de los vectores podemos implementar distintas
  funciones nuevas.
  \end{block}

  \pause

  \begin{block}{}
  Recordemos la función \cf{filter}:
  \end{block}

  \begin{exampleblock}{función filter}
    \cf{filter} toma una colección de elementos $c$ de algún tipo A y un predicado sobre A, y retorna
    una colección con los elementos de $c$ que satisfacen el predicado.
  \end{exampleblock}

  \pause
  
  \begin{block}{}
    Queremos implementar \cf{filter} sobre el tipo de los vectores. Primero definamos una función
    que retorne la cantidad de elementos que satisfacen el predicado:
  \end{block}
  
\end{frame}

\begin{frame}

  \begin{block}{$\#$-filter}\small

  \cf{$\#$-filter} : \{A : \ct{Set}\} \{n : $\N$\} $\ra$ (A $\ra$ \ct{Bool}) $\ra$ \ct{Vec} A n $\ra$ $\N$\\
  \cf{$\#$-filter} p \cc{$[]$} $=$ \cc{zero}\\
  \cf{$\#$-filter} p (x \cc{$::$} xs) \ck{with} p x\\
  $\ldots$ $|$ \cc{true}  $=$ \cc{suc} (\cf{$\#$-filter} p xs)\\
  $\ldots$ $|$ \cc{false} $=$ \cf{$\#$-filter} p xs
  \end{block}
  
  \pause
  
  \begin{block}{}
    Luego podemos definir el filter:
  \end{block}

  \pause

  \begin{block}{Filter}\small

  \cf{filter} : \{A : \ct{Set}\} \{n : $\N$\} $\ra$\\
  \ \ \ \ \ \ \ \ \ (p : A $\ra$ \ct{Bool}) $\ra$ (xs : \ct{Vec} A n) $\ra$ \ct{Vec} A (\cf{$\#$-filter} p xs)\\
  \cf{filter} p \cc{$[]$} $=$ \cc{$[]$}\\
  \cf{filter} p (x \cc{$::$} xs) \ck{with} p x\\
  $\ldots$ $|$ \cc{true}  $=$ x \cc{$::$} (\cf{filter} p xs)\\
  $\ldots$ $|$ \cc{false} $=$ \cf{filter} p xs

  \end{block}

\end{frame}

\begin{frame}

\begin{block}{}
Ahora bien, se puede ver que calcular \cf{$\#$-filter} y \cf{filter} se
podría hacer al mismo tiempo. Solo necesitamos un tipo lo suficientemente
expresivo para poder construir valores, veamos como los pares dependientes
nos permiten realizar una implementación mejorada.
\end{block}

\pause

\begin{block}{Pares dependientes}\small

Constructor del tipo:\\ 
Dados tipos A : \ct{Set}, B : A $\ra$ \ct{Set} podemos construir el tipo
\ct{$\Sigma$[} x \ct{$\in$} A \ct{]} B\\
Constructor de valores: \cc{\_$,$\_}\\
Eliminadores: \\
\T - \cf{proj$_1$} : \ct{$\Sigma$[} x \ct{$\in$} A \ct{]} B $\ra$ A\\
\T - \cf{proj$_2$} : \ct{$\Sigma$[} x \ct{$\in$} A \ct{]} B $\ra$ B x\\

\end{block}

\pause

\begin{block}{}
 A este tipo también se lo puede escribir \ct{$\exists$} ($\lambda$ x $\ra$ B x)
\end{block}


\end{frame}

\begin{frame}

\begin{block}{Filter mejorado}\small

\cf{filterImproved} : \{A : \ct{Set}\} \{n : $\N$\} $\ra$\\
\T \T \T \T \ \ (A $\ra$ \ct{Bool}) $\ra$ (\ct{Vec} A n) $\ra$ \ct{$\exists$} ($\lambda$ m $\ra$ \ct{Vec} A m)\\
\pause
\cf{filterImproved} p \cc{$[]$} $=$ (\cc{zero} \cc{$,$} \cc{$[]$})\\
\cf{filterImproved} p (x \cc{$::$} xs) \ck{with} p x\\
$\ldots$ $|$ \cc{false} $=$ \cf{filterImproved} p xs\\
$\ldots$ $|$ \cc{true} $=$ \ck{let} (n' \cc{$,$} xs') $=$ \cf{filterImproved} p xs\\
\T \T \T  \ \ck{in} (\cc{suc} n' \cc{$,$} x \cc{$::$} xs')

\end{block}

\end{frame}


\begin{frame}

\begin{block}{}
  ¿Podremos especificar alguna propiedad más en el tipo resultante?
\end{block}

\pause

  \begin{block}{}
    Redefinamos el tipo del filter, agregando una ``postcondición'' más: El tamaño
    del vector resultante debe tener a lo sumo tantos elementos como el original
  \end{block}
  
  \pause

  \begin{block}{filter mejorado y con prueba}

  \cf{filterImproved'} : \{A : \ct{Set}\} \{n : $\N$\} $\ra$
  (A $\ra$ \ct{Bool}) $\ra$ (\ct{Vec} A n) $\ra$\\
  \T \T \T \T \ \ 
  \ct{$\exists$} ($\lambda$ m $\ra$ \ct{Vec} A m \ct{$\times$} m \ct{$\leq$} n)\\
  \pause
  \cf{filterImproved'} p \cc{$[]$} $=$ (\cc{zero} \cc{$,$} \cc{$[]$} \cc{$,$} \cc{z$\leq$n})\\
  \cf{filterImproved'} p (x \cc{$::$} xs) \ck{with} p x $|$ \cf{filterImproved'} p xs\\
  $\ldots$ $|$ \cc{false} $|$ (n' \cc{$,$} xs' \cc{$,$} m$\leq$n) = 
  (n' \cc{$,$} xs' \cc{$,$} \cf{prop$\leq$} m$\leq$n)\\
  $\ldots$ $|$ \cc{true}  $|$ (n' \cc{$,$} xs' \cc{$,$} m$\leq$n) = 
  (\cc{suc} n' , x \cc{$::$} xs' , \cc{s$\leq$s} m$\leq$n)

  \end{block}
  
\end{frame}

\begin{frame}

\begin{block}{}
  Creemos que esta implementación es correcta, pero el tipo de la función no asegura que cumpla
  con la especificación que detallamos.
  
  Podemos redefinirla con el siguiente tipo:
\end{block}

\begin{block}{Filter con especificación}
  Lo mostramos en Agda.
\end{block}

\end{frame}

\end{document}