3In this section we discuss a variety of additional features:
4auto implicit and default
5arguments, literate programming, interfacing with external libraries through the
6foriegn function interface, and the universe hierarchy.
8\subsection{Auto implicit arguments}
10We have already seen implicit arguments, which allows arguments to be omitted when
11they can be inferred by the type checker, e.g.
16In other situations, it may be possible to infer arguments not by type checking but
17by searching the context for an appropriate value, or constructing a proof. For example,
18the following definition of \texttt{head} which requires a proof that the list is
21\begin{SaveVerbatim}{safehead}
23isCons : List a -> Bool
25isCons (x :: xs) = True
27head : (xs : List a) -> (isCons xs = True) -> a
34If the list is statically known to be non-empty, either because its value is known or
35because a proof already exists in the context, the proof can be constructed
36automatically. Auto implicit arguments allow this to happen silently. We define
37\texttt{head} as follows:
39\begin{SaveVerbatim}{headauto}
41head : (xs : List a) -> {auto p : isCons xs = True} -> a
48The \texttt{auto} annotation on the implicit argument means that \Idris{} will
49attempt to fill in the implicit argument using the \texttt{trivial} tactic, which
50searches through the context for a proof, and tries to solve with \texttt{refl}
51if a proof is not found.
52Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof
53is not found, it can be provided explicitly as normal:
55\begin{SaveVerbatim}{headapp}
57head xs {p = ?headProof}
63More generally, we can fill in implicit arguments with a default value by annotating
64them with \texttt{default}. The definition above is equivalent to:
66\begin{SaveVerbatim}{defimp}
68head : (xs : List a) ->
69 {default proof { trivial; } p : isCons xs = True} -> a
75\subsection{Implicit conversions}
77\Idris{} supports the creation of \emph{implicit conversions}, which allow
78automatic conversion of values from one type to another when required to make
79a term type correct. This is intended to increase convenience and reduce
80verbosity. A contrived but simple example is the following:
82\begin{SaveVerbatim}{implicit}
84implicit intString : Int -> String
88test x = "Number " ++ x
94In general, we cannot append an \texttt{Int} to a \texttt{String}, but the
95implicit conversion function \texttt{intString} can convert \texttt{x} to a
96\texttt{String}, so the definition of \texttt{test} is type correct. An
97implicit conversion is implemented just like any other function, but given
98the \texttt{implicit} modifier, and restricted to one explicit argument.
100Only one implicit conversion will be applied at a time. That is, implicit
101conversions cannot be chained.
102Implicit conversions of simple types, as above, are however discouraged! More
103commonly, an implicit conversion would be used to reduce verbosity in an
104embedded domain specific language, or to hide details of a proof. Such examples
105are beyond the scope of this tutorial.
107\subsection{Literate programming}
109Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
110extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
111programs, everything is assumed to be a comment unless the line begins with a
112greater than sign \texttt{>}, for example:
114\begin{SaveVerbatim}{litidr}
118This is a comment. The main program is below
121> main = putStrLn "Hello literate world!\n"
127An additional restriction is that there must be a blank line between a program
128line (beginning with \texttt{>}) and a comment line (beginning with any other
131\subsection{Foreign function calls}
133For practical programming, it is often necessary to be able to use external libraries,
134particularly for interfacing with the operating system, file system, networking, etc.
135\Idris{} provides a lightweight foreign function interface for achieving this,
136as part of the prelude. For this, we assume a certain amount of knowledge of
137C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
140\begin{SaveVerbatim}{foreignty}
142data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
148Each of these corresponds directly to a C type. Respectively: \texttt{int},
149\texttt{double}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
150There is also a translation to a concrete \Idris{} type, described by the
153\begin{SaveVerbatim}{interpfty}
155interpFTy : FTy -> Type
157interpFTy FFloat = Float
158interpFTy FChar = Char
159interpFTy FString = String
167A foreign function is described by a list of input types and a return type, which
168can then be converted to an \Idris{} type:
170\begin{SaveVerbatim}{ffunty}
172ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
178A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
179\texttt{IO} type, for example:
181\begin{SaveVerbatim}{ftyex}
183Idris> ForeignTy [FInt, FString] FString
184Int -> String -> IO String : Type
186Idris> ForeignTy [FInt, FString] FUnit
187Int -> String -> IO () : Type
193We build a call to a foreign function by giving the name of the function, a list of
194argument types and the return type. The built in function \texttt{mkForeign}
195converts this description to a function callable by \Idris{}
197\begin{SaveVerbatim}{mkForeign}
199data Foreign : Type -> Type where
200 FFun : String -> (xs:List FTy) -> (t:FTy) ->
201 Foreign (ForeignTy xs t)
203mkForeign : Foreign x -> x
209For example, the \texttt{putStr} function is implemented as follows, as a call to
210an external function \texttt{putStr} defined in the run-time system:
212\begin{SaveVerbatim}{putStrex}
214putStr : String -> IO ()
215putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
219\subsubsection*{Include and linker directives}
221Foreign function calls are translated directly to calls to C functions, with appropriate
222conversion between the \Idris{} representation of a value and the C representation.
223Often this will require extra libraries to be linked in, or extra header and object files.
224This is made possible through the following directives:
227\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
228\texttt{-lx} option to \texttt{gcc}.
229\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
230\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.
231\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
234\subsubsection*{Testing foreign function calls}
235Normally, the Idris interpreter (used for typechecking and at the REPL) will
236not perform IO actions. Additionally, as it neither generates C code nor
237compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and
238\texttt{\%link} directives have no effect. IO actions and FFI calls can be
239tested using the special REPL command \texttt{:x EXPR}, and C libraries can be
240dynamically loaded in the interpreter by using the \texttt{:dynamic} command
241or the \texttt{\%dynamic} directive. For example:
243\begin{SaveVerbatim}{xdynamic}
244Idris> :dynamic libm.so
245Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
2460.9995736030415051 : Float
249\subsection{Cumulativity}
251Since values can appear in types and \emph{vice versa}, it is natural that types themselves
252have types. For example:
254\begin{SaveVerbatim}{typetypes}
259Vect : Type -> Nat -> Type
265But what about the type of \texttt{Type}? If we ask \Idris{} it reports
267\begin{SaveVerbatim}{setset}
276It \emph{appears} that \texttt{Type} is its own type. This would lead to an inconsitency
277due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
278of types (or \emph{universes}):
280\begin{SaveVerbatim}{sethierarchy}
282Type : Type 1 : Type 2 : Type 3 : ...
285\useverb{sethierarchy}
288Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that
289\texttt{x : Type m}, as long as \texttt{n < m}.
290The typechecker generates such universe
291constraints and reports an error if any inconsistencies are found. Ordinarily, a
292programmer does not need to worry about this, but it does prevent (contrived)
293programs such as the following:
295\begin{SaveVerbatim}{idid}
297myid : (a : Type) -> a -> a
300idid : (a : Type) -> a -> a
307The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
308--- \texttt{myid}'s first argument is a \texttt{Type}, which cannot be at a lower level
309than required if it is applied to itself.
311%\subsection{Comparison}
313%How does \Idris{} compare with other dependently typed languages and proof
314%assistants, such as Coq, Agda and Epigram?
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list