Commit f67508ab authored by Nicola Botta's avatar Nicola Botta
Browse files

Added L3 and L4.

parent 29186c84
% -*-Latex-*-
%if False
> module Lecture3
> import Syntax.PreorderReasoning
> %default total
> %auto_implicits on
> %access public export
> Real : Type
> Real = Double
> cong2 : {a1, a2 : a} -> {b1, b2 : b} -> {f : a -> b -> c} ->
>
> (a1 = a2) -> (b1 = b2) -> f a1 b1 = f a2 b2
>
> cong2 Refl Refl = Refl
%endif
\begin{frame}
\frametitle{Objectives}
\begin{itemize}
\vfill
\item<1-> Learn the basics of \hl<1>{dependent} \hl<1>{types} and \hl<2>{verified} \hl<2>{programming}.
\end{itemize}
\vfill
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris and Haskell}
%
\begin{itemize}
\vfill
\item<2-> Haskell, Agda, Idris, Coq are all \hl<2>{functional} programming languages.
\vfill
\item<3-> \hl<3>{Idris} and Agda are very similar to \hl<3>{Haskell}.
\vfill
\item<4-> In Idris, one can introduce \hl<4>{type} \hl<4>{synonyms} \dots
> Pos : Type
> Pos = (Int, Int)
> Pair : Type -> Type
> Pair a = (a, a)
\vfill
\item<5-> \dots completely \hl<5>{new} \hl<5>{types} \dots
> data HL = H | L
>
> data Shape = Circle Real | Rect Real Real
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Haskell and Idris}
%
\begin{itemize}
\vfill
\item<1-> \dots and \hl<1>{recursive} data types:
< data List : Type -> Type where
< Nil : List a
< (::) : a -> List a -> List a
<
\vfill
\item<2-> Notice the \hl<2>{explicit} declaration of the type of |List|
< IRP :t List
< List : Type -> Type
\vfill
\item<3-> and the role of \hl<3>{|:|} and \hl<3>{|::|} in Idris
< IRP :t (True :: (False :: Nil))
< [True, False] : List Bool
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: vectors}
%
\begin{itemize}
\vfill
\item<2-> Idris (and Agda, Coq) support \hl<2>{dependent} \hl<2>{types}.
\vfill
\item<3-> Dependent types are types that depend on \hl<3>{values}:
< data Vect : Nat -> Type -> Type where
< Nil : Vect Z a
< (::) : a -> Vect n a -> Vect (S n) a
\vfill
\item<4-> The syntax is an abbreviation for
> data Vect : Nat -> Type -> Type where
> Nil : {a : Type} -> Vect Z a
> (::) : {a : Type} -> {n : Nat} ->
> a -> Vect n a -> Vect (S n) a
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: vectors}
%
\begin{itemize}
\vfill
\item<1-> The \hl<1>{length} is \hl<1>{encoded} in the \hl<1>{type} and can be exploited to
implement \hl<1>{safe} operations \dots
< head : Vect (S n) a -> a
< head (x :: xs) = x
< tail : Vect (S n) a -> Vect n a
< tail (x :: xs) = xs
\vfill
\item<2-> \dots without the need to return \hl<2>{|Maybe|} values.
\vfill
\item<3-> The Idris type checker recognizes that the case |head Nil|
is \hl<3>{impossible} and that |head| is \hl<3>{total}.
\vfill
\item<4-> \sh{Exercise 3.1}: define concatenation and a safe |zip| for vectors.
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
%if False
\begin{frame}[fragile]
\frametitle{Idris: vectors}
%
\begin{itemize}
\vfill
\item<1-> \sh{Exercise 3.1:}
> concat : Vect m a -> Vect n a -> Vect (m + n) a
> concat {m = Z} Nil ys = ys
> concat {m = S l} (x :: xs) ys = x :: concat xs ys
> zip : Vect m a -> Vect m b -> Vect m (a, b)
> zip {m = Z} Nil Nil = Nil
> zip {m = S l} (x :: xs) (y :: ys) = (x, y) :: zip xs ys
\end{itemize}
\vfill
%
\end{frame}
%endif
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: types as specifications}
%
\begin{itemize}
\vfill
\item<1-> The definitions
< head : Vect (S n) a -> a
< head (x :: xs) = x
<
< tail : Vect (S n) a -> Vect n a
< tail (x :: xs) = xs
are abbreviations for
> head : {a : Type} -> {n : Nat} -> Vect (S n) a -> a
> head (x :: xs) = x
>
> tail : {a : Type} -> {n : Nat} -> Vect (S n) a -> Vect n a
> tail (x :: xs) = xs
\vfill
\item<2-> Learn to read \hl<2>{type} \hl<2>{declarations} as \hl<2>{program} \hl<2>{specifications}:
\pause \pause \hl<3>{|∀ ! n : Nat|}, \hl<4>{|∀ ! a : Type|}, \hl<5>{|∀ ! xs : Vect (S n) a|}, \hl<6>{\textbf{Compute}} \hl<6>{|tail xs : Vect n a|}.
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: types as specifications}
%
\begin{itemize}
\vfill
\item<1-> This is also the most verbose way of writing the type of |tail|:
< tail : {a : Type} -> {n : Nat} -> (xs : Vect (S n) a) ->
< Vect n a
\vfill
\item<2-> The difference between the arguments \hl<2>{|a|}, \hl<2>{|n|} and \hl<2>{|xs|} is that
the first two are \hl<2>{implicit} and the third one is \hl<2>{explicit}.
\vfill
\item<3-> Notice that the type of |tail {a} {n} xs| depends on |a| and
|n| but not on |xs|.
\vfill
\item<4-> In dependently typed programming, the notions of \hl<4>{value}
and of \hl<4>{type} become less distinct: |a| is a (value of type)
|Type|, |n| is a |Nat| and |Vect n a| is a |Type|!
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: equality}
%
\begin{itemize}
\vfill
\item<2-> Many predefined Idris types come with equality \hl<2>{tests}:
< IRP 2 + 1 == 3
< True : Bool
<
< IRP [1,2,3] == [2,1,3]
< False : Bool
\vfill
\item<3-> But Idris also has a built-in data type for
\hl<3>{definitional} \hl<3>{equality}:
< data (=) : {A, B : Type} -> A -> B -> Type where
<
< Refl : x = x
\vfill
\item<4-> We can apply it to \hl<4>{prove} boring identities \dots
> eq1 : 1 = 1
> eq1 = Refl
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: equality}
%
\begin{itemize}
\vfill
\item<1-> \dots \hl<1>{postulate} non-provable equalities \dots
> postulate eq2 : 1 = 0
\vfill
\item<2-> \dots but also prove \hl<2>{properties} of programs:
> eq3 : (v : Vect (S n) a) -> (head v :: tail v) = v
> eq3 (x :: xs) = Refl
\vfill
\item<3-> The Idris type checker applies built-in \hl<3>{rules} (like
|f = \ x => f x|) and all the \hl<3>{definitions} available (so far) in a
program to \hl<3>{reduce} the LHS and the RHS of equality types to identical
expressions!
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: equality}
%
\begin{itemize}
\vfill
\item<1-> Sometimes the type checker does all the work:
> eq4 : (n : Nat) -> Z + n = n
> eq4 n = Refl
\vfill
\item<2-> Sometimes it needs some help:
%format whatNow = "\hl{whatNow}"
> eq5 : (n : Nat) -> n + Z = n
> eq5 Z = Refl
> eq5 (S m) = ( S m + Z )
> ={ Refl }=
> ( S (m + Z) )
> ={ cong (eq5 m) }=
> ( S m )
> QED
\vfill
\item<3-> Let's have a look at Lecture3.lidr!
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: Negation, logical impossibility}
%
\begin{itemize}
\vfill
\item<1-> We cannot implement a proof that 1 = 0, but we can
show that this equality does \hl<1>{not} hold:
> neq1 : Not (1 = 0)
> neq1 Refl impossible
\vfill
\item<2-> Here |Not| is the function \dots
< Not : Type -> Type
< Not A = A -> Void
\vfill
\item<3-> \dots and |Void| (\hl<3>{|Bot|}) is a type with no constructors:
< data Void : Type where
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: Negation, logical impossibility}
%
\begin{itemize}
\vfill
\item<1-> Idris provides a built-in rule for "ex falso sequitur quodlibet":
< void : Void -> a
\vfill
\item<2-> Thus, if we have a (value of type) |T| and a |Not T|, we can
prove everything:
%if False
> T : Type
%endif
> t : T
> nt : Not T
>
> nneq1 : 1 = 0
> nneq1 = void (nt t)
\vfill
\item<3-> Here |T| is an arbitrary type:
< T : Type
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: Negation, logical impossibility}
%
\begin{itemize}
\vfill
\item<1-> Back to the implementation of |neq1|:
< neq1 : Not (1 = 0)
< neq1 Refl impossible
\vfill
\item<2-> |impossible| is an Idris keyword like |where|, |let|, |data|, etc.
\vfill
\item<3-> It recognizes an \hl<3>{impossible} \hl<3>{pattern} \hl<3>{matching} and
return a value of type |Not (1 = 0)| that is |(1 = 0) -> Void|.
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: Properties, propositions}
%
\begin{itemize}
\vfill
\item<2-> We can apply \hl<2>{equality} \hl<2>{types} to express what it means for a
function to be \hl<2>{injective}:
> Injective : (a -> b) -> Type
> Injective {a} f = (x, y : a) -> f x = f y -> x = y
\vfill
\item<3-> \sh{Exercise 3.2:} remember the notion of \hl<3>{optimality} of
policies from lecture 2: |p : X -> Y| \textbf{optimal} w.r.t. |val : X
-> Y -> Nat| iff |∀ ! x : X|, |∀ ! y : Y|, \ |val x y ≤ val x (p
x)|. \pause \pause \pause Assume
> X : Type
> Y : Type
> val : X -> Y -> Real
> (<=) : Real -> Real -> Type
and \hl<4>{implement} an Idris specification of optimality for policies
as a function |Optimal : (X -> Y) -> Type|.
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
%%if False
\begin{frame}[fragile]
\frametitle{Idris: Properties, propositions}
%
\begin{itemize}
\vfill
\item<1-> Exercise 3.2:
> Optimal : (X -> Y) -> Type
> Optimal p = (x : X) -> (y : Y) -> val x y <= val x (p x)
\vfill
\item<2-> For natural numbers, |(<=)| is defined as follows
< data LTE : (n, m : Nat) -> Type where
< LTEZero : LTE Z right
< LTESucc : LTE left right -> LTE (S left) (S right)
\vfill
\item<3-> \sh{Exercise 3.3:} explain the definition of |LTE| (remember the definition of |Nat|).
\end{itemize}
\vfill
%
\end{frame}
%%endif
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: Existential types}
%
\begin{itemize}
\vfill
\item<1-> In mathematical specifications we often find fragments of the
form |∃ ! x ∈ X| \textbf{s.t.} \dots:
\begin{equation*}
\text{|d ∈ Nat| is a \textbf{divisor} of |n ∈ Nat| iff |∃ ! q ∈ Nat|, \textbf{s.t.} |d * q = n|}
\end{equation*}
\vfill
\item<2-> In Idris, we can define a data type that encodes "there exists
an |x| such that |P x| holds" \dots
> data Exists : (X : Type) -> (P : X -> Type) -> Type where
> Evidence : {X : Type} -> {P : X -> Type} ->
> (x : X) -> (px : P x) -> Exists X P
\vfill
\item<3-> \dots specify what it means for a \hl<3>{|d|} to be a \hl<3>{divisor} of an \hl<3>{|n|} \dots
> Divisor : (d : Nat) -> (n : Nat) -> Type
> Divisor d n = Exists Nat (\ q => d * q = n)
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Idris: Existential types}
%
\begin{itemize}
\vfill
\item<1-> \dots and prove that 3 is a divisor of 6:
> threeDivSix : Divisor 3 6
> threeDivSix = Evidence 2 Refl
\vfill
\item<2-> Thus, values of type |Exists X P| are just \hl<2>{pairs} from which we
can take out the \hl<2>{first} (a witness) and the \hl<2>{second} (a proof) element:
< getWitness (Evidence w p) = w
<
< getProof (Evidence w p) = p
\vfill
\item<3-> \sh{Exercise 3.4:} what is the type of \hl<3>{|Refl|} in the
definition of |threeDivSix|? What are the types of \hl<4>{|getWitness|} and \hl<4>{|getProof|}?
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
%if False
\begin{frame}[fragile]
\frametitle{Idris: Properties, propositions}
%
\begin{itemize}
\vfill
\item<1-> Exercise 3.4:
< Refl : 3 * 2 = 6
\vfill
\item<2-> Exercise 3.4:
%if False
> getWitness : {X : Type} -> {P : X -> Type} ->
> Exists X P -> X
> getWitness (Evidence w p) = w
>
> getProof : {X : Type} -> {P : X -> Type} ->
> (e : Exists X P) -> P (getWitness e)
> getProof (Evidence w p) = p
%endif
< getWitness : {X : Type} -> {P : X -> Type} ->
< Exists X P -> X
<
< getProof : {X : Type} -> {P : X -> Type} ->
< (e : Exists X P) -> P (getWitness e)
\end{itemize}
\vfill
%
\end{frame}
%endif
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Specifications and program correctness}
%
\begin{itemize}
\vfill
\item<1-> Dependent types can be applied to implement programs that are
\hl<1>{correct} \hl<1>{by} \hl<1>{construction} or \hl<2>{verified}.
\vfill
\item<3-> This is done in three steps:
\begin{itemize}
\vfill
\item \hl<4>{Specify} a program |P|,
\vfill
\item \hl<5>{Implement} |P|,
\vfill
\item \hl<6>{Prove} that |P| fulfills its specification.
\end{itemize}
\end{itemize}
\vfill
%
\end{frame}
%% -------------------------------------------------------------------
\begin{frame}[fragile]
\frametitle{Example: Specify}
%
\begin{itemize}
\vfill
\item<1-> Given a data type for \hl<1>{binary} \hl<1>{trees} \dots
> data BT : Type -> Type where
> Leaf : a -> BT a
> Branch : BT a -> BT a -> BT a
\vfill
\item<2-> \dots we want to \hl<2>{implement}