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.
17Auto implicit arguments
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
27In other situations, it may be possible to infer arguments not by type
28checking but by searching the context for an appropriate value, or
29constructing a proof. For example, the following definition of ``head``
30which requires a proof that the list is non-empty:
34 isCons : List a -> Bool
36 isCons (x :: xs) = True
38 head : (xs : List a) -> (isCons xs = True) -> a
41If the list is statically known to be non-empty, either because its
42value is known or because a proof already exists in the context, the
43proof can be constructed automatically. Auto implicit arguments allow
44this to happen silently. We define ``head`` as follows:
48 head : (xs : List a) -> {auto p : isCons xs = True} -> a
51The ``auto`` annotation on the implicit argument means that Idris
52will attempt to fill in the implicit argument by searching for a value
53of the appropriate type. It will try the following, in order:
55- Local variables, i.e. names bound in pattern matches or ``let`` bindings,
56 with exactly the right type.
57- The constructors of the required type. If they have arguments, it will
58 search recursively up to a maximum depth of 100.
59- Local variables with function types, searching recursively for the
61- Any function with the appropriate return type which is marked with the
64In the case that a proof is not found, it can be provided explicitly as normal:
68 head xs {p = ?headProof}
70More generally, we can fill in implicit arguments with a default value
71by annotating them with ``default``. The definition above is equivalent
76 head : (xs : List a) ->
77 {default proof { trivial; } p : isCons xs = True} -> a
83Idris supports the creation of *implicit conversions*, which allow
84automatic conversion of values from one type to another when required to
85make a term type correct. This is intended to increase convenience and
86reduce verbosity. A contrived but simple example is the following:
90 implicit intString : Int -> String
94 test x = "Number " ++ x
96In general, we cannot append an ``Int`` to a ``String``, but the
97implicit conversion function ``intString`` can convert ``x`` to a
98``String``, so the definition of ``test`` is type correct. An implicit
99conversion is implemented just like any other function, but given the
100``implicit`` modifier, and restricted to one explicit argument.
102Only one implicit conversion will be applied at a time. That is,
103implicit conversions cannot be chained. Implicit conversions of simple
104types, as above, are however discouraged! More commonly, an implicit
105conversion would be used to reduce verbosity in an embedded domain
106specific language, or to hide details of a proof. Such examples are
107beyond the scope of this tutorial.
112Like Haskell, Idris supports *literate* programming. If a file has
113an extension of ``.lidr`` then it is assumed to be a literate file. In
114literate programs, everything is assumed to be a comment unless the line
115begins with a greater than sign ``>``, for example:
121 This is a comment. The main program is below
124 > main = putStrLn "Hello literate world!\n"
126An additional restriction is that there must be a blank line between a
127program line (beginning with ``>``) and a comment line (beginning with
130Foreign function calls
131======================
133For practical programming, it is often necessary to be able to use
134external libraries, particularly for interfacing with the operating
135system, file system, networking, *et cetera*. Idris provides a
136lightweight foreign function interface for achieving this, as part of
137the prelude. For this, we assume a certain amount of knowledge of C and
138the ``gcc`` compiler. First, we define a datatype which describes the
139external types we can handle:
143 data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
145Each of these corresponds directly to a C type. Respectively: ``int``,
146``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a
147translation to a concrete Idris type, described by the following
152 interpFTy : FTy -> Type
154 interpFTy FFloat = Float
155 interpFTy FChar = Char
156 interpFTy FString = String
160A foreign function is described by a list of input types and a return
161type, which can then be converted to an Idris type:
165 ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
167A foreign function is assumed to be impure, so ``ForeignTy`` builds an
168``IO`` type, for example:
172 Idris> ForeignTy [FInt, FString] FString
173 Int -> String -> IO String : Type
175 Idris> ForeignTy [FInt, FString] FUnit
176 Int -> String -> IO () : Type
178We build a call to a foreign function by giving the name of the
179function, a list of argument types and the return type. The built in
180construct ``mkForeign`` converts this description to a function callable
185 data Foreign : Type -> Type where
186 FFun : String -> (xs:List FTy) -> (t:FTy) ->
187 Foreign (ForeignTy xs t)
189 mkForeign : Foreign x -> x
191Note that the compiler expects ``mkForeign`` to be fully applied to
192build a complete foreign function call. For example, the ``putStr``
193function is implemented as follows, as a call to an external function
194``putStr`` defined in the run-time system:
198 putStr : String -> IO ()
199 putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
201Include and linker directives
202-----------------------------
204Foreign function calls are translated directly to calls to C functions,
205with appropriate conversion between the Idris representation of a
206value and the C representation. Often this will require extra libraries
207to be linked in, or extra header and object files. This is made possible
208through the following directives:
210- ``%lib target x`` — include the ``libx`` library. If the target is
211 ``C`` this is equivalent to passing the ``-lx`` option to ``gcc``. If
212 the target is Java the library will be interpreted as a
213 ``groupId:artifactId:packaging:version`` dependency coordinate for
216- ``%include target x`` — use the header file or import ``x`` for the
217 given back end target.
219- ``%link target x.o`` — link with the object file ``x.o`` when using
220 the given back end target.
222- ``%dynamic x.so`` — dynamically link the interpreter with the shared
225Testing foreign function calls
226------------------------------
228Normally, the Idris interpreter (used for typechecking and at the REPL)
229will not perform IO actions. Additionally, as it neither generates C
230code nor compiles to machine code, the ``%lib``, ``%include`` and
231``%link`` directives have no effect. IO actions and FFI calls can be
232tested using the special REPL command ``:x EXPR``, and C libraries can
233be dynamically loaded in the interpreter by using the ``:dynamic``
234command or the ``%dynamic`` directive. For example:
238 Idris> :dynamic libm.so
239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
240 0.9995736030415051 : Float
245Idris type providers, inspired by F#’s type providers, are a means of
246making our types be “about” something in the world outside of Idris. For
247example, given a type that represents a database schema and a query that
248is checked against it, a type provider could read the schema of a real
249database during type checking.
251Idris type providers use the ordinary execution semantics of Idris to
252run an IO action and extract the result. This result is then saved as a
253constant in the compiled code. It can be a type, in which case it is
254used like any other type, or it can be a value, in which case it can be
255used as any other value, including as an index in types.
257Type providers are still an experimental extension. To enable the
258extension, use the ``%language`` directive:
262 %language TypeProviders
264A provider ``p`` for some type ``t`` is simply an expression of type
265``IO (Provider t)``. The ``%provide`` directive causes the type checker
266to execute the action and bind the result to a name. This is perhaps
267best illustrated with a simple example. The type provider ``fromFile``
268reads a text file. If the file consists of the string ``Int``, then the
269type ``Int`` will be provided. Otherwise, it will provide the type
274 strToType : String -> Type
275 strToType "Int" = Int
278 fromFile : String -> IO (Provider Type)
279 fromFile fname = do Right str <- readFile fname
280 | Left err => pure (Provide Void)
281 pure (Provide (strToType (trim str)))
283We then use the ``%provide`` directive:
287 %provide (T1 : Type) with fromFile "theType"
292If the file named ``theType`` consists of the word ``Int``, then ``foo``
293will be an ``Int``. Otherwise, it will be a ``Nat``. When Idris
294encounters the directive, it first checks that the provider expression
295``fromFile theType`` has type ``IO (Provider Type)``. Next, it executes
296the provider. If the result is ``Provide t``, then ``T1`` is defined as
297``t``. Otherwise, the result is an error.
299Our datatype ``Provider t`` has the following definition:
303 data Provider a = Error String
306We have already seen the ``Provide`` constructor. The ``Error``
307constructor allows type providers to return useful error messages. The
308example in this section was purposefully simple. More complex type
309provider implementations, including a statically-checked SQLite binding,
310are available in an external collection [1]_.
315The default target of Idris is C. Compiling via :
319 $ idris hello.idr -o hello
325 $ idris --codegen C hello.idr -o hello
327When the command above is used, a temporary C source is generated, which
328is then compiled into an executable named ``hello``.
330In order to view the generated C code, compile via :
334 $ idris hello.idr -S -o hello.c
336To turn optimisations on, use the ``%flag C`` pragma within the code, as
344 factorial : Int -> Int
346 factorial n = n * (factorial (n-1))
350 putStrLn $ show $ factorial 3
355Idris is capable of producing *JavaScript* code that can be run in a
356browser as well as in the *NodeJS* environment or alike. One can use the
357FFI to communicate with the *JavaScript* ecosystem.
362Code generation is split into two separate targets. To generate code
363that is tailored for running in the browser issue the following command:
367 $ idris --codegen javascript hello.idr -o hello.js
369The resulting file can be embedded into your HTML just like any other
372Generating code for *NodeJS* is slightly different. Idris outputs a
373*JavaScript* file that can be directly executed via ``node``.
377 $ idris --codegen node hello.idr -o hello
381Take into consideration that the *JavaScript* code generator is using
382``console.log`` to write text to ``stdout``, this means that it will
383automatically add a newline to the end of each string. This behaviour
384does not show up in the *NodeJS* code generator.
389To write a useful application we need to communicate with the outside
390world. Maybe we want to manipulate the DOM or send an Ajax request. For
391this task we can use the FFI. Since most *JavaScript* APIs demand
392callbacks we need to extend the FFI so we can pass functions as
395The *JavaScript* FFI works a little bit differently than the regular
396FFI. It uses positional arguments to directly insert our arguments into
397a piece of *JavaScript* code.
399One could use the primitive addition of *JavaScript* like so:
405 primPlus : Int -> Int -> IO Int
406 primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b
414Notice that the ``%n`` notation qualifies the position of the ``n``-th
415argument given to our foreign function starting from 0. When you need a
416percent sign rather than a position simply use ``%%`` instead.
418Passing functions to a foreign function is very similar. Let’s assume
419that we want to call the following function from the *JavaScript* world:
423 function twice(f, x) {
427We obviously need to pass a function ``f`` here (we can infer it from
428the way we use ``f`` in ``twice``, it would be more obvious if
429*JavaScript* had types).
431The *JavaScript* FFI is able to understand functions as arguments when
432you give it something of type ``FFunction``. The following example code
433calls ``twice`` in *JavaScript* and returns the result to our Idris
440 twice : (Int -> Int) -> Int -> IO Int
441 twice f x = mkForeign (
442 FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt
450The program outputs ``3``, just like we expected.
452Including external *JavaScript* files
453-------------------------------------
455Whenever one is working with *JavaScript* one might want to include
456external libraries or just some functions that she or he wants to call
457via FFI which are stored in external files. The *JavaScript* and
458*NodeJS* code generators understand the ``%include`` directive. Keep in
459mind that *JavaScript* and *NodeJS* are handled as different code
460generators, therefore you will have to state which one you want to
461target. This means that you can include different files for *JavaScript*
462and *NodeJS* in the same Idris source file.
464So whenever you want to add an external *JavaScript* file you can do
471 %include Node "path/to/external.js"
473And for use in the browser:
477 %include JavaScript "path/to/external.js"
479The given files will be added to the top of the generated code.
481Including *NodeJS* modules
482--------------------------
484The *NodeJS* code generator can also include modules with the ``%lib``
491This directive compiles into the following *JavaScript*
493.. code-block:: javascript
495 var fs = require("fs");
497Shrinking down generated *JavaScript*
498-------------------------------------
500Idris can produce very big chunks of *JavaScript* code. However, the
501generated code can be minified using the ``closure-compiler`` from
502Google. Any other minifier is also suitable but ``closure-compiler``
503offers advanced compilation that does some aggressive inlining and code
504elimination. Idris can take full advantage of this compilation mode
505and it’s highly recommended to use it when shipping a *JavaScript*
506application written in Idris.
511Since values can appear in types and *vice versa*, it is natural that
512types themselves have types. For example:
519 Vect : Nat -> Type -> Type
521But what about the type of ``Type``? If we ask Idris it reports
528If ``Type`` were its own type, it would lead to an inconsistency due to
529`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_ , so internally there is a
530*hierarchy* of types (or *universes*):
534 Type : Type 1 : Type 2 : Type 3 : ...
536Universes are *cumulative*, that is, if ``x : Type n`` we can also have
537that ``x : Type m``, as long as ``n < m``. The typechecker generates
538such universe constraints and reports an error if any inconsistencies
539are found. Ordinarily, a programmer does not need to worry about this,
540but it does prevent (contrived) programs such as the following:
544 myid : (a : Type) -> a -> a
547 idid : (a : Type) -> a -> a
550The application of ``myid`` to itself leads to a cycle in the universe
551hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
552at a lower level than required if it is applied to itself.
555 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