\subsection{Views} \label{Views} As we have seen pattern matching in Agda can reveal information not only about the term being matched but also about terms occurring in the type of this term. For instance, matching a proof of \verb!x == y! against the \verb!refl! constructor we (and the type checker) will learn that \verb!x! and \verb!y! are the same. We can exploit this, and design datatypes whose sole purpose is to tell us something interesting about its indices. We call such a datatype a {\em view}~\cite{mcbride:left}. To use the view we define a view function, computing an element of the view for arbitrary indices. This section on views is defined in the file {\tt Views.lagda} so here is the top-level module declaration: \begin{code} module Views where \end{code} \subsubsection{Natural number parity} Let us start with an example. We all know that any natural number $n$ can be written on the form $2k$ or $2k + 1$ for some $k$. Here is a view datatype expressing that. We use the natural numbers defined in the summer school library module \verb!Data.Nat!. \begin{code} open import Data.Nat data Parity : Nat -> Set where even : (k : Nat) -> Parity (k * 2) odd : (k : Nat) -> Parity (1 + k * 2) \end{code} An element of \verb!Parity n! tells you if \verb!n! is even or odd, i.e. if $n = 2k$ or $n = 2k + 1$, and in each case what $k$ is. The reason for writing \verb!k * 2! and \verb!1 + k * 2! rather than \verb!2 * k! and \verb!2 * k + 1! has to do with the fact that \verb!_+_! and \verb!_*_! are defined by recursion over their first argument. This way around we get a better reduction behaviour. Now, just defining the view datatype isn't very helpful. We also need to show that any natural number can be viewed in this way. In other words, that given an arbitrary natural number \verb!n! we can to compute an element of \verb!Parity n!. \begin{code} parity : (n : Nat) -> Parity n parity zero = even zero parity (suc n) with parity n parity (suc .(k * 2)) | even k = odd k parity (suc .(1 + k * 2)) | odd k = even (suc k) \end{code} In the \verb!suc n! case we use the view recursively to find out the parity of \verb!n!. If \verb!n = k * 2! then \verb!suc n = 1 + k * 2! and if \verb!n = 1 + k * 2! then \verb!suc n = suc k * 2!. In effect, this view gives us the ability to pattern match on a natural number with the patterns \verb!k * 2! and \verb!1 + k * 2!. Using this ability, defining the function that divides a natural number by two is more or less trivial: \begin{code} half : Nat -> Nat half n with parity n half .(k * 2) | even k = k half .(1 + k * 2) | odd k = k \end{code} Note that \verb!k! is bound in the pattern for the view, not in the dotted pattern for the natural number. \subsubsection{Finding an element in a list} Let us turn our attention to lists. First some imports: we will use the definitions of lists and booleans from the summer school library. \begin{code} open import Data.Function open import Data.List open import Data.Bool \end{code} Now, given a predicate \verb!P! and a list \verb!xs! we can define what it means for \verb!P! to hold for all elements of \verb!xs!: \begin{code} infixr 30 _:all:_ data All {A : Set}(P : A -> Set) : List A -> Set where all[] : All P [] _:all:_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs) \end{code} A proof of \verb!All P xs! is simply a list of proofs of \verb!P x! for each element \verb!x! of \verb!xs!. Note that \verb!P! does not have to be a decidable predicate. To turn a decidable predicate into a general predicate we define a function \verb!satisfies!. \begin{fakecode} satisfies : {A : Set} -> (A -> Bool) -> A -> Set satisfies p x = isTrue (p x) \end{fakecode} Using the \verb!All! datatype we could prove the second part of the correctness of the \verb!filter! function, namely that all the elements of the result of \verb!filter! satisfies the predicate: \verb!All (Sat p) (filter p xs)!. This is left as an exercise. Instead, let us define some interesting views on lists. Given a decidable predicate on the elements of a list, we can either find an element in the list that satisfies the predicate, or else all elements satifies the negation of the predicate. Here is the corresponding view datatype: \begin{code} data Find {A : Set}(p : A -> Bool) : List A -> Set where found : (xs : List A)(y : A) -> satisfies p y -> (ys : List A) -> Find p (xs ++ y :: ys) not-found : forall {xs} -> All (satisfies (not ∘ p)) xs -> Find p xs \end{code} We don't specify which element to use as a witness in the \verb!found! case. If we wanted the view to always return the first (or last) matching element we could force the elements of \verb!xs! (or \verb!ys!) to satisfy the negation of \verb!p!. To complete the view we need to define the view function computing an element of \verb!Find p xs! for any \verb!p! and \verb!xs!. Here is a first attempt: \begin{code} find₁ : {A : Set}(p : A -> Bool)(xs : List A) -> Find p xs find₁ p [] = not-found all[] find₁ p (x :: xs) with p x ... | true = found [] x {! !} xs ... | false = {! !} \end{code} In the case where \verb!p x! is \verb!true! we want to return \verb!found! (hence, returning the first match), but there is a problem. The type of the hole (\verb+{+\verb+! !+\verb+}+) is \verb!isTrue (p x)!, even though we already matched on \verb!p x! and found out that it was \verb!true!. The problem is that when we abstracted over \verb!p x! we didn't know that we wanted to use the \verb!found! constructor, so there were no \verb!p x! to abstract over. Remember that \verb!with! doesn't remember the connection between the with-term and the patterns. One solution to this problem is to make this connection explicit with a proof object. The idea is to not abstract over the term itself but rather over an arbitrary term of the same type and a proof that it is equal to the original term. Remember the type of equality proofs: \begin{code} data _==_ {A : Set}(x : A) : A -> Set where refl : x == x \end{code} Now we define the type of elements of a type \verb!A! together with proofs that they are equal to some given \verb!x! in \verb!A!. % \begin{code} data Inspect {A : Set}(x : A) : Set where it : (y : A) -> x == y -> Inspect x \end{code} % There is one obvious way to construct an element of \verb!Inspect x!, namely to pick \verb!x! as the thing which is equal to \verb!x!. % \begin{code} inspect : {A : Set}(x : A) -> Inspect x inspect x = it x refl \end{code} We can now define \verb!find! by abstracting over \verb!inspect (p x)! rather than \verb!p x! itself. This will provide us with either a proof of \verb!p x == true! or a proof of \verb!p x == false! which we can use in the arguments to \verb!found! and \verb!not-found!. First we need a couple of lemmas about \verb!isTrue! and \verb!isFalse!: \begin{code} trueIsTrue : {x : Bool} -> x == true -> isTrue x trueIsTrue refl = _ falseIsFalse : {x : Bool} -> x == false -> isFalse x falseIsFalse refl = _ \end{code} Now we can define \verb!find! without any problems. \begin{code} find : {A : Set}(p : A -> Bool)(xs : List A) -> Find p xs find p [] = not-found all[] find p (x :: xs) with inspect (p x) ... | it true prf = found [] x (trueIsTrue prf) xs ... | it false prf with find p xs find p (x :: ._) | it false _ | found xs y py ys = found (x :: xs) y py ys find p (x :: xs) | it false prf | not-found npxs = not-found (falseIsFalse prf :all: npxs) \end{code} In the case where \verb!p x! is true, \verb!inspect (p x)! matches \verb!it true prf! where \verb!prf : p x == true!. Using our lemma we can turn this into the proof of \verb!isTrue (p x)! that we need for the third argument of \verb!found!. We get a similar situation when \verb!p x! is false and \verb!find p xs! returns \verb!not-found!. \subsubsection{Indexing into a list} In Sections \ref{Families} and Section \ref{CurryHoward} we saw two ways of safely indexing into a list. In both cases the type system guaranteed that the index didn't point outside the list. However, sometimes we have no control over the value of the index and it might well be that it is pointing outside the list. One solution in this case would be to wrap the result of the lookup function in a maybe type, but maybe types don't really tell you anything very interesting and we can do a lot better. First let us define the type of proofs that an element \verb!x! is in a list \verb!xs!. \begin{code} data _∈_ {A : Set}(x : A) : List A -> Set where hd : forall {xs} -> x ∈ x :: xs tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs \end{code} The first element of a list is a member of the list, and any element of the tail of a list is also an element of the entire list. Given a proof of \verb!x ∈ xs! we can compute the index at which \verb!x! occurs in \verb!xs! simply by counting the number of \verb!tl!s in the proof. \begin{code} index : forall {A}{x : A}{xs} -> x ∈ xs -> Nat index hd = zero index (tl p) = suc (index p) \end{code} Now, let us define a view on natural numbers \verb!n! with respect to a list \verb!xs!. Either \verb!n! indexes some \verb!x! in \verb!xs! in which case it is of the form \verb!index p! for some proof \verb!p : x ∈ xs!, or \verb!n! points outside the list, in which case it is of the form \verb!length xs + m! for some \verb!m!. \begin{code} data Lookup {A : Set}(xs : List A) : Nat -> Set where inside : (x : A)(p : x ∈ xs) -> Lookup xs (index p) outside : (m : Nat) -> Lookup xs (length xs + m) \end{code} In the case that \verb!n! is a valid index we not only get the element at the corresponding position in \verb!xs! but we are guaranteed that this is the element that is returned. There is no way a lookup function could cheat and always return the first element, say. % In the case that \verb!n! is indexing outside the list we also get some more information. We get a proof that \verb!n! is out of bounds and we also get to know by how much. Defining the lookup function is no more difficult than it would have been to define the lookup function returning a maybe. \begin{code} _!_ : {A : Set}(xs : List A)(n : Nat) -> Lookup xs n [] ! n = outside n (x :: xs) ! zero = inside x hd (x :: xs) ! suc n with xs ! n (x :: xs) ! suc .(index p) | inside y p = inside y (tl p) (x :: xs) ! suc .(length xs + n) | outside n = outside n \end{code} \subsubsection{A type checker for $\lambda$-calculus} To conclude this section on views, let us look at a somewhat bigger example: a type checker for simply typed $λ$-calculus. This example is due to Conor McBride~\cite{mcbride:left} and was first implemented in Epigram. His version not only guaranteed that when the type checker said ok things were really ok, but also provided a detailed explanation in the case where type checking failed. We will focus on the positive side here and leave the reporting of sensible and guaranteed precise error message as an exercise. First, let us define the type language. We have one base type \verb!ı! and a function type. \begin{code} infixr 30 _→_ data Type : Set where ı : Type _→_ : Type -> Type -> Type \end{code} When doing type checking we will inevitably have to compare types for equality, so let us define a view. \begin{code} data Equal? : Type -> Type -> Set where yes : forall {τ} -> Equal? τ τ no : forall {σ τ} -> Equal? σ τ _=?=_ : (σ τ : Type) -> Equal? σ τ ı =?= ı = yes ı =?= (_ → _) = no (_ → _) =?= ı = no (σ₁ → τ₁) =?= (σ₂ → τ₂) with σ₁ =?= σ₂ | τ₁ =?= τ₂ (σ → τ) =?= (.σ → .τ) | yes | yes = yes (σ₁ → τ₁) =?= (σ₂ → τ₂) | _ | _ = no \end{code} Note that we don't give any justification in the \verb!no! case. The \verb!_=?=_! could return \verb!no! all the time without complaints from the type checker. In the \verb!yes! case, however, we guarantee that the two types are identical. Next up we define the type of raw lambda terms. We use unchecked deBruijn indices to represent variables. \begin{code} infixl 80 _$_ data Raw : Set where var : Nat -> Raw _$_ : Raw -> Raw -> Raw lam : Type -> Raw -> Raw \end{code} We use Church style terms in order to simplify type inference. The idea with our type checker is that it should take a raw term and return a well-typed term, so we need to define the type of well-typed $λ$-terms with respect to a context $Γ$ and a type $τ$. \begin{code} Cxt = List Type data Term (Γ : Cxt) : Type -> Set where var : forall {τ} -> τ ∈ Γ -> Term Γ τ _$_ : forall {σ τ} -> Term Γ (σ → τ) -> Term Γ σ -> Term Γ τ lam : forall σ {τ} -> Term (σ :: Γ) τ -> Term Γ (σ → τ) \end{code} We represent variables by proofs that a type is in the context. Remember that the proofs of list membership provide us with an index into the list where the element can be found. Given a well-typed term we can erase all the type information and get a raw term. \begin{code} erase : forall {Γ τ} -> Term Γ τ -> Raw erase (var x) = var (index x) erase (t$ u) = erase t $erase u erase (lam σ t) = lam σ (erase t) \end{code} In the variable case we turn the proof into a natural number using the \verb!index! function. Now we are ready to define the view of a raw term as either being the erasure of a well-typed term or not. Again, we don't provide any justification for giving a negative result. Since, we are doing type inference the type is not a parameter of the view but computed by the view function. \begin{code} data Infer (Γ : Cxt) : Raw -> Set where ok : (τ : Type)(t : Term Γ τ) -> Infer Γ (erase t) bad : {e : Raw} -> Infer Γ e \end{code} The view function is the type inference function taking a raw term and computing an element of the \verb!Infer! view. \begin{code} infer : (Γ : Cxt)(e : Raw) -> Infer Γ e \end{code} Let us walk through the three cases: variable, application, and lambda abstraction. \begin{code} infer Γ (var n) with Γ ! n infer Γ (var .(length Γ + n)) | outside n = bad infer Γ (var .(index x)) | inside σ x = ok σ (var x) \end{code} In the variable case we need to take case of the fact that the raw variable might be out of scope. We can use the lookup function \verb+_!_+ we defined above for that. When the variable is in scope the lookup function provides us with the type of the variable and the proof that it is in scope. \begin{code} infer Γ (e₁$ e₂) with infer Γ e₁ infer Γ (e₁ $e₂) | bad = bad infer Γ (.(erase t₁)$ e₂) | ok ı t₁ = bad infer Γ (.(erase t₁) $e₂) | ok (σ → τ) t₁ with infer Γ e₂ infer Γ (.(erase t₁)$ e₂) | ok (σ → τ) t₁ | bad = bad infer Γ (.(erase t₁) $.(erase t₂)) | ok (σ → τ) t₁ | ok σ' t₂ with σ =?= σ' infer Γ (.(erase t₁)$ .(erase t₂)) | ok (σ → τ) t₁ | ok .σ t₂ | yes = ok τ (t₁ $t₂) infer Γ (.(erase t₁)$ .(erase t₂)) | ok (σ → τ) t₁ | ok σ' t₂ | no = bad \end{code} The application case is the bulkiest simply because there are a lot of things we need to check: that the two terms are type correct, that the first term has a function type and that the type of the second term matches the argument type of the first term. This is all done by pattern matching on recursive calls to the \verb!infer! view and the type equality view. \begin{code} infer Γ (lam σ e) with infer (σ :: Γ) e infer Γ (lam σ .(erase t)) | ok τ t = ok (σ → τ) (lam σ t) infer Γ (lam σ e) | bad = bad \end{code} Finally, the lambda case is very simple. If the body of the lambda is type correct in the extended context, then the lambda is well-typed with the corresponding function type. Without much effort we have defined a type checker for simply typed $λ$-calculus that not only is guaranteed to compute well-typed terms, but also guarantees that the erasure of the well-typed term is the term you started with.