\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
foreign function interface, type providers, 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 target "x"} --- include the \texttt{libx} library. If the target is \texttt{C} this is equivalent to passing the
\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a 
"groupId:artifactId:packaging:version" dependency coordinate for maven.
\item \texttt{\%include target "x"} --- use the header file or import \texttt{x} for the given back end target.
\item \texttt{\%link target "x.o"} --- link with the object file \texttt{x.o} when using the given back end target.
\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
\end{itemize}

\subsubsection*{Testing foreign function calls}
Normally, the Idris interpreter (used for typechecking and at the REPL) will
not perform IO actions.  Additionally, as it neither generates C code nor
compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and
\texttt{\%link} directives have no effect. IO actions and FFI calls can be
tested using the special REPL command \texttt{:x EXPR}, and C libraries can be
dynamically loaded in the interpreter by using the \texttt{:dynamic} command
or the \texttt{\%dynamic} directive. For example:

\begin{SaveVerbatim}{xdynamic}

Idris> :dynamic libm.so
Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
0.9995736030415051 : Float

\end{SaveVerbatim}
\useverb{xdynamic}

\subsection{Type Providers}
Idris type providers, inspired by F\#'s type providers, are a means of making
our types be ``about'' something in the world outside of Idris. For example,
given a type that represents a database schema and a query that is checked
against it, a type provider could read the schema of a real database during
type checking.

Idris type providers use the ordinary execution semantics of Idris to run an
IO action and extract the result. This result is then saved as a constant in
the compiled code. It can be a type, in which case it is used like any other
type, or it can be a value, in which case it can be used as any other value,
including as an index in types.

Type providers are still an experimental extension. To enable the extension,
use the \texttt{\%language} directive:
\begin{SaveVerbatim}{languageProv}

%language TypeProviders

\end{SaveVerbatim}

\useverb{languageProv}


A provider \texttt{p} for some type \texttt{t} is simply an expression of type
\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type
checker to execute the action and bind the result to a name.  This is perhaps
best illustrated with a simple example. The type provider \texttt{fromFile}
reads a text file. If the file consists of the string \texttt{"Int"}, then the
type \texttt{Int} will be provided. Otherwise, it will provide the type
\texttt{Nat}.

\begin{SaveVerbatim}{fromFile}

strToType : String -> Type
strToType "Int" = Int
strToType _ = Nat

fromFile : String -> IO (Provider Type)
fromFile fname = do str <- readFile fname
                    return (Provide (strToType (trim str)))

\end{SaveVerbatim}
\useverb{fromFile}

We then use the \texttt{\%provide} directive:

\begin{SaveVerbatim}{fromFileUse}

%provide (T1 : Type) with fromFile "theType"

foo : T1
foo = 2

\end{SaveVerbatim}
\useverb{fromFileUse}

\noindent
If the file named \texttt{theType} consists of the word \texttt{Int}, then
\texttt{foo} will be an \texttt{Int}. Otherwise, it will be a \texttt{Nat}.
When Idris encounters the directive, it first checks that the provider
expression \texttt{fromFile "theType"} has type \texttt{IO (Provider
  Type)}. Next, it executes the provider. If the result is \texttt{Provide t},
then \texttt{T1} is defined as \texttt{t}. Otherwise, the result is an error.

Our datatype \texttt{Provider t} has the following definition:

\begin{SaveVerbatim}{providerdef}

data Provider a = Error String
                | Provide a

\end{SaveVerbatim}
\useverb{providerdef}

\noindent
We have already seen the \texttt{Provide} constructor. The \texttt{Error}
constructor allows type providers to return useful error messages.  The
example in this section was purposefully simple. More complex type provider
implementations, including a statically-checked SQLite binding, are available
in an external collection.\footnote{\url{https://github.com/david-christiansen/idris-type-providers}}

\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 : Nat -> Type -> 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 1

\end{SaveVerbatim}
\useverb{setset} 

\noindent
If \texttt{Type} were its own type, it 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?