Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

267 lines (187 sloc) 7.731 kb
\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{vlookupimpty}
\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{float}, \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 -> Set
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) -> Set
\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 : Set
Idris> ForeignTy [FInt, FString] FUnit
Int -> String -> IO () : Set
\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 : Set -> Set 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{\%obj "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 : Set
*universe> :t Vect
Vect : Set -> Nat -> Set
\end{SaveVerbatim}
\useverb{typetypes}
\noindent
But what about the type of \texttt{Set}? If we ask \Idris{} it reports
\begin{SaveVerbatim}{setset}
*universe> :t Set
Set : Set
\end{SaveVerbatim}
\useverb{setset}
\noindent
It \emph{appears} that \texttt{Set} 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}
Set : Set 1 : Set 2 : Set 3 : ...
\end{SaveVerbatim}
\useverb{sethierarchy}
\noindent
Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have that
\texttt{x : Set 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 : Set) -> a -> a
myid _ x = x
idid : (a : Set) -> 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{Set}, 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?
Jump to Line
Something went wrong with that request. Please try again.