\subsection{Universes}

The second programming technique we will look at that is not available in
non-dependently typed languages is {\em universe construction}.  First the
module header.

\begin{code}
module Universes where
\end{code}

A universe is a set of types (or type formers) and a universe construction
consists of a type of codes and a decoding function mapping codes to types
in the universe. The purpose of a universe construction is to be able to
define functions over the types of the universe by inspecting their
codes. In fact we have seen an example of a universe construction already.

\subsubsection{A familiar universe}

The universe of decidable propositions consists of the singleton type
\verb!True! and the empty type \verb!False!. Codes are booleans and the
decoder is the \verb!isTrue! function.

\begin{code}
data   False : Set where
record True  : Set where

data Bool : Set where
  true  : Bool
  false : Bool

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False
\end{code}

Now functions over decidable propositions can be defined by manipulating
the boolean codes. For instance, we can define negation and conjunction as
functions on codes and prove some properties of the corresponding
propositions.

\begin{code}
infix  30 not_
infixr 25 _and_

not_ : Bool -> Bool
not true  = false
not false = true

_and_ : Bool -> Bool -> Bool
true  and x = x
false and _ = false

notNotId : (a : Bool) -> isTrue (not not a) -> isTrue a
notNotId true  p = p
notNotId false ()

andIntro : (a b : Bool) -> isTrue a -> isTrue b -> isTrue (a and b)
andIntro true  _ _  p = p
andIntro false _ () _
\end{code}

A nice property of this universe is that proofs of \verb!True! can be found
automatically. This means that if you have a function taking a proof of a
precondition as an argument, where you expect the precondition to be
trivially true at the point where you are calling the function, you can
make the precondition an implicit argument. For instance, if you expect to
mostly divide by concrete numbers, division of natural numbers can be given
the type signature
\begin{code}
open import Data.Nat

nonZero : Nat -> Bool
nonZero zero    = false
nonZero (suc _) = true

postulate _div_ : Nat -> (m : Nat){p : isTrue (nonZero m)} -> Nat

three = 16 div 5
\end{code}
Here the proof obligation \verb!isTrue (nonZero 5)! will reduce to
\verb!True! and solved automatically by the type checker. Note that if you
tell the type checker that you have defined the type of natural numbers,
you are allowed to use natural number literals like \verb!16! and
\verb!5!. This has been done in the library.

\subsubsection{Universes for generic programming}

Generic programming deals with the problem of defining functions
generically over a set of types. We can achieve this by defining a universe
for the set of types we are interested in. Here is a simple example of how
to program generically over the set of types computed by fixed points over
polynomial functors.

First we define a type of codes for polynomial functors.
\begin{code}
data Functor : Set1 where
  |Id|  : Functor
  |K|   : Set -> Functor
  _|+|_ : Functor -> Functor -> Functor
  _|x|_ : Functor -> Functor -> Functor
\end{code}
A polynomial functor is either the identity functor, a constant functor,
the disjoint union of two functors, or the cartesian product of two
functors. Since codes for functors can contain arbitrary \verb!Set!s (in the case
of the constant functor) the type of codes cannot itself be a \verb!Set!,
but lives in \verb!Set1!.

Before defining the decoding function for functors we define datatypes for
disjoint union and cartesian product.
\begin{code}
data _⊕_ (A B : Set) : Set where
  inl : A -> A ⊕ B
  inr : B -> A ⊕ B

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

infixr 50 _|+|_ _⊕_
infixr 60 _|x|_ _×_
\end{code}

The decoding function takes a code for a functor to a function on
\verb!Set!s and is computed recursively over the code.

\begin{code}
[_] : Functor -> Set -> Set
[ |Id|    ] X = X
[ |K| A   ] X = A
[ F |+| G ] X = [ F ] X ⊕ [ G ] X
[ F |x| G ] X = [ F ] X × [ G ] X
\end{code}

Since it's called a functor it ought to support a map operation. We can
define this by recursion over the code.

\begin{code}
map : (F : Functor){X Y : Set} -> (X -> Y) -> [ F ] X -> [ F ] Y
map |Id|      f x       = f x
map (|K| A)   f c       = c
map (F |+| G) f (inl x) = inl (map F f x)
map (F |+| G) f (inr y) = inr (map G f y)
map (F |x| G) f (x , y) = map F f x , map G f y
\end{code}

Next we define the least fixed point of a polynomial functor.

\begin{code}
data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) -> μ F
\end{code}

To ensure termination, recursive datatypes must be strictly positive and
this is checked by the type checker. Our definition of least fixed point
goes through, since the type checker can spot that \verb![_]! is strictly
positive in its second argument.

With this definition we can define a generic fold operation on least fixed
points. Grabbing for the closest category theory text book we might try
something like this
\begin{code}
-- fold : (F : Functor){A : Set} -> ([ F ] A -> A) -> μ F -> A
-- fold F φ < x > = φ (map F (fold F φ) x)
\end{code}
Unfortunately, this definition does not pass the termination checker since
the recursive call to \verb!fold! is passed to the higher order function
\verb!map! and the termination checker cannot see that \verb!map! isn't
applying it to bad things. 

To make \verb!fold! pass the termination checker we can fuse \verb!map! and
\verb!fold! into a single function
\verb!mapFold F G φ x = map F (fold G φ) x! defined recursively over
\verb!x!. We need to keep two copies of the functor since \verb!fold! is
always called on the same functor, whereas \verb!map! is defined by taking
its functor argument apart.
\begin{code}
mapFold : forall {X} F G -> ([ G ] X -> X) -> [ F ] (μ G) -> [ F ] X
mapFold |Id|        G φ < x >   = φ (mapFold G G φ x)
mapFold (|K| A)     G φ c       = c
mapFold (F₁ |+| F₂) G φ (inl x) = inl (mapFold F₁ G φ x)
mapFold (F₁ |+| F₂) G φ (inr y) = inr (mapFold F₂ G φ y)
mapFold (F₁ |x| F₂) G φ (x , y) = mapFold F₁ G φ x , mapFold F₂ G φ y

fold : {F : Functor}{A : Set} -> ([ F ] A -> A) -> μ F -> A
fold {F} φ < x > = φ (mapFold F F φ x)
\end{code}

There is a lot more fun to be had here, but let us make do with a couple of
examples. Both natural numbers and lists are examples of least fixed points
of polynomial functors:

\begin{code}
NatF = |K| True |+| |Id|
NAT  = μ NatF

Z : NAT
Z = < inl _ >

S : NAT -> NAT
S n = < inr n >

ListF = \A -> |K| True |+| |K| A |x| |Id|
LIST  = \A -> μ (ListF A)

nil : {A : Set} -> LIST A
nil = < inl _ >

cons : {A : Set} -> A -> LIST A -> LIST A
cons x xs = < inr (x , xs) >
\end{code}

To make implementing the argument to fold easier we introduce a few helper
functions:
%
\begin{code}
[_||_] : {A B C : Set} -> (A -> C) -> (B -> C) -> A ⊕ B -> C
[ f || g ] (inl x) = f x
[ f || g ] (inr y) = g y

uncurry : {A B C : Set} -> (A -> B -> C) -> A × B -> C
uncurry f (x , y) = f x y

const : {A B : Set} -> A -> B -> A
const x y = x
\end{code}
%
Finally some familiar functions expressed as folds.
%
\begin{code}
foldr : {A B : Set} -> (A -> B -> B) -> B -> LIST A -> B
foldr {A}{B} f z = fold [ const z || uncurry f ]

plus : NAT -> NAT -> NAT
plus n m = fold [ const m || S ] n
\end{code}

\subsubsection{Universes for overloading}

At the moment, Agda does not have a class system like the one in
Haskell. However, a limited form of overloading can be achieved using
universes. The idea is simply if you know in advance at which types you
want to overload a function, you can construct a universe for these types
and define the overloaded function by pattern matching on a code.

A simple example: suppose we want to overload equality for some of our
standard types. We start by defining our universe:

\begin{code}
open import Data.List

data Type : Set where
  bool : Type
  nat  : Type
  list : Type -> Type
  pair : Type -> Type -> Type

El : Type -> Set
El nat        = Nat
El bool       = Bool
El (list a)   = List (El a)
El (pair a b) = El a × El b
\end{code}

In order to achieve proper overloading it is important that we don't have
to supply the code explicitly everytime we are calling the overloaded
function. In this case we won't have to since the decoding function
computes distinct datatypes in each clause. This means that the type checker
can figure out a code from its decoding. For instance, the only code that
can decode into \verb!Bool! is \verb!bool!, and if the decoding of a code
is a product type then the code must be \verb!pair! of some codes.

Now an overloaded equality function simply takes an implicit code and
computes a boolean relation over the semantics of the code.

\begin{code}
infix 30 _==_
_==_ : {a : Type} -> El a -> El a -> Bool

_==_ {nat} zero    zero    = true
_==_ {nat} (suc _) zero    = false
_==_ {nat} zero    (suc _) = false
_==_ {nat} (suc n) (suc m) = n == m

_==_ {bool} true  x = x
_==_ {bool} false x = not x

_==_ {list a} [] []       = true
_==_ {list a} (_ :: _) [] = false
_==_ {list a} [] (_ :: _) = false
_==_ {list a} (x :: xs) (y :: ys) = x == y and xs == ys

_==_ {pair a b} (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ and y₁ == y₂
\end{code}

In the recursive calls of \verb!_==_! the code argument is inferred
automatically. The same happens when we use our equality function on
concrete examples:

\begin{code}
example₁ : isTrue (2 + 2 == 4)
example₁ = _

example₂ : isTrue (not (true :: false :: [] == true :: true :: []))
example₂ = _
\end{code}

In summary, universe constructions allows us to define functions by pattern
matching on (codes for) types. We have seen a few simple examples, but
there are a lot of other interesting possibilities. For example
\begin{itemize}
\item XML schemas as codes for the types of well-formed XML documents,
\item a universe of tables in a relational database, allowing us to
      make queries which are guaranteed to be well-typed
\end{itemize}