\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{Implicit conversions}

\Idris{} supports the creation of \emph{implicit conversions}, which allow
automatic conversion of values from one type to another when required to make
a term type correct. This is intended to increase convenience and reduce
verbosity. A contrived but simple example is the following:

\begin{SaveVerbatim}{implicit}

implicit intString : Int -> String
intString = show
  
test : Int -> String
test x = "Number " ++ x

\end{SaveVerbatim}
\useverb{implicit}

\noindent
In general, we cannot append an \texttt{Int} to a \texttt{String}, but the
implicit conversion function \texttt{intString} can convert \texttt{x} to a
\texttt{String}, so the definition of \texttt{test} is type correct. An
implicit conversion is implemented just like any other function, but given
the \texttt{implicit} modifier, and restricted to one explicit argument.

Only one implicit conversion will be applied at a time. That is, implicit
conversions cannot be chained.
Implicit conversions of simple types, as above, are however discouraged! More
commonly, an implicit conversion would be used to reduce verbosity in an
embedded domain specific language, or to hide details of a proof. Such examples
are beyond the scope of this tutorial.

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