git.iko.soy/Idris-dev
on 694bf20 help sign in
Idris-dev/tutorial/miscellany.tex
266 lines 7.7 kB history raw
1\section{Miscellany}
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.
13\useverb{vindeximpty}
15\noindent
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
19non-empty
21\begin{SaveVerbatim}{safehead}
23isCons : List a -> Bool
24isCons [] = False
25isCons (x :: xs) = True
27head : (xs : List a) -> (isCons xs = True) -> a
28head (x :: xs) _ = x
30\end{SaveVerbatim}
31\useverb{safehead}
33\noindent
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
42head (x :: xs) = x
44\end{SaveVerbatim}
45\useverb{headauto}
47\noindent
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}
59\end{SaveVerbatim}
60\useverb{headapp}
62\noindent
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
70head (x :: xs) = x
72\end{SaveVerbatim}
73\useverb{defimp}
75\subsection{Literate programming}
77Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
78extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
79programs, everything is assumed to be a comment unless the line begins with a
80greater than sign \texttt{>}, for example:
82\begin{SaveVerbatim}{litidr}
84> module literate
86This is a comment. The main program is below
88> main : IO ()
89> main = putStrLn "Hello literate world!\n"
91\end{SaveVerbatim}
92\useverb{litidr}
94\noindent
95An additional restriction is that there must be a blank line between a program
96line (beginning with \texttt{>}) and a comment line (beginning with any other
97character).
99\subsection{Foreign function calls}
101For practical programming, it is often necessary to be able to use external libraries,
102particularly for interfacing with the operating system, file system, networking, etc.
103\Idris{} provides a lightweight foreign function interface for achieving this,
104as part of the prelude. For this, we assume a certain amount of knowledge of
105C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
106types we can handle:
108\begin{SaveVerbatim}{foreignty}
110data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
112\end{SaveVerbatim}
113\useverb{foreignty}
115\noindent
116Each of these corresponds directly to a C type. Respectively: \texttt{int},
117\texttt{double}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
118There is also a translation to a concrete \Idris{} type, described by the
119following function:
121\begin{SaveVerbatim}{interpfty}
123interpFTy : FTy -> Set
124interpFTy FInt = Int
125interpFTy FFloat = Float
126interpFTy FChar = Char
127interpFTy FString = String
128interpFTy FPtr = Ptr
129interpFTy FUnit = ()
131\end{SaveVerbatim}
132\useverb{interpfty}
134\noindent
135A foreign function is described by a list of input types and a return type, which
136can then be converted to an \Idris{} type:
138\begin{SaveVerbatim}{ffunty}
140ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
142\end{SaveVerbatim}
143\useverb{ffunty}
145\noindent
146A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
147\texttt{IO} type, for example:
149\begin{SaveVerbatim}{ftyex}
151Idris> ForeignTy [FInt, FString] FString
152Int -> String -> IO String : Set
154Idris> ForeignTy [FInt, FString] FUnit
155Int -> String -> IO () : Set
157\end{SaveVerbatim}
158\useverb{ftyex}
160\noindent
161We build a call to a foreign function by giving the name of the function, a list of
162argument types and the return type. The built in function \texttt{mkForeign}
163converts this description to a function callable by \Idris{}
165\begin{SaveVerbatim}{mkForeign}
167data Foreign : Set -> Set where
168 FFun : String -> (xs:List FTy) -> (t:FTy) ->
169 Foreign (ForeignTy xs t)
171mkForeign : Foreign x -> x
173\end{SaveVerbatim}
174\useverb{mkForeign}
176\noindent
177For example, the \texttt{putStr} function is implemented as follows, as a call to
178an external function \texttt{putStr} defined in the run-time system:
180\begin{SaveVerbatim}{putStrex}
182putStr : String -> IO ()
183putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
184\end{SaveVerbatim}
185\useverb{putStrex}
187\subsubsection*{Include and linker directives}
189Foreign function calls are translated directly to calls to C functions, with appropriate
190conversion between the \Idris{} representation of a value and the C representation.
191Often this will require extra libraries to be linked in, or extra header and object files.
192This is made possible through the following directives:
194\begin{itemize}
195\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
196\texttt{-lx} option to \texttt{gcc}.
197\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
198\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.
199\end{itemize}
201\subsection{Cumulativity}
203Since values can appear in types and \emph{vice versa}, it is natural that types themselves
204have types. For example:
206\begin{SaveVerbatim}{typetypes}
208*universe> :t Nat
209Nat : Set
210*universe> :t Vect
211Vect : Set -> Nat -> Set
213\end{SaveVerbatim}
214\useverb{typetypes}
216\noindent
217But what about the type of \texttt{Set}? If we ask \Idris{} it reports
219\begin{SaveVerbatim}{setset}
221*universe> :t Set
222Set : Set
224\end{SaveVerbatim}
225\useverb{setset}
227\noindent
228It \emph{appears} that \texttt{Set} is its own type. This would lead to an inconsitency
229due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
230of types (or \emph{universes}):
232\begin{SaveVerbatim}{sethierarchy}
234Set : Set 1 : Set 2 : Set 3 : ...
236\end{SaveVerbatim}
237\useverb{sethierarchy}
239\noindent
240Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have that
241\texttt{x : Set m}, as long as \texttt{n < m}.
242The typechecker generates such universe
243constraints and reports an error if any inconsistencies are found. Ordinarily, a
244programmer does not need to worry about this, but it does prevent (contrived)
245programs such as the following:
247\begin{SaveVerbatim}{idid}
249myid : (a : Set) -> a -> a
250myid _ x = x
252idid : (a : Set) -> a -> a
253idid = myid _ myid
255\end{SaveVerbatim}
256\useverb{idid}
258\noindent
259The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
260--- \texttt{myid}'s first argument is a \texttt{Set}, which cannot be at a lower level
261than required if it is applied to itself.
263%\subsection{Comparison}
265%How does \Idris{} compare with other dependently typed languages and proof
266%assistants, such as Coq, Agda and Epigram?