10``Idris`` defines several primitive types: ``Int``, ``Integer`` and
11``Float`` for numeric operations, ``Char`` and ``String`` for text
12manipulation, and ``Ptr`` which represents foreign pointers. There are
13also several data types declared in the library, including ``Bool``,
14with values ``True`` and ``False``. We can declare some constants with
15these types. Enter the following into a file ``prims.idr`` and load it
16into the ``Idris`` interactive environment by typing
27 foo = "Sausage machine"
35An ``Idris`` file consists of an optional module declaration (here
36``module prims``) followed by an optional list of imports (none here,
37however ``Idris`` programs can consist of several modules, and the
38definitions in each module each have their own namespace, as we will
39discuss in Section :ref:`sect-namespaces`) and a collection of declarations
40and definitions. The order of definitions is significant — functions and
41data types must be defined before use. Each definition must have a type
42declaration, for example see ``x : Int``, ``foo : String``, from the
43above listing. Indentation is significant — a new declaration begins at
44the same level of indentation as the preceding declaration.
45Alternatively, declarations may be terminated with a semicolon.
47A library module ``prelude`` is automatically imported by every
48``Idris`` program, including facilities for IO, arithmetic, data
49structures and various common functions. The prelude defines several
50arithmetic and comparison operators, which we can use at the prompt.
51Evaluating things at the prompt gives an answer, and the type of the
61All of the usual arithmetic and comparison operators are defined for the
62primitive types. They are overloaded using type classes, as we will
63discuss in Section :ref:`sect-classes` and can be extended to work on user
64defined types. Boolean expressions can be tested with the
65``if...then...else`` construct:
69 *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
70 "The answer!" : String
75Data types are declared in a similar way to Haskell data types, with a
76similar syntax. Natural numbers and lists, for example, can be declared
81 data Nat = Z | S Nat -- Natural numbers
82 -- (zero and successor)
83 data List a = Nil | (::) a (List a) -- Polymorphic lists
85The above declarations are taken from the standard library. Unary
86natural numbers can be either zero (``Z``), or the successor of another
87natural number (``S k``). Lists can either be empty (``Nil``) or a value
88added to the front of another list (``x :: xs``). In the declaration for
89``List``, we used an infix operator ``::``. New operators such as this
90can be added using a fixity declaration, as follows:
96Functions, data constructors and type constructors may all be given
97infix operators as names. They may be used in prefix form if enclosed in
98brackets, e.g. \ ``(::)``. Infix operators can use any of the symbols:
107Functions are implemented by pattern matching, again using a similar
108syntax to Haskell. The main difference is that ``Idris`` requires type
109declarations for all functions, using a single colon ``:`` (rather than
110Haskell’s double colon ``::``). Some natural number arithmetic functions
111can be defined as follows, again taken from the standard library:
116 plus : Nat -> Nat -> Nat
118 plus (S k) y = S (plus k y)
120 -- Unary multiplication
121 mult : Nat -> Nat -> Nat
123 mult (S k) y = plus y (mult k y)
125The standard arithmetic operators ``+`` and ``*`` are also overloaded
126for use by ``Nat``, and are implemented using the above functions.
127Unlike Haskell, there is no restriction on whether types and function
128names must begin with a capital letter or not. Function names (``plus``
129and ``mult`` above), data constructors (``Z``, ``S``, ``Nil`` and
130``::``) and type constructors (``Nat`` and ``List``) are all part of the
131same namespace. We can test these functions at the ``Idris`` prompt:
135 Idris> plus (S (S Z)) (S (S Z))
137 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
140**Note:** ``Idris`` automatically desugars the ``Nat`` representation
141into a more human readable format. The result of
142``plus (S (S Z)) (S (S Z))`` is actually ``(S (S (S (S Z))))`` which is
143the Integer 4. This can be checked at the ``Idris`` prompt:
147 Idris> (S (S (S (S Z))))
150Like arithmetic operations, integer literals are also overloaded using
151type classes, meaning that we can also test the functions as follows:
157 Idris> mult 3 (plus 2 2)
160You may wonder, by the way, why we have unary natural numbers when our
161computers have perfectly good integer arithmetic built in. The reason is
162primarily that unary numbers have a very convenient structure which is
163easy to reason about, and easy to relate to other data structures as we
164will see later. Nevertheless, we do not want this convenience to be at
165the expense of efficiency. Fortunately, ``Idris`` knows about the
166relationship between ``Nat`` (and similarly structured types) and
167numbers. This means it can optimise the representation, and functions
168such as ``plus`` and ``mult``.
173Functions can also be defined *locally* using ``where`` clauses. For
174example, to define a function which reverses a list, we can use an
175auxiliary function which accumulates the new, reversed list, and which
176does not need to be visible globally:
180 reverse : List a -> List a
181 reverse xs = revAcc [] xs where
182 revAcc : List a -> List a -> List a
184 revAcc acc (x :: xs) = revAcc (x :: acc) xs
186Indentation is significant — functions in the ``where`` block must be
187indented further than the outer function.
189**Scope:** Any names which are visible in the outer scope are also
190visible in the ``where`` clause (unless they have been redefined, such
191as ``xs`` here). A name which appears only in the type will be in scope
192in the ``where`` clause if it is a *parameter* to one of the types,
193i.e. it is fixed across the entire structure.
195As well as functions, ``where`` blocks can include local data
196declarations, such as the following where ``MyLT`` is not accessible
197outside the definition of ``foo``:
209 isLT = if x < 20 then Yes else No
211In general, functions defined in a ``where`` clause need a type
212declaration just like any top level function. However, the type
213declaration for a function ``f`` *can* be omitted if:
215- ``f`` appears in the right hand side of the top level definition
217- The type of ``f`` can be completely determined from its first
220So, for example, the following definitions are legal:
226 even (S k) = odd k where
231 test = [c (S 1), c Z, d (S Z)]
233 d y = c (y + 1 + z y)
242A standard example of a dependent type is the type of “lists with
243length”, conventionally called vectors in the dependent type literature.
244They are available as part of the ``Idris`` library, by importing
245``Data.Vect``, or we can declare them as follows:
249 data Vect : Nat -> Type -> Type where
251 (::) : a -> Vect k a -> Vect (S k) a
253Note that we have used the same constructor names as for ``List``.
254Ad-hoc name overloading such as this is accepted by ``Idris``, provided
255that the names are declared in different namespaces (in practice,
256normally in different modules). Ambiguous constructor names can normally
257be resolved from context.
259This declares a family of types, and so the form of the declaration is
260rather different from the simple type declarations above. We explicitly
261state the type of the type constructor ``Vect`` — it takes a ``Nat`` and
262a type as an argument, where ``Type`` stands for the type of types. We
263say that ``Vect`` is *indexed* over ``Nat`` and *parameterised* by
264``Type``. Each constructor targets a different part of the family of
265types. ``Nil`` can only be used to construct vectors with zero length,
266and ``::`` to construct vectors with non-zero length. In the type of
267``::``, we state explicitly that an element of type ``a`` and a tail of
268type ``Vect k a`` (i.e., a vector of length ``k``) combine to make a
269vector of length ``S k``.
271We can define functions on dependent types such as ``Vect`` in the same
272way as on simple types such as ``List`` and ``Nat`` above, by pattern
273matching. The type of a function over ``Vect`` will describe what
274happens to the lengths of the vectors involved. For example, ``++``,
275defined as follows, appends two ``Vect``\ s:
279 (++) : Vect n a -> Vect m a -> Vect (n + m) a
281 (++) (x :: xs) ys = x :: xs ++ ys
283The type of ``(++)`` states that the resulting vector’s length will be
284the sum of the input lengths. If we get the definition wrong in such a
285way that this does not hold, ``Idris`` will not accept the definition.
290 (++) : Vect n a -> Vect m a -> Vect (n + m) a
292 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
294When run through the ``Idris`` type checker, this results in the
299 $ idris vbroken.idr --check
300 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
301 When elaborating an application of constructor Vect.:::
313This error message suggests that there is a length mismatch between two
314vectors — we needed a vector of length ``k + m``, but provided a vector
320Finite sets, as the name suggests, are sets with a finite number of
321elements. They are available as part of the ``Idris`` library, by
322importing ``Data.Fin``, or can be declared as follows:
326 data Fin : Nat -> Type where
328 FS : Fin k -> Fin (S k)
330``FZ`` is the zeroth element of a finite set with ``S k`` elements;
331``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
332elements. ``Fin`` is indexed by a ``Nat``, which represents the number
333of elements in the set. Obviously we can’t construct an element of an
334empty set, so neither constructor targets ``Fin Z``.
336A useful application of the ``Fin`` family is to represent bounded
337natural numbers. Since the first ``n`` natural numbers form a finite set
338of ``n`` elements, we can treat ``Fin n`` as the set of natural numbers
341For example, the following function which looks up an element in a
342``Vect``, by a bounded index given as a ``Fin n``, is defined in the
347 index : Fin n -> Vect n a -> a
348 index FZ (x :: xs) = x
349 index (FS k) (x :: xs) = index k xs
351This function looks up a value at a given location in a vector. The
352location is bounded by the length of the vector (``n`` in each case), so
353there is no need for a run-time bounds check. The type checker
354guarantees that the location is no larger than the length of the vector.
356Note also that there is no case for ``Nil`` here. This is because it is
357impossible. Since there is no element of ``Fin Z``, and the location is
358a ``Fin n``, then ``n`` can not be ``Z``. As a result, attempting to
359look up an element in an empty vector would give a compile time type
360error, since it would force ``n`` to be ``Z``.
365Let us take a closer look at the type of ``index``:
369 index : Fin n -> Vect n a -> a
371It takes two arguments, an element of the finite set of ``n`` elements,
372and a vector with ``n`` elements of type ``a``. But there are also two
373names, ``n`` and ``a``, which are not declared explicitly. These are
374*implicit* arguments to ``index``. We could also write the type of
379 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
381Implicit arguments, given in braces ``{}`` in the type declaration, are
382not given in applications of ``index``; their values can be inferred
383from the types of the ``Fin n`` and ``Vect n a`` arguments. Any name
384with a which appears as a parameter or index in a type declaration, but
385which is otherwise free, will be automatically bound as an implicit
386argument. Implicit arguments can still be given explicitly in
387applications, using ``{a=value}`` and ``{n=value}``, for example:
391 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
393In fact, any argument, implicit or explicit, may be given a name. We
394could have declared the type of ``index`` as:
398 index : (i:Fin n) -> (xs:Vect n a) -> a
400It is a matter of taste whether you want to do this — sometimes it can
401help document a function by making the purpose of an argument more
407Sometimes it is useful to provide types of implicit arguments,
408particularly where there is a dependency ordering, or where the implicit
409arguments themselves have dependencies. For example, we may wish to
410state the types of the implicit arguments in the following definition,
411which defines a predicate on vectors:
415 data Elem : a -> Vect n a -> Type where
416 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
417 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
419An instance of ``Elem x xs`` states that ``x`` is an element of ``xs``.
420We can construct such a predicate if the required element is ``Here``,
421at the head of the vector, or ``There``, in the tail of the vector. For
427 testVec = 3 :: 4 :: 5 :: 6 :: Nil
429 inVect : Elem 5 testVec
430 inVect = There (There Here)
432If the same implicit arguments are being used a lot, it can make a
433definition difficult to read. To avoid this problem, a ``using`` block
434gives the types and ordering of any implicit arguments which can appear
439 using (x:a, y:a, xs:Vect n a)
440 data Elem : a -> Vect n a -> Type where
441 Here : Elem x (x :: xs)
442 There : Elem x xs -> Elem x (y :: xs)
444Note: Declaration Order and ``mutual`` blocks
445~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
447In general, functions and data types must be defined before use, since
448dependent types allow functions to appear as part of types, and their
449reduction behaviour to affect type checking. However, this restriction
450can be relaxed by using a ``mutual`` block, which allows data types and
451functions to be defined simultaneously:
464In a ``mutual`` block, first all of the type declarations are added,
465then the function bodies. As a result, none of the function types can
466depend on the reduction behaviour of any of the functions in the block.
471Computer programs are of little use if they do not interact with the
472user or the system in some way. The difficulty in a pure language such
473as ``Idris`` — that is, a language where expressions do not have
474side-effects — is that I/O is inherently side-effecting. Therefore in
475``Idris``, such interactions are encapsulated in the type ``IO``:
479 data IO a -- IO operation returning a value of type a
481We’ll leave the definition of ``IO`` abstract, but effectively it
482describes what the I/O operations to be executed are, rather than how to
483execute them. The resulting operations are executed externally, by the
484run-time system. We’ve already seen one IO program:
489 main = putStrLn "Hello world"
491The type of ``putStrLn`` explains that it takes a string, and returns an
492element of the unit type ``()`` via an I/O action. There is a variant
493``putStr`` which outputs a string without a newline:
497 putStrLn : String -> IO ()
498 putStr : String -> IO ()
500We can also read strings from user input:
506A number of other I/O operations are defined in the prelude, for example
507for reading and writing files, including:
511 data File -- abstract
512 data Mode = Read | Write | ReadWrite
514 openFile : String -> Mode -> IO File
515 closeFile : File -> IO ()
517 fread : File -> IO String
518 fwrite : File -> String -> IO ()
519 feof : File -> IO Bool
521 readFile : String -> IO String
526I/O programs will typically need to sequence actions, feeding the output
527of one computation into the input of the next. ``IO`` is an abstract
528type, however, so we can’t access the result of a computation directly.
529Instead, we sequence operations with ``do`` notation:
534 greet = do putStr "What is your name? "
536 putStrLn ("Hello " ++ name)
538The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
539type ``IO a``, and puts the result, of type ``a`` into the variable
540``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
541has type ``String``. Indentation is significant — each statement in the
542do block must begin in the same column. The ``return`` operation allows
543us to inject a value directly into an IO operation:
549As we will see later, ``do`` notation is more general than this, and can
560Intermediate values can be calculated using ``let`` bindings:
564 data Person = MkPerson String Int
566 showPerson : Person -> String
567 showPerson p = let MkPerson name age = p in
568 name ++ " is " ++ show age ++ " years old"
570 splitAt : Char -> String -> (String, String)
571 splitAt c x = case break (== c) x of
572 (x, y) => (x, strTail y)
574We can do simple pattern matching in ``let`` bindings too. For example,
575we can extract fields from a record as follows, as well as by pattern
576matching at the top level:
580 data Person = MkPerson String Int
582 showPerson : Person -> String
583 showPerson p = let MkPerson name age = p in
584 name ++ " is " ++ show age ++ " years old"
591``Idris`` provides *comprehension* notation as a convenient shorthand
592for building lists. The general form is:
596 [ expression | qualifiers ]
598This generates the list of values produced by evaluating the
599``expression``, according to the conditions given by the comma separated
600``qualifiers``. For example, we can build a list of Pythagorean triples
605 pythag : Int -> List (Int, Int, Int)
606 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
609The ``[a..b]`` notation is another shorthand which builds a list of
610numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
611list of numbers between ``a`` and ``c`` with the increment specified by
612the difference between ``a`` and ``b``. This works for any numeric type,
613using the ``count`` function from the prelude.
618Another way of inspecting intermediate values of *simple* types is to
619use a ``case`` expression. The following function, for example, splits a
620string into two at a given character:
624 splitAt : Char -> String -> (String, String)
625 splitAt c x = case break (== c) x of
626 (x, y) => (x, strTail y)
628``break`` is a library function which breaks a string into a pair of
629strings at the point where the given function returns true. We then
630deconstruct the pair it returns, and remove the first character of the
633A ``case`` expression can match several cases, for example, to inspect
634an intermediate value of type ``Maybe a``. Recall ``list_lookup`` which
635looks up an index in a list, returning ``Nothing`` if the index is out
636of bounds. We can use this to write ``lookup_default``, which looks up
637an index and returns a default value if the index is out of bounds:
641 lookup_default : Nat -> List a -> a -> a
642 lookup_default i xs def = case list_lookup i xs of
646If the index is in bounds, we get the value at that index, otherwise we
651 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
653 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
656**Restrictions:** The ``case`` construct is intended for simple analysis
657of intermediate expressions to avoid the need to write auxiliary
658functions, and is also used internally to implement pattern matching
659``let`` and lambda bindings. It will *only* work if:
661- Each branch *matches* a value of the same type, and *returns* a value
664- The type of the result is “known”. i.e. the type of the expression
665 can be determined *without* type checking the ``case``-expression
671*Records* are data types which collect several values (the record’s
672*fields*) together. ``Idris`` provides syntax for defining records and
673automatically generating field access and update functions. For example,
674we can represent a person’s name and age in a record:
678 record Person : Type where
679 MkPerson : (name : String) ->
680 (age : Int) -> Person
683 fred = MkPerson "Fred" 30
685Record declarations are like ``data`` declarations, except that they are
686introduced by the ``record`` keyword, and can only have one constructor.
687The names of the binders in the constructor type (``name`` and ``age``)
688here are the field names, which we can use to access the field values:
697 name : Person -> String
699We can also use the field names to update a record (or, more precisely,
700produce a new record with the given fields updated).
704 *record> record { name = "Jim" } fred
705 MkPerson "Jim" 30 : Person
706 *record> record { name = "Jim", age = 20 } fred
707 MkPerson "Jim" 20 : Person
709The syntax ``record { field = val, ... }`` generates a function which
710updates the given fields in a record.
712Records, and fields within records, can have dependent types. Updates
713are allowed to change the type of a field, provided that the result is
714well-typed, and the result does not affect the type of the record as a
719 record Class : Type where
720 ClassInfo : (students : Vect n Person) ->
721 (className : String) ->
724It is safe to update the ``students`` field to a vector of a different
725length because it will not affect the type of the record:
729 addStudent : Person -> Class -> Class
730 addStudent p c = record { students = p :: students c } c
734 *record> addStudent fred (ClassInfo [] "CS")
735 ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
741``Idris`` also provides a convenient syntax for accessing and updating
742nested records. For example, if a field is accessible with the
743expression ``c (b (a x))``, it can be updated using the following
748 record { a->b->c = val } x
750This returns a new record, with the field accessed by the path
751``a->b->c`` set to ``x``. The syntax is first class, i.e.
752``record { a->b->c = val }`` itself has a function type. Symmetrically,
753the field can also be accessed with the following syntax:
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