\section{Miscellany}

In this section we discuss a variety of additional features:
auto implicit and default 
arguments, literate programming, interfacing with external libraries through the
foriegn function interface, and the universe hierarchy.

\subsection{Auto implicit arguments}

We have already seen implicit arguments, which allows arguments to be omitted when
they can be inferred by the type checker, e.g.

\useverb{vindeximpty}

\noindent
In other situations, it may be possible to infer arguments not by type checking but
by searching the context for an appropriate value, or constructing a proof. For example,
the following definition of \texttt{head} which requires a proof that the list is
non-empty

\begin{SaveVerbatim}{safehead}

isCons : List a -> Bool
isCons [] = False
isCons (x :: xs) = True

head : (xs : List a) -> (isCons xs = True) -> a
head (x :: xs) _ = x

\end{SaveVerbatim}
\useverb{safehead} 

\noindent
If the list is statically known to be non-empty, either because its value is known or
because a proof already exists in the context, the proof can be constructed
automatically. Auto implicit arguments allow this to happen silently. We define
\texttt{head} as follows:

\begin{SaveVerbatim}{headauto}

head : (xs : List a) -> {auto p : isCons xs = True} -> a
head (x :: xs) = x

\end{SaveVerbatim}
\useverb{headauto} 

\noindent
The \texttt{auto} annotation on the implicit argument means that \Idris{} will
attempt to fill in the implicit argument using the \texttt{trivial} tactic, which
searches through the context for a proof, and tries to solve with \texttt{refl}
if a proof is not found.
Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof
is not found, it can be provided explicitly as normal:

\begin{SaveVerbatim}{headapp}

head xs {p = ?headProof} 

\end{SaveVerbatim}
\useverb{headapp} 

\noindent
More generally, we can fill in implicit arguments with a default value by annotating
them with \texttt{default}. The definition above is equivalent to:

\begin{SaveVerbatim}{defimp}

head : (xs : List a) -> 
       {default proof { trivial; } p : isCons xs = True} -> a
head (x :: xs) = x

\end{SaveVerbatim}
\useverb{defimp} 

\subsection{Literate programming}

Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
programs, everything is assumed to be a comment unless the line begins with a
greater than sign \texttt{>}, for example:

\begin{SaveVerbatim}{litidr}

> module literate

This is a comment. The main program is below

> main : IO ()
> main = putStrLn "Hello literate world!\n"

\end{SaveVerbatim}
\useverb{litidr}

\noindent
An additional restriction is that there must be a blank line between a program
line (beginning with \texttt{>}) and a comment line (beginning with any other
character).

\subsection{Foreign function calls}

For practical programming, it is often necessary to be able to use external libraries,
particularly for interfacing with the operating system, file system, networking, etc.
\Idris{} provides a lightweight foreign function interface for achieving this,
as part of the prelude. For this, we assume a certain amount of knowledge of
C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
types we can handle:

\begin{SaveVerbatim}{foreignty}

data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit

\end{SaveVerbatim}
\useverb{foreignty}

\noindent
Each of these corresponds directly to a C type. Respectively: \texttt{int},
\texttt{double}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
There is also a translation to a concrete \Idris{} type, described by the
following function:

\begin{SaveVerbatim}{interpfty}

interpFTy : FTy -> Type
interpFTy FInt    = Int
interpFTy FFloat  = Float
interpFTy FChar   = Char
interpFTy FString = String
interpFTy FPtr    = Ptr
interpFTy FUnit   = ()

\end{SaveVerbatim}
\useverb{interpfty}

\noindent
A foreign function is described by a list of input types and a return type, which
can then be converted to an \Idris{} type:

\begin{SaveVerbatim}{ffunty}

ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

\end{SaveVerbatim}
\useverb{ffunty}

\noindent
A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
\texttt{IO} type, for example:

\begin{SaveVerbatim}{ftyex}

Idris> ForeignTy [FInt, FString] FString
Int -> String -> IO String : Type

Idris> ForeignTy [FInt, FString] FUnit 
Int -> String -> IO () : Type

\end{SaveVerbatim}
\useverb{ftyex}

\noindent
We build a call to a foreign function by giving the name of the function, a list of
argument types and the return type. The built in function \texttt{mkForeign}
converts this description to a function callable by \Idris{}

\begin{SaveVerbatim}{mkForeign}

data Foreign : Type -> Type where
    FFun : String -> (xs:List FTy) -> (t:FTy) -> 
           Foreign (ForeignTy xs t)

mkForeign : Foreign x -> x

\end{SaveVerbatim}
\useverb{mkForeign}

\noindent
For example, the \texttt{putStr} function is implemented as follows, as a call to 
an external function \texttt{putStr} defined in the run-time system:

\begin{SaveVerbatim}{putStrex}

putStr : String -> IO ()
putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
\end{SaveVerbatim}
\useverb{putStrex}

\subsubsection*{Include and linker directives}

Foreign function calls are translated directly to calls to C functions, with appropriate
conversion between the \Idris{} representation of a value and the C representation.
Often this will require extra libraries to be linked in, or extra header and object files.
This is made possible through the following directives:

\begin{itemize}
\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
\texttt{-lx} option to \texttt{gcc}.
\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.
\end{itemize}

\subsection{Cumulativity}

Since values can appear in types and \emph{vice versa}, it is natural that types themselves
have types. For example:

\begin{SaveVerbatim}{typetypes}

*universe> :t Nat
Nat : Type
*universe> :t Vect
Vect : Type -> Nat -> Type

\end{SaveVerbatim}
\useverb{typetypes} 

\noindent
But what about the type of \texttt{Type}? If we ask \Idris{} it reports

\begin{SaveVerbatim}{setset}

*universe> :t Type
Type : Type

\end{SaveVerbatim}
\useverb{setset} 

\noindent
It \emph{appears} that \texttt{Type} is its own type. This would lead to an inconsitency
due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
of types (or \emph{universes}):

\begin{SaveVerbatim}{sethierarchy}

Type : Type 1 : Type 2 : Type 3 : ...

\end{SaveVerbatim}
\useverb{sethierarchy} 

\noindent
Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that
\texttt{x : Type m}, as long as \texttt{n < m}. 
The typechecker generates such universe 
constraints and reports an error if any inconsistencies are found. Ordinarily, a
programmer does not need to worry about this, but it does prevent (contrived)
programs such as the following:

\begin{SaveVerbatim}{idid}

myid : (a : Type) -> a -> a
myid _ x = x

idid :  (a : Type) -> a -> a
idid = myid _ myid

\end{SaveVerbatim}
\useverb{idid} 

\noindent
The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
--- \texttt{myid}'s first argument is a \texttt{Type}, which cannot be at a lower level
than required if it is applied to itself.

%\subsection{Comparison}

%How does \Idris{} compare with other dependently typed languages and proof
%assistants, such as Coq, Agda and Epigram?