7In this section we discuss a variety of additional features:
9+ auto, implicit, and default arguments;
10+ literate programming;
11+ interfacing with external libraries through the foreign function;
15+ the universe hierarchy.
18=======================
20We have already seen implicit arguments, which allows arguments to be
21omitted when they can be inferred by the type checker, e.g.
25 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
27Auto implicit arguments
28------------------------
30In other situations, it may be possible to infer arguments not by type
31checking but by searching the context for an appropriate value, or
32constructing a proof. For example, the following definition of ``head``
33which requires a proof that the list is non-empty:
37 isCons : List a -> Bool
39 isCons (x :: xs) = True
41 head : (xs : List a) -> (isCons xs = True) -> a
44If the list is statically known to be non-empty, either because its
45value is known or because a proof already exists in the context, the
46proof can be constructed automatically. Auto implicit arguments allow
47this to happen silently. We define ``head`` as follows:
51 head : (xs : List a) -> {auto p : isCons xs = True} -> a
54The ``auto`` annotation on the implicit argument means that Idris
55will attempt to fill in the implicit argument by searching for a value
56of the appropriate type. It will try the following, in order:
58- Local variables, i.e. names bound in pattern matches or ``let`` bindings,
59 with exactly the right type.
60- The constructors of the required type. If they have arguments, it will
61 search recursively up to a maximum depth of 100.
62- Local variables with function types, searching recursively for the
64- Any function with the appropriate return type which is marked with the
67In the case that a proof is not found, it can be provided explicitly as normal:
71 head xs {p = ?headProof}
73Default implicit arguments
74---------------------------
76Besides having Idris automatically find a value of a given type, sometimes we
77want to have an implicit argument with a specific default value. In Idris, we can
78do this using the ``default`` annotation. While this is primarily intended to assist
79in automatically constructing a proof where auto fails, or finds an unhelpful value,
80it might be easier to first consider a simpler case, not involving proofs.
82If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
83number as 0), we could write:
87 fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
88 fibonacci {lag} Z = lag
89 fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
91After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
92and will return the 5th fibonacci number. Note that while this works, this is not the
93intended use of the ``default`` annotation. It is included here for illustrative purposes
94only. Usually, ``default`` is used to provide things like a custom proof search script.
100Idris supports the creation of *implicit conversions*, which allow
101automatic conversion of values from one type to another when required to
102make a term type correct. This is intended to increase convenience and
103reduce verbosity. A contrived but simple example is the following:
107 implicit intString : Int -> String
111 test x = "Number " ++ x
113In general, we cannot append an ``Int`` to a ``String``, but the
114implicit conversion function ``intString`` can convert ``x`` to a
115``String``, so the definition of ``test`` is type correct. An implicit
116conversion is implemented just like any other function, but given the
117``implicit`` modifier, and restricted to one explicit argument.
119Only one implicit conversion will be applied at a time. That is,
120implicit conversions cannot be chained. Implicit conversions of simple
121types, as above, are however discouraged! More commonly, an implicit
122conversion would be used to reduce verbosity in an embedded domain
123specific language, or to hide details of a proof. Such examples are
124beyond the scope of this tutorial.
129Like Haskell, Idris supports *literate* programming. If a file has
130an extension of ``.lidr`` then it is assumed to be a literate file. In
131literate programs, everything is assumed to be a comment unless the line
132begins with a greater than sign ``>``, for example:
138 This is a comment. The main program is below
141 > main = putStrLn "Hello literate world!\n"
143An additional restriction is that there must be a blank line between a
144program line (beginning with ``>``) and a comment line (beginning with
147Foreign function calls
148======================
150For practical programming, it is often necessary to be able to use
151external libraries, particularly for interfacing with the operating
152system, file system, networking, *et cetera*. Idris provides a
153lightweight foreign function interface for achieving this, as part of
154the prelude. For this, we assume a certain amount of knowledge of C and
155the ``gcc`` compiler. First, we define a datatype which describes the
156external types we can handle:
160 data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
162Each of these corresponds directly to a C type. Respectively: ``int``,
163``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a
164translation to a concrete Idris type, described by the following
169 interpFTy : FTy -> Type
171 interpFTy FFloat = Double
172 interpFTy FChar = Char
173 interpFTy FString = String
177A foreign function is described by a list of input types and a return
178type, which can then be converted to an Idris type:
182 ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
184A foreign function is assumed to be impure, so ``ForeignTy`` builds an
185``IO`` type, for example:
189 Idris> ForeignTy [FInt, FString] FString
190 Int -> String -> IO String : Type
192 Idris> ForeignTy [FInt, FString] FUnit
193 Int -> String -> IO () : Type
195We build a call to a foreign function by giving the name of the
196function, a list of argument types and the return type. The built in
197construct ``mkForeign`` converts this description to a function callable
202 data Foreign : Type -> Type where
203 FFun : String -> (xs:List FTy) -> (t:FTy) ->
204 Foreign (ForeignTy xs t)
206 mkForeign : Foreign x -> x
208Note that the compiler expects ``mkForeign`` to be fully applied to
209build a complete foreign function call. For example, the ``putStr``
210function is implemented as follows, as a call to an external function
211``putStr`` defined in the run-time system:
215 putStr : String -> IO ()
216 putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
218Include and linker directives
219-----------------------------
221Foreign function calls are translated directly to calls to C functions,
222with appropriate conversion between the Idris representation of a
223value and the C representation. Often this will require extra libraries
224to be linked in, or extra header and object files. This is made possible
225through the following directives:
227- ``%lib target x`` — include the ``libx`` library. If the target is
228 ``C`` this is equivalent to passing the ``-lx`` option to ``gcc``. If
229 the target is Java the library will be interpreted as a
230 ``groupId:artifactId:packaging:version`` dependency coordinate for
233- ``%include target x`` — use the header file or import ``x`` for the
234 given back end target.
236- ``%link target x.o`` — link with the object file ``x.o`` when using
237 the given back end target.
239- ``%dynamic x.so`` — dynamically link the interpreter with the shared
242Testing foreign function calls
243------------------------------
245Normally, the Idris interpreter (used for typechecking and at the REPL)
246will not perform IO actions. Additionally, as it neither generates C
247code nor compiles to machine code, the ``%lib``, ``%include`` and
248``%link`` directives have no effect. IO actions and FFI calls can be
249tested using the special REPL command ``:x EXPR``, and C libraries can
250be dynamically loaded in the interpreter by using the ``:dynamic``
251command or the ``%dynamic`` directive. For example:
255 Idris> :dynamic libm.so
256 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
257 0.9995736030415051 : Double
262Idris type providers, inspired by F#’s type providers, are a means of
263making our types be “about” something in the world outside of Idris. For
264example, given a type that represents a database schema and a query that
265is checked against it, a type provider could read the schema of a real
266database during type checking.
268Idris type providers use the ordinary execution semantics of Idris to
269run an IO action and extract the result. This result is then saved as a
270constant in the compiled code. It can be a type, in which case it is
271used like any other type, or it can be a value, in which case it can be
272used as any other value, including as an index in types.
274Type providers are still an experimental extension. To enable the
275extension, use the ``%language`` directive:
279 %language TypeProviders
281A provider ``p`` for some type ``t`` is simply an expression of type
282``IO (Provider t)``. The ``%provide`` directive causes the type checker
283to execute the action and bind the result to a name. This is perhaps
284best illustrated with a simple example. The type provider ``fromFile``
285reads a text file. If the file consists of the string ``Int``, then the
286type ``Int`` will be provided. Otherwise, it will provide the type
291 strToType : String -> Type
292 strToType "Int" = Int
295 fromFile : String -> IO (Provider Type)
296 fromFile fname = do Right str <- readFile fname
297 | Left err => pure (Provide Void)
298 pure (Provide (strToType (trim str)))
300We then use the ``%provide`` directive:
304 %provide (T1 : Type) with fromFile "theType"
309If the file named ``theType`` consists of the word ``Int``, then ``foo``
310will be an ``Int``. Otherwise, it will be a ``Nat``. When Idris
311encounters the directive, it first checks that the provider expression
312``fromFile theType`` has type ``IO (Provider Type)``. Next, it executes
313the provider. If the result is ``Provide t``, then ``T1`` is defined as
314``t``. Otherwise, the result is an error.
316Our datatype ``Provider t`` has the following definition:
320 data Provider a = Error String
323We have already seen the ``Provide`` constructor. The ``Error``
324constructor allows type providers to return useful error messages. The
325example in this section was purposefully simple. More complex type
326provider implementations, including a statically-checked SQLite binding,
327are available in an external collection [1]_.
332The default target of Idris is C. Compiling via:
336 $ idris hello.idr -o hello
342 $ idris --codegen C hello.idr -o hello
344When the command above is used, a temporary C source is generated, which
345is then compiled into an executable named ``hello``.
347In order to view the generated C code, compile via:
351 $ idris hello.idr -S -o hello.c
353To turn optimisations on, use the ``%flag C`` pragma within the code, as
361 factorial : Int -> Int
363 factorial n = n * (factorial (n-1))
367 putStrLn $ show $ factorial 3
369To compile the generated C with debugging information e.g. to use
370``gdb`` to debug segmentation faults in Idris programs, use the
371``%flag C`` pragma to include debugging symbols, as is shown below:
380Idris is capable of producing *JavaScript* code that can be run in a
381browser as well as in the *NodeJS* environment or alike. One can use the
382FFI to communicate with the *JavaScript* ecosystem.
387Code generation is split into two separate targets. To generate code
388that is tailored for running in the browser issue the following command:
392 $ idris --codegen javascript hello.idr -o hello.js
394The resulting file can be embedded into your HTML just like any other
397Generating code for *NodeJS* is slightly different. Idris outputs a
398*JavaScript* file that can be directly executed via ``node``.
402 $ idris --codegen node hello.idr -o hello
406Take into consideration that the *JavaScript* code generator is using
407``console.log`` to write text to ``stdout``, this means that it will
408automatically add a newline to the end of each string. This behaviour
409does not show up in the *NodeJS* code generator.
414To write a useful application we need to communicate with the outside
415world. Maybe we want to manipulate the DOM or send an Ajax request. For
416this task we can use the FFI. Since most *JavaScript* APIs demand
417callbacks we need to extend the FFI so we can pass functions as
420The *JavaScript* FFI works a little bit differently than the regular
421FFI. It uses positional arguments to directly insert our arguments into
422a piece of *JavaScript* code.
424One could use the primitive addition of *JavaScript* like so:
430 primPlus : Int -> Int -> IO Int
431 primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b
439Notice that the ``%n`` notation qualifies the position of the ``n``-th
440argument given to our foreign function starting from 0. When you need a
441percent sign rather than a position simply use ``%%`` instead.
443Passing functions to a foreign function is very similar. Let’s assume
444that we want to call the following function from the *JavaScript* world:
448 function twice(f, x) {
452We obviously need to pass a function ``f`` here (we can infer it from
453the way we use ``f`` in ``twice``, it would be more obvious if
454*JavaScript* had types).
456The *JavaScript* FFI is able to understand functions as arguments when
457you give it something of type ``FFunction``. The following example code
458calls ``twice`` in *JavaScript* and returns the result to our Idris
465 twice : (Int -> Int) -> Int -> IO Int
466 twice f x = mkForeign (
467 FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt
475The program outputs ``3``, just like we expected.
477Including external *JavaScript* files
478-------------------------------------
480Whenever one is working with *JavaScript* one might want to include
481external libraries or just some functions that she or he wants to call
482via FFI which are stored in external files. The *JavaScript* and
483*NodeJS* code generators understand the ``%include`` directive. Keep in
484mind that *JavaScript* and *NodeJS* are handled as different code
485generators, therefore you will have to state which one you want to
486target. This means that you can include different files for *JavaScript*
487and *NodeJS* in the same Idris source file.
489So whenever you want to add an external *JavaScript* file you can do
496 %include Node "path/to/external.js"
498And for use in the browser:
502 %include JavaScript "path/to/external.js"
504The given files will be added to the top of the generated code.
505For library packages you can also use the ipkg objs option to include the
506js file in the installation, and use:
510 %include Node "package/external.js"
512The *JavaScript* and *NodeJS* backends of Idris will also lookup for the file
515Including *NodeJS* modules
516--------------------------
518The *NodeJS* code generator can also include modules with the ``%lib``
525This directive compiles into the following *JavaScript*
527.. code-block:: javascript
529 var fs = require("fs");
531Shrinking down generated *JavaScript*
532-------------------------------------
534Idris can produce very big chunks of *JavaScript* code. However, the
535generated code can be minified using the ``closure-compiler`` from
536Google. Any other minifier is also suitable but ``closure-compiler``
537offers advanced compilation that does some aggressive inlining and code
538elimination. Idris can take full advantage of this compilation mode
539and it’s highly recommended to use it when shipping a *JavaScript*
540application written in Idris.
545Since values can appear in types and *vice versa*, it is natural that
546types themselves have types. For example:
553 Vect : Nat -> Type -> Type
555But what about the type of ``Type``? If we ask Idris it reports:
562If ``Type`` were its own type, it would lead to an inconsistency due to
563`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
564so internally there is a *hierarchy* of types (or *universes*):
568 Type : Type 1 : Type 2 : Type 3 : ...
570Universes are *cumulative*, that is, if ``x : Type n`` we can also have
571that ``x : Type m``, as long as ``n < m``. The typechecker generates
572such universe constraints and reports an error if any inconsistencies
573are found. Ordinarily, a programmer does not need to worry about this,
574but it does prevent (contrived) programs such as the following:
578 myid : (a : Type) -> a -> a
581 idid : (a : Type) -> a -> a
584The application of ``myid`` to itself leads to a cycle in the universe
585hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
586at a lower level than required if it is applied to itself.
589 https://github.com/david-christiansen/idris-type-providers
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