\section{Types and Functions}

\subsection{Primitive Types}

\Idris{} defines several primitive types: \tTC{Int}, \tTC{Integer} and
\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for
text manipulation, and \tTC{Ptr} which represents foreign pointers.
There are also several data types declared in the library, including
\tTC{Bool}, with values \tDC{True} and \tDC{False}.
We can declare some constants with these types. Enter the following
into a file \texttt{prims.idr} and load it into the \Idris{} interactive
environment by typing \texttt{idris prims.idr}:

\begin{SaveVerbatim}{constprims}

module prims

x : Int
x = 42

foo : String
foo = "Sausage machine"

bar : Char
bar = 'Z'

quux : Bool
quux = False

\end{SaveVerbatim}
\useverb{constprims}

\noindent
An \Idris{} file consists of an optional module declaration (here
\texttt{module prims}) followed by an optional list of imports (none here,
however \Idris{} programs can consist of several modules, and the definitions
in each module each have their own namespace, as we will discuss in Section
\ref{sect:namespaces}) and a
collection of declarations and definitions. The order of definitions is
significant --- functions and data types must be defined before use.
Each definition must have a type
declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
Indentation is significant --- a new declaration begins at the same level
of indentation as the preceding declaration. Alternatively, declarations
may be terminated with a semicolon.

A library module \texttt{prelude} is automatically imported by every \Idris{} program,
including facilities for IO, arithmetic, data structures and various common
functions. The prelude defines several arithmetic and comparison operators,
which we can use at the prompt. Evaluating things at the prompt gives an
answer, and the type of the answer. For example:

\begin{SaveVerbatim}{promptprim}

*prims> 6*6+6
42 : Int
*prims> x == 6*6+6
True : Bool

\end{SaveVerbatim}
\useverb{promptprim}

\noindent
All of the usual arithmetic and comparison operators are defined for the primitive
types. They are overloaded using type classes, as we will discuss in Section
\ref{sec:classes} and can be extended to work on user defined types.
Boolean expressions can be tested with the \texttt{if...then...else} construct:

\begin{SaveVerbatim}{ifthenelse}

*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
"The answer!" : String

\end{SaveVerbatim}
\useverb{ifthenelse}

\subsection{Data Types}

Data types are declared in a similar way to Haskell data types, with a similar
syntax. Natural numbers and lists, for example, can be declared as follows:

\begin{SaveVerbatim}{natlist}

data Nat    = O   | S Nat           -- Natural numbers
                                    -- (zero and successor)
data List a = Nil | (::) a (List a) -- Polymorphic lists

\end{SaveVerbatim}
\useverb{natlist}

\noindent
The above declarations are taken from the standard library. Unary natural
numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
the successor of another natural number (\texttt{S k}). 
Lists can either be empty (\texttt{Nil})
or a value added to the front of another list (\texttt{x :: xs}).
In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
such as this can be added using a fixity declaration, as follows:

\begin{SaveVerbatim}{infixcons}

infixr 10 :: 

\end{SaveVerbatim}
\useverb{infixcons}

\noindent
Functions, data constructors and type constuctors may all be given infix
operators as names. They may be used in prefix form if enclosed in brackets,
e.g. \tDC{(::)}. Infix operators can use any of the symbols:

\begin{SaveVerbatim}{infixsyms}

:+-*/=_.?|&><!@$%^~.

\end{SaveVerbatim}
\useverb{infixsyms}

\begin{SaveVerbatim}{argh}
$
\end{SaveVerbatim}

\subsection{Functions}

Functions are implemented by pattern matching, again using a similar syntax to
Haskell. The main difference is that \Idris{} requires type declarations for all
functions, using a single colon \texttt{:} (rather than
Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
defined as follows, again taken from the standard library:

\begin{SaveVerbatim}{natfns}

-- Unary addition
plus : Nat -> Nat -> Nat
plus O     y = y
plus (S k) y = S (plus k y)

-- Unary multiplication
mult : Nat -> Nat -> Nat
mult O     y = O
mult (S k) y = plus y (mult k y)

\end{SaveVerbatim}
\useverb{natfns}

\noindent
The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
for use by \texttt{Nat}, and are implemented
using the above functions.  Unlike Haskell, there is no restriction on whether
types and function names must begin with a capital letter or not. Function
names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
all part of the same namespace.

We can test these functions at the \Idris{} prompt:

\begin{SaveVerbatim}{fntest}

Idris> plus (S (S O)) (S (S O))
S (S (S (S O))) : Nat
Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat

\end{SaveVerbatim}
\useverb{fntest}

\noindent
Like arithmetic operations, integer literals are also overloaded using type classes, 
meaning that we can also test the functions as follows:

\begin{SaveVerbatim}{fntest}

Idris> plus 2 2 
S (S (S (S O))) : Nat
Idris> mult 3 (plus 2 2)
S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat

\end{SaveVerbatim}
\useverb{fntest}

\noindent
You may wonder, by the way, why we have unary natural numbers when our
computers have perfectly good integer arithmetic built in. The reason is
primarily that unary numbers have a very convenient structure which is easy to
reason about, and easy to relate to other data structures as we will see later.
Nevertheless, we do not want this convenience to be at the expense of
efficiency. Fortunately, \Idris{} knows about the relationship between
\tTC{Nat} (and similarly structured types) and numbers, so optimises the
representation and functions such as \tFN{plus} and \tFN{mult}.

\subsubsection*{\texttt{where} clauses}

Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,
to define a function which reverses a list, we can use an auxiliary function which
accumulates the new, reversed list, and which does not need to be visible globally:

\begin{SaveVerbatim}{revwhere}

reverse : List a -> List a
reverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs

\end{SaveVerbatim}
\useverb{revwhere}

\noindent
Indentation is significant --- functions in the \texttt{where} block must be indented
further than the outer function.

\textbf{Scope:} 
Any names which are visible in the outer scope are also visible in the \texttt{where}
clause (unless they have been redefined, such as \texttt{xs} here).
\emph{However}, names which appear in the type are \emph{not} in scope. In particular,
in the above example, the \texttt{a} in the top level type and the \texttt{a} in the
auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required
behaviour, the \texttt{a} can be brought into scope as follows:

\begin{SaveVerbatim}{revwhereb}

reverse : List a -> List a
reverse {a} xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  ...

\end{SaveVerbatim}
\useverb{revwhereb}

\noindent
As well as functions, \texttt{where} blocks can include local data
declarations, such as the following where \texttt{MyLT} is not accessible outside
the definition of \texttt{foo}:

\begin{SaveVerbatim}{wheredata}

foo : Int -> Int
foo x = case isLT of
            Yes => x*2
            No => x*4
    where
       data MyLT = Yes | No

       isLT : MyLT
       isLT = if x < 20 then Yes else No

\end{SaveVerbatim}
\useverb{wheredata}

\noindent
In general, functions defined in a \texttt{where} clause need a type declaration
just like any top level function. However, the type declaration for
a function \texttt{f} \remph{can} be omitted if:

\begin{itemize}
\item \texttt{f} appears in the right hand side of the top level definition 
\item The type of \texttt{f} can be completely determined from its first
application
\end{itemize}

\noindent
So, for example, the following definitions are legal:

\begin{SaveVerbatim}{whereinfer}

even : Nat -> Bool 
even O = True 
even (S k) = odd k where 
  odd O = False 
  odd (S k) = even k 

test : Num a => List a 
test = [c 1, c 2, d 3] 
  where c x = 42 + x 
        d y = c (y + 1 + z y) 
           where z w = y + w 

\end{SaveVerbatim}
\useverb{whereinfer}


\subsection{Dependent Types}

\subsubsection{Vectors}

A standard example of a dependent type is the type of ``lists with length'',
conventionally called vectors in the dependent type literature. In \Idris{},
we declare vectors as follows:

\begin{SaveVerbatim}{vect}

data Vect : Type -> Nat -> Type where
   Nil  : Vect a O
   (::) : a -> Vect a k -> Vect a (S k)

\end{SaveVerbatim}
\useverb{vect}

\noindent
Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
name overloading such as this is accepted by \Idris{}, provided that the names
are declared in different namespaces (in practice, normally in different modules).
Ambiguous constructor names can normally be resolved from context.

This declares a family of types, and so the form of the declaration is rather
different from the simple type declarations above. We explicitly state the type
of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an
argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}
is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
constructor targets a different part of the family of types. \tDC{Nil} can only
be used to construct vectors with zero length, and \tDC{::} to construct
vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element
of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})
combine to make a vector of length \texttt{S k}.

We can define functions on dependent types such as \tTC{Vect} in the same way
as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
The type of a function over \tTC{Vect} will describe what happens to the
lengths of the vectors involved. For example, \tFN{++}, defined in the
library, appends two \tTC{Vect}s:

\begin{SaveVerbatim}{vapp}

(++) : Vect A n -> Vect A m -> Vect A (n + m)
(++) Nil       ys = ys
(++) (x :: xs) ys = x :: xs ++ ys

\end{SaveVerbatim}
\useverb{vapp}

\noindent
The type of \tFN{(++)} states that the resulting vector's length will be the sum of
the input lengths. If we get the definition wrong in such a way that this does
not hold, \Idris{} will not accept the definition. For example:

\begin{SaveVerbatim}{vapperr}

(++) : Vect a n -> Vect a m -> Vect a (n + m)
(++) Nil       ys = ys
(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

\end{SaveVerbatim}
\useverb{vapperr}

\begin{SaveVerbatim}{vapperrmsg}

$ idris vbroken.idr --check
vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))

Specifically:
	 Can't unify k with m

\end{SaveVerbatim}
\begin{SaveVerbatim}{bleh}
$
\end{SaveVerbatim}
\useverb{vapperrmsg}

\noindent
This error message suggests that there is a length mismatch between two vectors
--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
of length \texttt{(S (k + k))}.
Note that the terms in the error message have been \emph{normalised}, so in
particular \texttt{n + m} has been reduced to \texttt{plus n m}.

\subsubsection{The Finite Sets}

Finite sets, as the name suggests, are sets with a finite number of elements.
They are declared as follows (again, in the prelude):

\begin{SaveVerbatim}{findecl}

data Fin : Nat -> Type where
   fO : Fin (S k)
   fS : Fin k -> Fin (S k)

\end{SaveVerbatim}
\useverb{findecl}

\noindent
\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements; 
\texttt{fS n} is the
\texttt{n+1}th element of a finite set with \texttt{S k} elements. 
\tTC{Fin} is indexed by a \tTC{Nat}, which
represents the number of elements in the set. Obviously we can't construct an
element of an empty set, so neither constructor targets \texttt{Fin O}.

A useful application of the \tTC{Fin} family is to represent bounded
natural numbers. Since the first \tTC{n} natural numbers form a finite
set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural
numbers bounded by \tTC{n}. 

For example, the following function which looks up an element in a \tTC{Vect},
by a bounded index given as a \tTC{Fin n}, is defined in the prelude:

\begin{SaveVerbatim}{vindex}

index : Fin n -> Vect a n -> a
index fO     (x :: xs) = x
index (fS k) (x :: xs) = index k xs

\end{SaveVerbatim}
\useverb{vindex}

\noindent
This function looks up a value at a given location in a vector. The location is
bounded by the length of the vector (\texttt{n} in each case), so there is no
need for a run-time bounds check. The type checker guarantees that the location
is no larger than the length of the vector.

Note also that there is no case for \texttt{Nil} here. This is because it is
impossible. Since there is no element of \texttt{Fin O}, and the location is a
\texttt{Fin n}, then \texttt{n} can not be \tDC{O}.  As a result, attempting to
look up an element in an empty vector would give a compile time type error,
since it would force \texttt{n} to be \tDC{O}.

\subsubsection{Implicit Arguments}

Let us take a closer look at the type of \texttt{index}:

\begin{SaveVerbatim}{vindexty}

index : Fin n -> Vect a n -> a

\end{SaveVerbatim}
\useverb{vindexty}

\noindent
It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
with \texttt{n} elements of type \texttt{a}. But there are also two names, 
\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
arguments to \texttt{index}. We could also write the type of \texttt{index} as:

\begin{SaveVerbatim}{vindeximpty}

index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

\end{SaveVerbatim}
\useverb{vindeximpty}

\noindent
Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
not given in applications of \texttt{index}; their values can be inferred from
the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name 
with a \remph{lower case initial letter} which
appears as a parameter or index in a type declaration, but which is otherwise
free, will be automatically bound as an implicit argument.  Implicit arguments
can still be given explicitly in applications, using \texttt{\{a=value\}} and
\texttt{\{n=value\}}, for example:

\begin{SaveVerbatim}{vindexexp}

index {a=Int} {n=2} fO (2 :: 3 :: Nil)

\end{SaveVerbatim}
\useverb{vindexexp}

\noindent
In fact, any argument, implicit or explicit, may be given a name. We could have
declared the type of \texttt{index} as:

\begin{SaveVerbatim}{vindexn}

index : (i:Fin n) -> (xs:Vect a n) -> a

\end{SaveVerbatim}
\useverb{vindexn}

\noindent
It is a matter of taste whether you want to do this --- sometimes it can help
document a function by making the purpose of an argument more clear.

\subsubsection{``\texttt{using}'' notation}

Sometimes it is necessary to provide types of implicit arguments where
the type checker can not work them out itself. This can happen if there is a
dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
before being used --- or if an implicit argument has a complex type. For example,
we will need to state the types of the implicit arguments in the following
definition, which defines a predicate on vectors:

\begin{SaveVerbatim}{elem}

data Elem : a -> Vect a n -> Type where
   here :  {x:a} ->   {xs:Vect a n} -> Elem x (x :: xs)
   there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

\end{SaveVerbatim}
\useverb{elem}

\noindent
An instance of \texttt{Elem x xs} states that \texttt{x} is an element of 
\texttt{xs}. We can construct
such a predicate if the required element is \texttt{here}, at the head of the vector, 
or \texttt{there}, in the tail of the vector. For example:

\begin{SaveVerbatim}{testelem}

testVec : Vect Int 4
testVec = 3 :: 4 :: 5 :: 6 :: Nil

inVect : Elem 5 testVec
inVect = there (there here)

\end{SaveVerbatim}
\useverb{testelem}

\noindent
If the same implicit arguments are being used a lot, it can make a definition
difficult to read. To avoid this problem, a \texttt{using} block gives the types and
ordering of any implicit arguments which can appear within the block:

\begin{SaveVerbatim}{elemusing}

using (x:a, y:a, xs:Vect a n)
  data Elem : a -> Vect a n -> Type where
     here  : Elem x (x :: xs)
     there : Elem x xs -> Elem x (y :: xs)

\end{SaveVerbatim}
\useverb{elemusing}

\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}

In general, functions and data types must be defined before use, since
dependent types allow functions to appear as part of types, and their
reduction behaviour to affect type checking. However, this
restriction can be relaxed by using a \texttt{mutual} block, which allows
data types and functions to be defined simultaneously:

\begin{SaveVerbatim}{mutual}

mutual
  even : Nat -> Bool
  even O = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd O = False
  odd (S k) = even k

\end{SaveVerbatim}
\useverb{mutual}

\noindent
In a \texttt{mutual} block, first all of the type declarations are added,
then the function bodies. As a result, none of the function types can depend
on the reduction behaviour of any of the functions in the block.

\subsection{I/O}

Computer programs are of little use if they do not interact with the user or
the system in some way. The difficulty in a pure language such as \Idris{} ---
that is, a language where expressions do not have side-effects --- is that I/O
is inherently side-effecting. Therefore in \Idris{}, such interactions are
encapsulated in the type \texttt{IO}:

\begin{SaveVerbatim}{ioty}

data IO a -- IO operation returning a value of type a

\end{SaveVerbatim}
\useverb{ioty}

\noindent
We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
the I/O operations to be executed are, rather than how to execute them. The
resulting operations are executed externally,
by the run-time system. We've already seen one IO
program:

\begin{SaveVerbatim}{main}

main : IO ()
main = putStrLn "Hello world"

\end{SaveVerbatim}
\useverb{main}

\noindent
The type of \texttt{putStrLn} explains that it takes a string, and returns an
element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
outputs a string without a newline:

\begin{SaveVerbatim}{putstr}

putStrLn : String -> IO ()
putStr   : String -> IO ()

\end{SaveVerbatim}

We can also read strings from user input:

\begin{SaveVerbatim}{getline}

getLine : IO String

\end{SaveVerbatim}
\useverb{getline}

\noindent
A number of other I/O operations are defined in the prelude, for example for reading and
writing files, including:

\begin{SaveVerbatim}{fileops}

data File -- abstract
data Mode = Read | Write | ReadWrite

openFile  : String -> Mode -> IO File
closeFile : File -> IO ()

fread  : File -> IO String
fwrite : File -> String -> IO ()
feof   : File -> IO Bool

readFile : String -> IO String

\end{SaveVerbatim}
\useverb{fileops}

\subsection{``\texttt{do}'' notation}

\label{sect:do}

I/O programs will typically need to sequence actions, feeding the output of one
computation into the input of the next. \texttt{IO} is an abstract type, however, so we
can't access the result of a computation directly. Instead, we sequence
operations with \texttt{do} notation:

\begin{SaveVerbatim}{greet}

greet : IO ()
greet = do putStr "What is your name? "
           name <- getLine
           putStrLn ("Hello " ++ name)

\end{SaveVerbatim}
\useverb{greet}

\noindent
The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type 
\texttt{IO a}, and
puts the result, of type \texttt{a} into the variable \texttt{x}. 
In this case, \texttt{getLine} returns an \texttt{IO String},
so \texttt{name} has type \texttt{String}. Indentation is significant --- each
statement in the do block must begin in the same column.
The \texttt{return} operation allows us to inject a value directly into an IO
operation:

\begin{SaveVerbatim}{return}

return : a -> IO a

\end{SaveVerbatim}
\useverb{return}

\noindent
As we will see later, \texttt{do} notation is more general than this, and can be
overloaded.

\subsection{Useful Data Types}

\Idris{} includes a number of useful data types and library functions (see the
\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
functions described here are imported automatically by every \Idris{} program, as
part of \texttt{prelude.idr}.

\subsubsection{\texttt{List} and \texttt{Vect}}

We have already seen the \texttt{List} and \texttt{Vect} data types:

\begin{SaveVerbatim}{listvec}

data List a = Nil | (::) a (List a)

data Vect : Type -> Nat -> Type where
   Nil  : Vect a O
   (::) : a -> Vect a k -> Vect a (S k)

\end{SaveVerbatim}
\useverb{listvec}

\noindent
Note that the constructor names are the same for each --- constructor names (in
fact, names in general) can be overloaded, provided that they are declared in
different namespaces (see Section \ref{sect:namespaces}), and will typically be
resolved according to their type. As syntactic sugar, any type with the constructor
names \texttt{Nil} and \texttt{::} can be written in list form. For example:

\begin{itemize}
\item \texttt{[]} means \texttt{Nil}
\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
\end{itemize}

\noindent
The library also defines a number of functions for manipulating these types.
\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
and applies a function to every element of the list or vector.

\begin{SaveVerbatim}{map}

map : (a -> b) -> List a -> List b
map f []        = []
map f (x :: xs) = f x :: map f xs

map : (a -> b) -> Vect a n -> Vect b n
map f []        = []
map f (x :: xs) = f x :: map f xs

\end{SaveVerbatim}
\useverb{map}

\noindent
For example, to double every element in a vector of integers:

\begin{SaveVerbatim}{dvect}

intVec : Vect Int 5
intVec = [1, 2, 3, 4, 5]

double : Int -> Int
double x = x * 2

\end{SaveVerbatim}
\useverb{dvect}

\noindent
You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:

\begin{SaveVerbatim}{rundvect}

*usefultypes> show (map double intVec) 
"[2, 4, 6, 8, 10]" : String

\end{SaveVerbatim}
\useverb{rundvect}

\noindent
For more details of the functions available on \texttt{List} and \texttt{Vect},
look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
Functions include filtering, appending, reversing, and so on. Also remember
that \Idris{} is still in development, so if you don't see the function you
need, please feel free to add it and submit a patch!

\subsubsection*{Aside: Anonymous functions and operator sections}

There are actually neater ways to write the above expression. One way would be
to use an anonymous function:

\begin{SaveVerbatim}{lam1}

*usefultypes> show (map (\x => x * 2) intVec)
"[2, 4, 6, 8, 10]" : String

\end{SaveVerbatim}
\useverb{lam1}

\noindent
The notation \texttt{$\backslash$x => val} constructs an anonymous function
which takes one argument, \texttt{x} and returns the expression \texttt{val}.
Anonymous functions may take several arguments, separated by commas, e.g.
\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
e.g. \texttt{$\backslash$ (x, y) => x + y}.
We could also use an operator section:

\begin{SaveVerbatim}{sec1}

*usefultypes> show (map (* 2) intVec)
"[2, 4, 6, 8, 10]" : String

\end{SaveVerbatim}
\useverb{sec1}

\noindent
\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
\texttt{$\backslash$x => x * 2}. 
Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.

\subsubsection{Maybe}

\texttt{Maybe} describes an optional value. Either there is a value of the given type,
or there isn't:

\begin{SaveVerbatim}{maybe}

data Maybe a = Just a | Nothing

\end{SaveVerbatim}
\useverb{maybe}

\noindent
\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
looking something up in a \texttt{List} (rather than a vector) may result in an out of
bounds error:

\begin{SaveVerbatim}{lookuplist}

list_lookup : Nat -> List a -> Maybe a
list_lookup _     Nil       = Nothing
list_lookup O     (x :: xs) = Just x
list_lookup (S k) (x :: xs) = list_lookup k xs

\end{SaveVerbatim}
\useverb{lookuplist}

\noindent
The \texttt{maybe} function is used to process values of type \texttt{Maybe}, 
either by applying a function to the value, if there is one, or by providing a default value:

\begin{SaveVerbatim}{maybefn}

maybe : Maybe a -> |(default:b) -> (a -> b) -> b

\end{SaveVerbatim}
\useverb{maybefn}

\noindent
The vertical bar $\mid$ before the default value is a laziness annotation. Normally
expressions are evaluated before being passed to a function. This is typically
the most efficient behaviour. However, in this case, the default value might
not be used and if it is a large expression, evaluating it will be wasteful.
The $\mid$ annotation tells the compiler not to evaluate the argument until it is
needed.

\subsubsection{Tuples and Dependent Pairs}

Values can be paired with the following built-in data type:

\begin{SaveVerbatim}{mkpair}

data Pair a b = MkPair a b

\end{SaveVerbatim}
\useverb{mkpair}

\noindent
As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
means either \texttt{Pair a b} or \texttt{MkPair a b}.
Tuples can contain an arbitrary number of values, represented as nested pairs:

\begin{SaveVerbatim}{tuple}

fred : (String, Int)
fred = ("Fred", 42)

jim : (String, Int, String)
jim = ("Jim", 25, "Cambridge")

\end{SaveVerbatim}
\useverb{tuple}

\subsubsection*{Dependent Pairs}

Dependent pairs allow the type of the second element of a pair to depend on
the value of the first element:

\begin{SaveVerbatim}{sigma}

data Exists : (A : Type) -> (P : A -> Type) -> Type where
   Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P

\end{SaveVerbatim}
\useverb{sigma}

\noindent
Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )} 
constructs a value of this type. For example, we can pair a number with a 
\texttt{Vect} of a particular length.

\begin{SaveVerbatim}{dvec}

vec : (n : Nat ** Vect Int n)
vec = (2 ** [3, 4])

\end{SaveVerbatim}
\useverb{dvec}

\noindent
The type checker could of course infer the value of the first element from the
length of the vector. We can write an underscore \texttt{\_} in place of values which we
expect the type checker to fill in, so the above definition could also be
written as:

\begin{SaveVerbatim}{dvec1}

vec : (n : Nat ** Vect Int n)
vec = (_ ** [3, 4])

\end{SaveVerbatim}
\useverb{dvec1}

\noindent
We might also prefer to omit the type of the first element of the pair, since,
again, it can be inferred:

\begin{SaveVerbatim}{dvec2}

vec : (n ** Vect Int n)
vec = (_ ** [3, 4])

\end{SaveVerbatim}
\useverb{dvec2}

\noindent
One use for dependent pairs is to return values of dependent types where the
index is not necessarily known in advance. For example, if we filter elements
out of a \texttt{Vect} according to some predicate, we will not know in advance what the
length of the resulting vector will be:

\begin{SaveVerbatim}{vfilter}

filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

\end{SaveVerbatim}
\useverb{vfilter}

\noindent
If the \texttt{Vect} is empty, the result is easy:

\begin{SaveVerbatim}{vfilternil}

filter p Nil = (_ , [])

\end{SaveVerbatim}
\useverb{vfilternil}

\noindent
In the \texttt{::} case, we need to inspect the result of a recursive call to 
\texttt{filter} to
extract the length and the vector from the result. To do this, we use \texttt{with}
notation, which allows pattern matching on intermediate values:

\begin{SaveVerbatim}{vfiltercons}

filter p (x :: xs) with (filter p xs)
  | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

\end{SaveVerbatim}
\useverb{vfiltercons}

\noindent
We will see more on \texttt{with} notation later.

\subsection{\texttt{so}}

The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
value is true:

\begin{SaveVerbatim}{sotype}

data so : Bool -> Type where
    oh : so True

\end{SaveVerbatim}
\useverb{sotype} 

\noindent
This is most useful for providing a static guarantee that a dynamic check has been made.
For example, we might provide a safe interface to a function which draws a pixel
on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that 
the point \texttt{(x,y)} is within the bounds of a 640x480 window:

\begin{SaveVerbatim}{soexample}

inBounds : Int -> Int -> Bool
inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480

drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
drawPoint x y p = unsafeDrawPoint x y

\end{SaveVerbatim}
\useverb{soexample} 

\subsection{More Expressions}

\subsubsection*{\texttt{let} bindings}

Intermediate values can be calculated using \texttt{let} bindings:

\begin{SaveVerbatim}{letb}

mirror : List a -> List a
mirror xs = let xs' = rev xs in
                xs ++ xs'

\end{SaveVerbatim}
\useverb{letb} 

\noindent
We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
fields from a record as follows, as well as by pattern matching at the top level:

\begin{SaveVerbatim}{letp}

data Person = MkPerson String Int

showPerson : Person -> String
showPerson p = let MkPerson name age = p in
                   name ++ " is " ++ show age ++ " years old"

\end{SaveVerbatim}
\useverb{letp} 

\subsubsection*{List comprehensions}

\label{sec:listcomp}

\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
building lists. The general form is:

\begin{SaveVerbatim}{listcomp}

[ expression | qualifiers ]

\end{SaveVerbatim}
\useverb{listcomp} 

\noindent
This generates the list of values produced by evaluating the
\texttt{expression}, according to the conditions given by the comma separated
\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
follows:

\begin{SaveVerbatim}{triples}

pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
                         x*x + y*y == z*z ]
  
\end{SaveVerbatim}
\useverb{triples} 

\noindent
The \texttt{[a..b]} notation is another shorthand which builds a list of
numbers between \texttt{a} and \texttt{b}.  Alternatively \texttt{[a,b..c]}
builds a list of numbers between \texttt{a} and \texttt{c} with the increment
specified by the difference between \texttt{a} and \texttt{c}.  This works for
any numeric type, using the \texttt{count} function from the prelude. 

\subsubsection*{\texttt{case} expressions}

Another way of inspecting intermediate values of \emph{simple} types
is to use a \texttt{case} expression.
The following function, for example, splits a string into two at a given character:

\begin{SaveVerbatim}{split}

splitAt : Char -> String -> (String, String)
splitAt c x = case break (== c) x of
                  (x, y) => (x, strTail y)

\end{SaveVerbatim}
\useverb{split} 

\noindent
\texttt{break} is a library function which breaks a string into a pair of strings
at the point where the given function returns true. We then deconstruct the
pair it returns, and remove the first character of the second string.

A \texttt{case} expression can match several cases, for example, to inspect an
intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
looks up an index in a list, returning \texttt{Nothing} if the index is out
of bounds. We can use this to write \texttt{lookup\_default}, which
looks up an index and returns a default value if the index is out of bounds:

\begin{SaveVerbatim}{listlookup}

lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
                              Nothing => def
                              Just x => x

\end{SaveVerbatim}
\useverb{listlookup} 

\noindent
If the index is in bounds, we get the value at that index, otherwise we get
a default value:

\begin{SaveVerbatim}{deftest}

*usefultypes> lookup_default 2 [3,4,5,6] (-1)
5 : Int
*usefultypes> lookup_default 4 [3,4,5,6] (-1)
-1 : Int

\end{SaveVerbatim}
\useverb{deftest} 

\noindent
\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
of intermediate expressions to avoid the need to write auxiliary functions, and is
also used internally to implement pattern matching \texttt{let} and lambda bindings. 
It will \emph{only} work if:

\begin{itemize}
\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
value of the same type.
\item The type of the result is ``known''. i.e. the type of the expression can be
determined \emph{without} type checking the \texttt{case}-expression itself. 
\end{itemize}

\subsection{Dependent Records}

\remph{Records} are data types which collect several values (the record's
\remph{fields}) together. \Idris{} provides syntax for defining records and
automatically generating field access and update functions. For example, we
can represent a person's name and age in a record:

\begin{SaveVerbatim}{recsimpl}

record Person : Type where
    MkPerson : (name : String) ->
               (age : Int) -> Person

fred : Person
fred = MkPerson "Fred" 30

\end{SaveVerbatim}
\useverb{recsimpl} 

\noindent
Record declarations are like \texttt{data} declarations, except that they are 
introduced by the \texttt{record} keyword, and can only have one constructor.
The names of the binders in the constructor type (\texttt{name} and \texttt{age})
here are the field names, which we can use to access the field values:

\begin{SaveVerbatim}{recaccess}

*record> name fred
"Fred" : String
*record> age fred
30 : Int
*record> :t name
name : Person -> String

\end{SaveVerbatim}
\useverb{recaccess} 

\noindent
We can also use the field names to update a record (or, more precisely, produce a
new record with the given fields updates).

\begin{SaveVerbatim}{recupdate}

*record> record { name = "Jim" } fred
MkPerson "Jim" 30 : Person
*record> record { name = "Jim", age = 20 } fred
MkPerson "Jim" 20 : Person

\end{SaveVerbatim}
\useverb{recupdate} 

\noindent
The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
the given fields in a record. 

Records, and fields within records, can have dependent types.
Updates are allowed to change the type of a field,
provided that the result is well-typed, and the result does not affect the type of
the record as a whole. For example:

\begin{SaveVerbatim}{deprec}

record Class : Type where
    ClassInfo : (students : Vect Person n) ->
                (className : String) ->
                Class

\end{SaveVerbatim}
\useverb{deprec} 

\noindent
It is safe to update the \texttt{students} field to a vector of a different length
because it will not affect the type of the record:

\begin{SaveVerbatim}{addstu}

addStudent : Person -> Class -> Class
addStudent p c = record { students = p :: students c } c

*record> addStudent fred (ClassInfo [] "CS")
ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS" 
  : Class

\end{SaveVerbatim}
\useverb{addstu}