3In this section we discuss a variety of additional features: extensible syntax,
4auto implicit and default
5arguments, literate programming, interfacing with external libraries through the
6foriegn function interface, and the universe hierarchy.
10\subsection{Auto implicit arguments}
12We have already seen implicit arguments, which allows arguments to be omitted when
13they can be inferred by the type checker, e.g.
18In other situations, it may be possible to infer arguments not by type checking but
19by searching the context for an appropriate value, or constructing a proof. For example,
20the following definition of \texttt{head} which requires a proof that the list is
23\begin{SaveVerbatim}{safehead}
25isCons : List a -> Bool
27isCons (x :: xs) = True
29head : (xs : List a) -> (isCons xs = True) -> a
36If the list is statically known to be non-empty, either because its value is known or
37because a proof already exists in the context, the proof can be constructed
38automatically. Auto implicit arguments allow this to happen silently. We define
39\texttt{head} as follows:
41\begin{SaveVerbatim}{headauto}
43head : (xs : List a) -> {auto p : isCons xs = True} -> a
50The \texttt{auto} annotation on the implicit argument means that \Idris{} will
51attempt to fill in the implicit argument using the \texttt{trivial} tactic, which
52searches through the context for a proof, and tries to solve with \texttt{refl}
53if a proof is not found.
54Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof
55is not found, it can be provided explicitly as normal:
57\begin{SaveVerbatim}{headapp}
59head xs {p = ?headProof}
65More generally, we can fill in implicit arguments with a default value by annotating
66them with \texttt{default}. The definition above is equivalent to:
68\begin{SaveVerbatim}{defimp}
70head : (xs : List a) ->
71 {default proof { trivial; } p : isCons xs = True} -> a
77\subsection{Literate programming}
79Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
80extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
81programs, everything is assumed to be a comment unless the line begins with a
82greater than sign \texttt{>}, for example:
84\begin{SaveVerbatim}{litidr}
88This is a comment. The main program is below
91> main = putStrLn "Hello literate world!\n"
97An additional restriction is that there must be a blank line between a program
98line (beginning with \texttt{>}) and a comment line (beginning with any other
101\subsection{Foreign function calls}
103For practical programming, it is often necessary to be able to use external libraries,
104particularly for interfacing with the operating system, file system, networking, etc.
105\Idris{} provides a lightweight foreign function interface for achieving this,
106as part of the prelude. For this, we assume a certain amount of knowledge of
107C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
110\begin{SaveVerbatim}{foreignty}
112data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
118Each of these corresponds directly to a C type. Respectively: \texttt{int},
119\texttt{float}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
120There is also a translation to a concrete \Idris{} type, described by the
123\begin{SaveVerbatim}{interpfty}
125interpFTy : FTy -> Set
127interpFTy FFloat = Float
128interpFTy FChar = Char
129interpFTy FString = String
137A foreign function is described by a list of input types and a return type, which
138can then be converted to an \Idris{} type:
140\begin{SaveVerbatim}{ffunty}
142ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
148A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
149\texttt{IO} type, for example:
151\begin{SaveVerbatim}{ftyex}
153Idris> ForeignTy [FInt, FString] FString
154Int -> String -> IO String : Set
156Idris> ForeignTy [FInt, FString] FUnit
157Int -> String -> IO () : Set
163We build a call to a foreign function by giving the name of the function, a list of
164argument types and the return type. The built in function \texttt{mkForeign}
165converts this description to a function callable by \Idris{}
167\begin{SaveVerbatim}{mkForeign}
169data Foreign : Set -> Set where
170 FFun : String -> (xs:List FTy) -> (t:FTy) ->
171 Foreign (ForeignTy xs t)
173mkForeign : Foreign x -> x
179For example, the \texttt{putStr} function is implemented as follows, as a call to
180an external function \texttt{putStr} defined in the run-time system:
182\begin{SaveVerbatim}{putStrex}
184putStr : String -> IO ()
185putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
189\subsubsection*{Include and linker directives}
191Foreign function calls are translated directly to calls to C functions, with appropriate
192conversion between the \Idris{} representation of a value and the C representation.
193Often this will require extra libraries to be linked in, or extra header and object files.
194This is made possible through the following directives:
197\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
198\texttt{-lx} option to \texttt{gcc}.
199\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
200\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
203\subsection{Cumulativity}
205Since values can appear in types and \emph{vice versa}, it is natural that types themselves
206have types. For example:
208\begin{SaveVerbatim}{typetypes}
213Vect : Set -> Nat -> Set
219But what about the type of \texttt{Set}? If we ask \Idris{} it reports
221\begin{SaveVerbatim}{setset}
230It \emph{appears} that \texttt{Set} is its own type. This would lead to an inconsitency
231due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
232of types (or \emph{universes}):
234\begin{SaveVerbatim}{sethierarchy}
236Set : Set 1 : Set 2 : Set 3 : ...
239\useverb{sethierarchy}
242Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have that
243\texttt{x : Set m}, as long as \texttt{n < m}.
244The typechecker generates such universe
245constraints and reports an error if any inconsistencies are found. Ordinarily, a
246programmer does not need to worry about this, but it does prevent (contrived)
247programs such as the following:
249\begin{SaveVerbatim}{idid}
251myid : (a : Set) -> a -> a
254idid : (a : Set) -> a -> a
261The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
262--- \texttt{myid}'s first argument is a \texttt{Set}, which cannot be at a lower level
263than required if it is applied to itself.
265%\subsection{Comparison}
267%How does \Idris{} compare with other dependently typed languages and proof
268%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