3In this section we discuss a variety of additional features:
4auto implicit and default
5arguments, literate programming, interfacing with external libraries through the
6foreign function interface, type providers, 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 target "x"} --- include the \texttt{libx} library. If the target is \texttt{C} this is equivalent to passing the
228\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a
229"groupId:artifactId:packaging:version" dependency coordinate for maven.
230\item \texttt{\%include target "x"} --- use the header file or import \texttt{x} for the given back end target.
231\item \texttt{\%link target "x.o"} --- link with the object file \texttt{x.o} when using the given back end target.
232\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
235\subsubsection*{Testing foreign function calls}
236Normally, the Idris interpreter (used for typechecking and at the REPL) will
237not perform IO actions. Additionally, as it neither generates C code nor
238compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and
239\texttt{\%link} directives have no effect. IO actions and FFI calls can be
240tested using the special REPL command \texttt{:x EXPR}, and C libraries can be
241dynamically loaded in the interpreter by using the \texttt{:dynamic} command
242or the \texttt{\%dynamic} directive. For example:
244\begin{SaveVerbatim}{xdynamic}
246Idris> :dynamic libm.so
247Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
2480.9995736030415051 : Float
253\subsection{Type Providers}
254Idris type providers, inspired by F\#'s type providers, are a means of making
255our types be ``about'' something in the world outside of Idris. For example,
256given a type that represents a database schema and a query that is checked
257against it, a type provider could read the schema of a real database during
260Idris type providers use the ordinary execution semantics of Idris to run an
261IO action and extract the result. This result is then saved as a constant in
262the compiled code. It can be a type, in which case it is used like any other
263type, or it can be a value, in which case it can be used as any other value,
264including as an index in types.
266Type providers are still an experimental extension. To enable the extension,
267use the \texttt{\%language} directive:
268\begin{SaveVerbatim}{languageProv}
270%language TypeProviders
274\useverb{languageProv}
277A provider \texttt{p} for some type \texttt{t} is simply an expression of type
278\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type
279checker to execute the action and bind the result to a name. This is perhaps
280best illustrated with a simple example. The type provider \texttt{fromFile}
281reads a text file. If the file consists of the string \texttt{"Int"}, then the
282type \texttt{Int} will be provided. Otherwise, it will provide the type
285\begin{SaveVerbatim}{fromFile}
287strToType : String -> Type
291fromFile : String -> IO (Provider Type)
292fromFile fname = do str <- readFile fname
293 return (Provide (strToType (trim str)))
298We then use the \texttt{\%provide} directive:
300\begin{SaveVerbatim}{fromFileUse}
302%provide (T1 : Type) with fromFile "theType"
311If the file named \texttt{theType} consists of the word \texttt{Int}, then
312\texttt{foo} will be an \texttt{Int}. Otherwise, it will be a \texttt{Nat}.
313When Idris encounters the directive, it first checks that the provider
314expression \texttt{fromFile "theType"} has type \texttt{IO (Provider
315 Type)}. Next, it executes the provider. If the result is \texttt{Provide t},
316then \texttt{T1} is defined as \texttt{t}. Otherwise, the result is an error.
318Our datatype \texttt{Provider t} has the following definition:
320\begin{SaveVerbatim}{providerdef}
322data Provider a = Error String
329We have already seen the \texttt{Provide} constructor. The \texttt{Error}
330constructor allows type providers to return useful error messages. The
331example in this section was purposefully simple. More complex type provider
332implementations, including a statically-checked SQLite binding, are available
333in an external collection.\footnote{\url{https://github.com/david-christiansen/idris-type-providers}}
335\subsection{Cumulativity}
337Since values can appear in types and \emph{vice versa}, it is natural that types themselves
338have types. For example:
340\begin{SaveVerbatim}{typetypes}
345Vect : Nat -> Type -> Type
351But what about the type of \texttt{Type}? If we ask \Idris{} it reports
353\begin{SaveVerbatim}{setset}
362If \texttt{Type} were its own type, it would lead to an inconsitency
363due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
364of types (or \emph{universes}):
366\begin{SaveVerbatim}{sethierarchy}
368Type : Type 1 : Type 2 : Type 3 : ...
371\useverb{sethierarchy}
374Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that
375\texttt{x : Type m}, as long as \texttt{n < m}.
376The typechecker generates such universe
377constraints and reports an error if any inconsistencies are found. Ordinarily, a
378programmer does not need to worry about this, but it does prevent (contrived)
379programs such as the following:
381\begin{SaveVerbatim}{idid}
383myid : (a : Type) -> a -> a
386idid : (a : Type) -> a -> a
393The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
394--- \texttt{myid}'s first argument is a \texttt{Type}, which cannot be at a lower level
395than required if it is applied to itself.
397%\subsection{Comparison}
399%How does \Idris{} compare with other dependently typed languages and proof
400%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