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 using the ``trivial``
53tactic, which searches through the context for a proof, and tries to
54solve with ``refl`` if a proof is not found. Now when ``head`` is
55applied, the proof can be omitted. In the case that a proof is not
56found, it can be provided explicitly as normal:
60 head xs {p = ?headProof}
62More generally, we can fill in implicit arguments with a default value
63by annotating them with ``default``. The definition above is equivalent
68 head : (xs : List a) ->
69 {default proof { trivial; } p : isCons xs = True} -> a
75Idris supports the creation of *implicit conversions*, which allow
76automatic conversion of values from one type to another when required to
77make a term type correct. This is intended to increase convenience and
78reduce verbosity. A contrived but simple example is the following:
82 implicit intString : Int -> String
86 test x = "Number " ++ x
88In general, we cannot append an ``Int`` to a ``String``, but the
89implicit conversion function ``intString`` can convert ``x`` to a
90``String``, so the definition of ``test`` is type correct. An implicit
91conversion is implemented just like any other function, but given the
92``implicit`` modifier, and restricted to one explicit argument.
94Only one implicit conversion will be applied at a time. That is,
95implicit conversions cannot be chained. Implicit conversions of simple
96types, as above, are however discouraged! More commonly, an implicit
97conversion would be used to reduce verbosity in an embedded domain
98specific language, or to hide details of a proof. Such examples are
99beyond the scope of this tutorial.
104Like Haskell, Idris supports *literate* programming. If a file has
105an extension of ``.lidr`` then it is assumed to be a literate file. In
106literate programs, everything is assumed to be a comment unless the line
107begins with a greater than sign ``>``, for example:
113 This is a comment. The main program is below
116 > main = putStrLn "Hello literate world!\n"
118An additional restriction is that there must be a blank line between a
119program line (beginning with ``>``) and a comment line (beginning with
122Foreign function calls
123======================
125For practical programming, it is often necessary to be able to use
126external libraries, particularly for interfacing with the operating
127system, file system, networking, *et cetera*. Idris provides a
128lightweight foreign function interface for achieving this, as part of
129the prelude. For this, we assume a certain amount of knowledge of C and
130the ``gcc`` compiler. First, we define a datatype which describes the
131external types we can handle:
135 data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
137Each of these corresponds directly to a C type. Respectively: ``int``,
138``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a
139translation to a concrete Idris type, described by the following
144 interpFTy : FTy -> Type
146 interpFTy FFloat = Float
147 interpFTy FChar = Char
148 interpFTy FString = String
152A foreign function is described by a list of input types and a return
153type, which can then be converted to an Idris type:
157 ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
159A foreign function is assumed to be impure, so ``ForeignTy`` builds an
160``IO`` type, for example:
164 Idris> ForeignTy [FInt, FString] FString
165 Int -> String -> IO String : Type
167 Idris> ForeignTy [FInt, FString] FUnit
168 Int -> String -> IO () : Type
170We build a call to a foreign function by giving the name of the
171function, a list of argument types and the return type. The built in
172construct ``mkForeign`` converts this description to a function callable
177 data Foreign : Type -> Type where
178 FFun : String -> (xs:List FTy) -> (t:FTy) ->
179 Foreign (ForeignTy xs t)
181 mkForeign : Foreign x -> x
183Note that the compiler expects ``mkForeign`` to be fully applied to
184build a complete foreign function call. For example, the ``putStr``
185function is implemented as follows, as a call to an external function
186``putStr`` defined in the run-time system:
190 putStr : String -> IO ()
191 putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
193Include and linker directives
194-----------------------------
196Foreign function calls are translated directly to calls to C functions,
197with appropriate conversion between the Idris representation of a
198value and the C representation. Often this will require extra libraries
199to be linked in, or extra header and object files. This is made possible
200through the following directives:
202- ``%lib target x`` — include the ``libx`` library. If the target is
203 ``C`` this is equivalent to passing the ``-lx`` option to ``gcc``. If
204 the target is Java the library will be interpreted as a
205 ``groupId:artifactId:packaging:version`` dependency coordinate for
208- ``%include target x`` — use the header file or import ``x`` for the
209 given back end target.
211- ``%link target x.o`` — link with the object file ``x.o`` when using
212 the given back end target.
214- ``%dynamic x.so`` — dynamically link the interpreter with the shared
217Testing foreign function calls
218------------------------------
220Normally, the Idris interpreter (used for typechecking and at the REPL)
221will not perform IO actions. Additionally, as it neither generates C
222code nor compiles to machine code, the ``%lib``, ``%include`` and
223``%link`` directives have no effect. IO actions and FFI calls can be
224tested using the special REPL command ``:x EXPR``, and C libraries can
225be dynamically loaded in the interpreter by using the ``:dynamic``
226command or the ``%dynamic`` directive. For example:
230 Idris> :dynamic libm.so
231 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
232 0.9995736030415051 : Float
237Idris type providers, inspired by F#’s type providers, are a means of
238making our types be “about” something in the world outside of Idris. For
239example, given a type that represents a database schema and a query that
240is checked against it, a type provider could read the schema of a real
241database during type checking.
243Idris type providers use the ordinary execution semantics of Idris to
244run an IO action and extract the result. This result is then saved as a
245constant in the compiled code. It can be a type, in which case it is
246used like any other type, or it can be a value, in which case it can be
247used as any other value, including as an index in types.
249Type providers are still an experimental extension. To enable the
250extension, use the ``%language`` directive:
254 %language TypeProviders
256A provider ``p`` for some type ``t`` is simply an expression of type
257``IO (Provider t)``. The ``%provide`` directive causes the type checker
258to execute the action and bind the result to a name. This is perhaps
259best illustrated with a simple example. The type provider ``fromFile``
260reads a text file. If the file consists of the string ``Int``, then the
261type ``Int`` will be provided. Otherwise, it will provide the type
266 strToType : String -> Type
267 strToType "Int" = Int
270 fromFile : String -> IO (Provider Type)
271 fromFile fname = do str <- readFile fname
272 return (Provide (strToType (trim str)))
274We then use the ``%provide`` directive:
278 %provide (T1 : Type) with fromFile "theType"
283If the file named ``theType`` consists of the word ``Int``, then ``foo``
284will be an ``Int``. Otherwise, it will be a ``Nat``. When Idris
285encounters the directive, it first checks that the provider expression
286``fromFile theType`` has type ``IO (Provider Type)``. Next, it executes
287the provider. If the result is ``Provide t``, then ``T1`` is defined as
288``t``. Otherwise, the result is an error.
290Our datatype ``Provider t`` has the following definition:
294 data Provider a = Error String
297We have already seen the ``Provide`` constructor. The ``Error``
298constructor allows type providers to return useful error messages. The
299example in this section was purposefully simple. More complex type
300provider implementations, including a statically-checked SQLite binding,
301are available in an external collection [1]_.
306The default target of Idris is C. Compiling via :
310 $ idris hello.idr -o hello
316 $ idris --codegen C hello.idr -o hello
318When the command above is used, a temporary C source is generated, which
319is then compiled into an executable named ``hello``.
321In order to view the generated C code, compile via :
325 $ idris hello.idr -S -o hello.c
327To turn optimisations on, use the ``%flag C`` pragma within the code, as
335 factorial : Int -> Int
337 factorial n = n * (factorial (n-1))
341 putStrLn $ show $ factorial 3
346Idris is capable of producing *JavaScript* code that can be run in a
347browser as well as in the *NodeJS* environment or alike. One can use the
348FFI to communicate with the *JavaScript* ecosystem.
353Code generation is split into two separate targets. To generate code
354that is tailored for running in the browser issue the following command:
358 $ idris --codegen javascript hello.idr -o hello.js
360The resulting file can be embedded into your HTML just like any other
363Generating code for *NodeJS* is slightly different. Idris outputs a
364*JavaScript* file that can be directly executed via ``node``.
368 $ idris --codegen node hello.idr -o hello
372Take into consideration that the *JavaScript* code generator is using
373``console.log`` to write text to ``stdout``, this means that it will
374automatically add a newline to the end of each string. This behaviour
375does not show up in the *NodeJS* code generator.
380To write a useful application we need to communicate with the outside
381world. Maybe we want to manipulate the DOM or send an Ajax request. For
382this task we can use the FFI. Since most *JavaScript* APIs demand
383callbacks we need to extend the FFI so we can pass functions as
386The *JavaScript* FFI works a little bit differently than the regular
387FFI. It uses positional arguments to directly insert our arguments into
388a piece of *JavaScript* code.
390One could use the primitive addition of *JavaScript* like so:
396 primPlus : Int -> Int -> IO Int
397 primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b
405Notice that the ``%n`` notation qualifies the position of the ``n``-th
406argument given to our foreign function starting from 0. When you need a
407percent sign rather than a position simply use ``%%`` instead.
409Passing functions to a foreign function is very similar. Let’s assume
410that we want to call the following function from the *JavaScript* world:
414 function twice(f, x) {
418We obviously need to pass a function ``f`` here (we can infer it from
419the way we use ``f`` in ``twice``, it would be more obvious if
420*JavaScript* had types).
422The *JavaScript* FFI is able to understand functions as arguments when
423you give it something of type ``FFunction``. The following example code
424calls ``twice`` in *JavaScript* and returns the result to our Idris
431 twice : (Int -> Int) -> Int -> IO Int
432 twice f x = mkForeign (
433 FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt
441The program outputs ``3``, just like we expected.
443Including external *JavaScript* files
444-------------------------------------
446Whenever one is working with *JavaScript* one might want to include
447external libraries or just some functions that she or he wants to call
448via FFI which are stored in external files. The *JavaScript* and
449*NodeJS* code generators understand the ``%include`` directive. Keep in
450mind that *JavaScript* and *NodeJS* are handled as different code
451generators, therefore you will have to state which one you want to
452target. This means that you can include different files for *JavaScript*
453and *NodeJS* in the same Idris source file.
455So whenever you want to add an external *JavaScript* file you can do
462 %include Node "path/to/external.js"
464And for use in the browser:
468 %include JavaScript "path/to/external.js"
470The given files will be added to the top of the generated code.
472Including *NodeJS* modules
473--------------------------
475The *NodeJS* code generator can also include modules with the ``%lib``
482This directive compiles into the following *JavaScript*
484.. code-block:: javascript
486 var fs = require("fs");
488Shrinking down generated *JavaScript*
489-------------------------------------
491Idris can produce very big chunks of *JavaScript* code. However, the
492generated code can be minified using the ``closure-compiler`` from
493Google. Any other minifier is also suitable but ``closure-compiler``
494offers advanced compilation that does some aggressive inlining and code
495elimination. Idris can take full advantage of this compilation mode
496and it’s highly recommended to use it when shipping a *JavaScript*
497application written in Idris.
502Since values can appear in types and *vice versa*, it is natural that
503types themselves have types. For example:
510 Vect : Nat -> Type -> Type
512But what about the type of ``Type``? If we ask Idris it reports
519If ``Type`` were its own type, it would lead to an inconsistency due to
520`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_ , so internally there is a
521*hierarchy* of types (or *universes*):
525 Type : Type 1 : Type 2 : Type 3 : ...
527Universes are *cumulative*, that is, if ``x : Type n`` we can also have
528that ``x : Type m``, as long as ``n < m``. The typechecker generates
529such universe constraints and reports an error if any inconsistencies
530are found. Ordinarily, a programmer does not need to worry about this,
531but it does prevent (contrived) programs such as the following:
535 myid : (a : Type) -> a -> a
538 idid : (a : Type) -> a -> a
541The application of ``myid`` to itself leads to a cycle in the universe
542hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
543at a lower level than required if it is applied to itself.
546 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