\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.