10Idris defines several primitive types: ``Int``, ``Integer`` and
11``Double`` 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 ``idris
27 foo = "Sausage machine"
35An Idris file consists of an optional module declaration (here
36``module Prims``) followed by an optional list of imports and a
37collection of declarations and definitions. In this example no imports
38have been specified. However Idris programs can consist of several
39modules and the definitions in each module each have their own
40namespace. This is discussed further in Section
41:ref:`sect-namespaces`). When writing Idris programs both the order in which
42definitions are given and indentation are significant. Functions and
43data types must be defined before use, incidentally each definition must
44have a type declaration, for example see ``x : Int``, ``foo :
45String``, from the above listing. New declarations must begin at the
46same level of indentation as the preceding declaration.
47Alternatively, a semicolon ``;`` can be used to terminate declarations.
49A library module ``prelude`` is automatically imported by every
50Idris program, including facilities for IO, arithmetic, data
51structures and various common functions. The prelude defines several
52arithmetic and comparison operators, which we can use at the prompt.
53Evaluating things at the prompt gives an answer, and the type of the
63All of the usual arithmetic and comparison operators are defined for
64the primitive types. They are overloaded using interfaces, as we
65will discuss in Section :ref:`sect-interfaces` and can be extended to
66work on user defined types. Boolean expressions can be tested with the
67``if...then...else`` construct, for example:
71 *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
72 "The answer!" : String
77Data types are declared in a similar way and with similar syntax to
78Haskell. Natural numbers and lists, for example, can be declared as
83 data Nat = Z | S Nat -- Natural numbers
84 -- (zero and successor)
85 data List a = Nil | (::) a (List a) -- Polymorphic lists
87The above declarations are taken from the standard library. Unary
88natural numbers can be either zero (``Z``), or the successor of
89another natural number (``S k``). Lists can either be empty (``Nil``)
90or a value added to the front of another list (``x :: xs``). In the
91declaration for ``List``, we used an infix operator ``::``. New
92operators such as this can be added using a fixity declaration, as
99Functions, data constructors and type constructors may all be given
100infix operators as names. They may be used in prefix form if enclosed
101in brackets, e.g. ``(::)``. Infix operators can use any of the
108Some operators built from these symbols can't be user defined. These are
109``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,
110``==>``, ``\``, ``%``, ``~``, ``?``, and ``!``.
115Functions are implemented by pattern matching, again using a similar
116syntax to Haskell. The main difference is that Idris requires type
117declarations for all functions, using a single colon ``:`` (rather
118than Haskell’s double colon ``::``). Some natural number arithmetic
119functions can be defined as follows, again taken from the standard
125 plus : Nat -> Nat -> Nat
127 plus (S k) y = S (plus k y)
129 -- Unary multiplication
130 mult : Nat -> Nat -> Nat
132 mult (S k) y = plus y (mult k y)
134The standard arithmetic operators ``+`` and ``*`` are also overloaded
135for use by ``Nat``, and are implemented using the above functions.
136Unlike Haskell, there is no restriction on whether types and function
137names must begin with a capital letter or not. Function names
138(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
139``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
140all part of the same namespace. By convention, however,
141data types and constructor names typically begin with a capital letter.
142We can test these functions at the Idris prompt:
146 Idris> plus (S (S Z)) (S (S Z))
148 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
153 When displaying an element of ``Nat`` such as ``(S (S (S (S Z))))``,
154 Idris displays it as ``4``.
155 The result of ``plus (S (S Z)) (S (S Z))``
156 is actually ``(S (S (S (S Z))))``
157 which is the natural number ``4``.
158 This can be checked at the Idris prompt:
162 Idris> (S (S (S (S Z))))
165Like arithmetic operations, integer literals are also overloaded using
166interfaces, meaning that we can also test the functions as follows:
172 Idris> mult 3 (plus 2 2)
175You may wonder, by the way, why we have unary natural numbers when our
176computers have perfectly good integer arithmetic built in. The reason
177is primarily that unary numbers have a very convenient structure which
178is easy to reason about, and easy to relate to other data structures
179as we will see later. Nevertheless, we do not want this convenience to
180be at the expense of efficiency. Fortunately, Idris knows about
181the relationship between ``Nat`` (and similarly structured types) and
182numbers. This means it can optimise the representation, and functions
183such as ``plus`` and ``mult``.
188Functions can also be defined *locally* using ``where`` clauses. For
189example, to define a function which reverses a list, we can use an
190auxiliary function which accumulates the new, reversed list, and which
191does not need to be visible globally:
195 reverse : List a -> List a
196 reverse xs = revAcc [] xs where
197 revAcc : List a -> List a -> List a
199 revAcc acc (x :: xs) = revAcc (x :: acc) xs
201Indentation is significant — functions in the ``where`` block must be
202indented further than the outer function.
206 Any names which are visible in the outer scope are also visible in
207 the ``where`` clause (unless they have been redefined, such as ``xs``
208 here). A name which appears only in the type will be in scope in the
209 ``where`` clause if it is a *parameter* to one of the types, i.e. it
210 is fixed across the entire structure.
212As well as functions, ``where`` blocks can include local data
213declarations, such as the following where ``MyLT`` is not accessible
214outside the definition of ``foo``:
226 isLT = if x < 20 then Yes else No
228In general, functions defined in a ``where`` clause need a type
229declaration just like any top level function. However, the type
230declaration for a function ``f`` *can* be omitted if:
232- ``f`` appears in the right hand side of the top level definition
234- The type of ``f`` can be completely determined from its first application
237So, for example, the following definitions are legal:
243 even (S k) = odd k where
248 test = [c (S 1), c Z, d (S Z)]
250 d y = c (y + 1 + z y)
258Idris programs can contain *holes* which stand for incomplete parts of
259programs. For example, we could leave a hole for the greeting in our
260"Hello world" program:
265 main = putStrLn ?greeting
267The syntax ``?greeting`` introduces a hole, which stands for a part of
268a program which is not yet written. This is a valid Idris program, and you
269can check the type of ``greeting``:
274 --------------------------------------
277Checking the type of a hole also shows the types of any variables in scope.
278For example, given an incomplete definition of ``even``:
284 even (S k) = ?even_rhs
286We can check the type of ``even_rhs`` and see the expected return type,
287and the type of the variable ``k``:
293 --------------------------------------
296Holes are useful because they help us write functions *incrementally*.
297Rather than writing an entire function in one go, we can leave some parts
298unwritten and use Idris to tell us what is necessary to complete the
309In Idris, types are first class, meaning that they can be computed and
310manipulated (and passed to functions) just like any other language construct.
311For example, we could write a function which computes a type:
315 isSingleton : Bool -> Type
316 isSingleton True = Nat
317 isSingleton False = List Nat
319This function calculates the appropriate type from a ``Bool`` which flags
320whether the type should be a singleton or not. We can use this function
321to calculate a type anywhere that a type can be used. For example, it
322can be used to calculate a return type:
326 mkSingle : (x : Bool) -> isSingleton x
330Or it can be used to have varying input types. The following function
331calculates either the sum of a list of ``Nat``, or returns the given
332``Nat``, depending on whether the singleton flag is true:
336 sum : (single : Bool) -> isSingleton single -> Nat
339 sum False (x :: xs) = x + sum False xs
344A standard example of a dependent data type is the type of “lists with
345length”, conventionally called vectors in the dependent type
346literature. They are available as part of the Idris library, by
347importing ``Data.Vect``, or we can declare them as follows:
351 data Vect : Nat -> Type -> Type where
353 (::) : a -> Vect k a -> Vect (S k) a
355Note that we have used the same constructor names as for ``List``.
356Ad-hoc name overloading such as this is accepted by Idris,
357provided that the names are declared in different namespaces (in
358practice, normally in different modules). Ambiguous constructor names
359can normally be resolved from context.
361This declares a family of types, and so the form of the declaration is
362rather different from the simple type declarations above. We
363explicitly state the type of the type constructor ``Vect`` — it takes
364a ``Nat`` and a type as an argument, where ``Type`` stands for the
365type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
366*parameterised* by ``Type``. Each constructor targets a different part
367of the family of types. ``Nil`` can only be used to construct vectors
368with zero length, and ``::`` to construct vectors with non-zero
369length. In the type of ``::``, we state explicitly that an element of
370type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
371``k``) combine to make a vector of length ``S k``.
373We can define functions on dependent types such as ``Vect`` in the same
374way as on simple types such as ``List`` and ``Nat`` above, by pattern
375matching. The type of a function over ``Vect`` will describe what
376happens to the lengths of the vectors involved. For example, ``++``,
377defined as follows, appends two ``Vect``:
381 (++) : Vect n a -> Vect m a -> Vect (n + m) a
383 (++) (x :: xs) ys = x :: xs ++ ys
385The type of ``(++)`` states that the resulting vector’s length will be
386the sum of the input lengths. If we get the definition wrong in such a
387way that this does not hold, Idris will not accept the definition.
392 (++) : Vect n a -> Vect m a -> Vect (n + m) a
394 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
396When run through the Idris type checker, this results in the
401 $ idris VBroken.idr --check
403 When checking right hand side of Vect.++ with expected type
406 When checking an application of constructor Vect.:::
407 Type mismatch between
408 Vect (k + k) a (Type of xs ++ xs)
410 Vect (plus k m) a (Expected type)
413 Type mismatch between
419This error message suggests that there is a length mismatch between
420two vectors — we needed a vector of length ``k + m``, but provided a
421vector of length ``k + k``.
426Finite sets, as the name suggests, are sets with a finite number of
427elements. They are available as part of the Idris library, by
428importing ``Data.Fin``, or can be declared as follows:
432 data Fin : Nat -> Type where
434 FS : Fin k -> Fin (S k)
436From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
437So this is not a set in the sense of a collection that is a container of objects,
438rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
439Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
440``n`` is the argument used to instantiate the ``Fin`` type.
441For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
443Let us look at the constructors in greater detail.
445``FZ`` is the zeroth element of a finite set with ``S k`` elements;
446``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
447elements. ``Fin`` is indexed by a ``Nat``, which represents the number
448of elements in the set. Since we can’t construct an element of an
449empty set, neither constructor targets ``Fin Z``.
451As mentioned above, a useful application of the ``Fin`` family is to
452represent bounded natural numbers. Since the first ``n`` natural
453numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
454the set of integers greater than or equal to zero and less than ``n``.
456For example, the following function which looks up an element in a
457``Vect``, by a bounded index given as a ``Fin n``, is defined in the
462 index : Fin n -> Vect n a -> a
463 index FZ (x :: xs) = x
464 index (FS k) (x :: xs) = index k xs
466This function looks up a value at a given location in a vector. The
467location is bounded by the length of the vector (``n`` in each case),
468so there is no need for a run-time bounds check. The type checker
469guarantees that the location is no larger than the length of the
470vector, and of course no less than zero.
472Note also that there is no case for ``Nil`` here. This is because it
473is impossible. Since there is no element of ``Fin Z``, and the
474location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
475attempting to look up an element in an empty vector would give a
476compile time type error, since it would force ``n`` to be ``Z``.
481Let us take a closer look at the type of ``index``:
485 index : Fin n -> Vect n a -> a
487It takes two arguments, an element of the finite set of ``n`` elements,
488and a vector with ``n`` elements of type ``a``. But there are also two
489names, ``n`` and ``a``, which are not declared explicitly. These are
490*implicit* arguments to ``index``. We could also write the type of
495 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
497Implicit arguments, given in braces ``{}`` in the type declaration,
498are not given in applications of ``index``; their values can be
499inferred from the types of the ``Fin n`` and ``Vect n a``
500arguments. Any name beginning with a lower case letter which appears
501as a parameter or index in a
502type declaration, which is not applied to any arguments, will
503*always* be automatically
504bound as an implicit argument. Implicit arguments can still be given
505explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
510 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
512In fact, any argument, implicit or explicit, may be given a name. We
513could have declared the type of ``index`` as:
517 index : (i:Fin n) -> (xs:Vect n a) -> a
519It is a matter of taste whether you want to do this — sometimes it can
520help document a function by making the purpose of an argument more
523Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
524``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";
529 isEmpty : Vect n a -> Bool
530 isEmpty {n = Z} _ = True
531 isEmpty {n = S k} _ = False
536Sometimes it is useful to provide types of implicit arguments,
537particularly where there is a dependency ordering, or where the
538implicit arguments themselves have dependencies. For example, we may
539wish to state the types of the implicit arguments in the following
540definition, which defines a predicate on vectors (this is also defined
541in ``Data.Vect``, under the name ``Elem``):
545 data IsElem : a -> Vect n a -> Type where
546 Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
547 There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
549An instance of ``IsElem x xs`` states that ``x`` is an element of
550``xs``. We can construct such a predicate if the required element is
551``Here``, at the head of the vector, or ``There``, in the tail of the
557 testVec = 3 :: 4 :: 5 :: 6 :: Nil
559 inVect : IsElem 5 Main.testVec
560 inVect = There (There Here)
563.. important:: Implicit Arguments and Scope
565 Within the type signature the typechecker will treat all variables
566 that start with an lowercase letter **and** are not applied to
567 something else as an implicit variable. To get the above code
568 example to compile you will need to provide a qualified name for
569 ``testVec``. In the example above, we have assumed that the code
570 lives within the ``Main`` module.
573If the same implicit arguments are being used a lot, it can make a
574definition difficult to read. To avoid this problem, a ``using`` block
575gives the types and ordering of any implicit arguments which can
576appear within the block:
580 using (x:a, y:a, xs:Vect n a)
581 data IsElem : a -> Vect n a -> Type where
582 Here : IsElem x (x :: xs)
583 There : IsElem x xs -> IsElem x (y :: xs)
587Note: Declaration Order and ``mutual`` blocks
588~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
590In general, functions and data types must be defined before use, since
591dependent types allow functions to appear as part of types, and type
592checking can rely on how particular functions are defined (though this
593is only true of total functions; see Section :ref:`sect-totality`)).
594However, this restriction can be relaxed by using a ``mutual`` block,
595which allows data types and functions to be defined simultaneously:
608In a ``mutual`` block, first all of the type declarations are added,
609then the function bodies. As a result, none of the function types can
610depend on the reduction behaviour of any of the functions in the
616Computer programs are of little use if they do not interact with the
617user or the system in some way. The difficulty in a pure language such
618as Idris — that is, a language where expressions do not have
619side-effects — is that I/O is inherently side-effecting. Therefore in
620Idris, such interactions are encapsulated in the type ``IO``:
624 data IO a -- IO operation returning a value of type a
626We’ll leave the definition of ``IO`` abstract, but effectively it
627describes what the I/O operations to be executed are, rather than how
628to execute them. The resulting operations are executed externally, by
629the run-time system. We’ve already seen one IO program:
634 main = putStrLn "Hello world"
636The type of ``putStrLn`` explains that it takes a string, and returns
637an element of the unit type ``()`` via an I/O action. There is a
638variant ``putStr`` which outputs a string without a newline:
642 putStrLn : String -> IO ()
643 putStr : String -> IO ()
645We can also read strings from user input:
651A number of other I/O operations are defined in the prelude, for
652example for reading and writing files, including:
656 data File -- abstract
657 data Mode = Read | Write | ReadWrite
659 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
660 closeFile : File -> IO ()
662 fGetLine : (h : File) -> IO (Either FileError String)
663 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
664 fEOF : File -> IO Bool
666Note that several of these return ``Either``, since they may fail.
673I/O programs will typically need to sequence actions, feeding the
674output of one computation into the input of the next. ``IO`` is an
675abstract type, however, so we can’t access the result of a computation
676directly. Instead, we sequence operations with ``do`` notation:
681 greet = do putStr "What is your name? "
683 putStrLn ("Hello " ++ name)
685The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
686type ``IO a``, and puts the result, of type ``a`` into the variable
687``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
688has type ``String``. Indentation is significant — each statement in
689the do block must begin in the same column. The ``pure`` operation
690allows us to inject a value directly into an IO operation:
696As we will see later, ``do`` notation is more general than this, and
704Normally, arguments to functions are evaluated before the function
705itself (that is, Idris uses *eager* evaluation). However, this is
706not always the best approach. Consider the following function:
710 ifThenElse : Bool -> a -> a -> a
711 ifThenElse True t e = t
712 ifThenElse False t e = e
714This function uses one of the ``t`` or ``e`` arguments, but not both
715(in fact, this is used to implement the ``if...then...else`` construct
716as we will see later. We would prefer if *only* the argument which was
717used was evaluated. To achieve this, Idris provides a ``Lazy``
718data type, which allows evaluation to be suspended:
722 data Lazy : Type -> Type where
723 Delay : (val : a) -> Lazy a
727A value of type ``Lazy a`` is unevaluated until it is forced by
728``Force``. The Idris type checker knows about the ``Lazy`` type,
729and inserts conversions where necessary between ``Lazy a`` and ``a``,
730and vice versa. We can therefore write ``ifThenElse`` as follows,
731without any explicit use of ``Force`` or ``Delay``:
735 ifThenElse : Bool -> Lazy a -> Lazy a -> a
736 ifThenElse True t e = t
737 ifThenElse False t e = e
742Codata types allow us to define infinite data structures by marking recursive
743arguments as potentially infinite. For
744a codata type ``T``, each of its constructor arguments of type ``T`` are transformed
745into an argument of type ``Inf T``. This makes each of the ``T`` arguments
746lazy, and allows infinite data structures of type ``T`` to be built. One
747example of a codata type is Stream, which is defined as follows.
751 codata Stream : Type -> Type where
752 (::) : (e : a) -> Stream a -> Stream a
754This gets translated into the following by the compiler.
758 data Stream : Type -> Type where
759 (::) : (e : a) -> Inf (Stream a) -> Stream a
761The following is an example of how the codata type ``Stream`` can be used to
762form an infinite data structure. In this case we are creating an infinite stream
770It is important to note that codata does not allow the creation of infinite
771mutually recursive data structures. For example the following will create an
772infinite loop and cause a stack overflow.
777 codata Blue a = B a (Red a)
778 codata Red a = R a (Blue a)
788 findB : (a -> Bool) -> Blue a -> a
789 findB f (B x r) = if f x then x else findR f r
791 findR : (a -> Bool) -> Red a -> a
792 findR f (R x b) = if f x then x else findB f b
795 main = do printLn $ findB (== 1) blue
797To fix this we must add explicit ``Inf`` declarations to the constructor
798parameter types, since codata will not add it to constructor parameters of a
799**different** type from the one being defined. For example, the following
805 data Blue : Type -> Type where
806 B : a -> Inf (Red a) -> Blue a
808 data Red : Type -> Type where
809 R : a -> Inf (Blue a) -> Red a
819 findB : (a -> Bool) -> Blue a -> a
820 findB f (B x r) = if f x then x else findR f r
822 findR : (a -> Bool) -> Red a -> a
823 findR f (R x b) = if f x then x else findB f b
826 main = do printLn $ findB (== 1) blue
831Idris includes a number of useful data types and library functions
832(see the ``libs/`` directory in the distribution, and the
833`documentation <https://www.idris-lang.org/documentation/>`_). This section
834describes a few of these. The functions described here are imported
835automatically by every Idris program, as part of ``Prelude.idr``.
840We have already seen the ``List`` and ``Vect`` data types:
844 data List a = Nil | (::) a (List a)
846 data Vect : Nat -> Type -> Type where
848 (::) : a -> Vect k a -> Vect (S k) a
850Note that the constructor names are the same for each — constructor
851names (in fact, names in general) can be overloaded, provided that
852they are declared in different namespaces (see Section
853:ref:`sect-namespaces`), and will typically be resolved according to
854their type. As syntactic sugar, any type with the constructor names
855``Nil`` and ``::`` can be written in list form. For example:
857- ``[]`` means ``Nil``
859- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
861The library also defines a number of functions for manipulating these
862types. ``map`` is overloaded both for ``List`` and ``Vect`` and
863applies a function to every element of the list or vector.
867 map : (a -> b) -> List a -> List b
869 map f (x :: xs) = f x :: map f xs
871 map : (a -> b) -> Vect n a -> Vect n b
873 map f (x :: xs) = f x :: map f xs
875For example, given the following vector of integers, and a function to
881 intVec = [1, 2, 3, 4, 5]
886the function ``map`` can be used as follows to double every element in
891 *UsefulTypes> show (map double intVec)
892 "[2, 4, 6, 8, 10]" : String
894For more details of the functions available on ``List`` and
895``Vect``, look in the library files:
897- ``libs/prelude/Prelude/List.idr``
899- ``libs/base/Data/List.idr``
901- ``libs/base/Data/Vect.idr``
903- ``libs/base/Data/VectType.idr``
905Functions include filtering, appending, reversing, and so on.
907Aside: Anonymous functions and operator sections
908~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
910There are actually neater ways to write the above expression. One way
911would be to use an anonymous function:
915 *UsefulTypes> show (map (\x => x * 2) intVec)
916 "[2, 4, 6, 8, 10]" : String
918The notation ``\x => val`` constructs an anonymous function which takes
919one argument, ``x`` and returns the expression ``val``. Anonymous
920functions may take several arguments, separated by commas,
921e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
922e.g. ``\x : Int => x * 2``, and can pattern match,
923e.g. ``\(x, y) => x + y``. We could also use an operator section:
927 *UsefulTypes> show (map (* 2) intVec)
928 "[2, 4, 6, 8, 10]" : String
930``(*2)`` is shorthand for a function which multiplies a number
931by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
937``Maybe`` describes an optional value. Either there is a value of the
938given type, or there isn’t:
942 data Maybe a = Just a | Nothing
944``Maybe`` is one way of giving a type to an operation that may
945fail. For example, looking something up in a ``List`` (rather than a
946vector) may result in an out of bounds error:
950 list_lookup : Nat -> List a -> Maybe a
951 list_lookup _ Nil = Nothing
952 list_lookup Z (x :: xs) = Just x
953 list_lookup (S k) (x :: xs) = list_lookup k xs
955The ``maybe`` function is used to process values of type ``Maybe``,
956either by applying a function to the value, if there is one, or by
957providing a default value:
961 maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
963Note that the types of the first two arguments are wrapped in
964``Lazy``. Since only one of the two arguments will actually be used,
965we mark them as ``Lazy`` in case they are large expressions where it
966would be wasteful to compute and then discard them.
971Values can be paired with the following built-in data type:
975 data Pair a b = MkPair a b
977As syntactic sugar, we can write ``(a, b)`` which, according to
978context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
979contain an arbitrary number of values, represented as nested pairs:
986 jim : (String, Int, String)
987 jim = ("Jim", 25, "Cambridge")
991 *UsefulTypes> fst jim
993 *UsefulTypes> snd jim
994 (25, "Cambridge") : (Int, String)
995 *UsefulTypes> jim == ("Jim", (25, "Cambridge"))
1001Dependent pairs allow the type of the second element of a pair to depend
1002on the value of the first element.
1004.. code-block:: idris
1006 data DPair : (a : Type) -> (P : a -> Type) -> Type where
1007 MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P
1009Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
1010of a pair of A and P, where the name ``a`` can occur inside ``P``.
1011``( a ** p )`` constructs a value of this type. For example, we can
1012pair a number with a ``Vect`` of a particular length.
1014.. code-block:: idris
1016 vec : (n : Nat ** Vect n Int)
1019If you like, you can write it out the long way, the two are precisely
1022.. code-block:: idris
1024 vec : DPair Nat (\n => Vect n Int)
1025 vec = MkDPair 2 [3, 4]
1027The type checker could of course infer the value of the first element
1028from the length of the vector. We can write an underscore ``_`` in
1029place of values which we expect the type checker to fill in, so the
1030above definition could also be written as:
1032.. code-block:: idris
1034 vec : (n : Nat ** Vect n Int)
1037We might also prefer to omit the type of the first element of the
1038pair, since, again, it can be inferred:
1040.. code-block:: idris
1042 vec : (n ** Vect n Int)
1045One use for dependent pairs is to return values of dependent types
1046where the index is not necessarily known in advance. For example, if
1047we filter elements out of a ``Vect`` according to some predicate, we
1048will not know in advance what the length of the resulting vector will
1051.. code-block:: idris
1053 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
1055If the ``Vect`` is empty, the result is easy:
1057.. code-block:: idris
1059 filter p Nil = (_ ** [])
1061In the ``::`` case, we need to inspect the result of a recursive call
1062to ``filter`` to extract the length and the vector from the result. To
1063do this, we use ``with`` notation, which allows pattern matching on
1066.. code-block:: idris
1068 filter p (x :: xs) with (filter p xs)
1069 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
1071We will see more on ``with`` notation later.
1073Dependent pairs are sometimes referred to as “sigma types”.
1078*Records* are data types which collect several values (the record's
1079*fields*) together. Idris provides syntax for defining records and
1080automatically generating field access and update functions. Unlike
1081the syntax used for data structures, records in Idris follow a
1082different syntax to that seen with Haskell. For example, we can
1083represent a person's name and age in a record:
1085.. code-block:: idris
1088 constructor MkPerson
1089 firstName, middleName, lastName : String
1093 fred = MkPerson "Fred" "Joe" "Bloggs" 30
1096The constructor name is provided using the ``constructor`` keyword,
1097and the *fields* are then given which are in an indented block
1098following the `where` keyword (here, ``firstName``, ``middleName``,
1099``lastName``, and ``age``). You can declare multiple fields on a
1100single line, provided that they have the same type. The field names
1101can be used to access the field values:
1105 *Record> firstName fred
1109 *Record> :t firstName
1110 firstName : Person -> String
1112We can also use the field names to update a record (or, more
1113precisely, produce a copy of the record with the given fields
1118 *Record> record { firstName = "Jim" } fred
1119 MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1120 *Record> record { firstName = "Jim", age $= (+ 1) } fred
1121 MkPerson "Jim" "Joe" "Bloggs" 31 : Person
1123The syntax ``record { field = val, ... }`` generates a function which
1124updates the given fields in a record. ``=`` assigns a new value to a field,
1125and ``$=`` applies a function to update its value.
1127Each record is defined in its own namespace, which means that field names
1128can be reused in multiple records.
1130Records, and fields within records, can have dependent types. Updates
1131are allowed to change the type of a field, provided that the result is
1134.. code-block:: idris
1137 constructor ClassInfo
1138 students : Vect n Person
1141It is safe to update the ``students`` field to a vector of a different
1142length because it will not affect the type of the record:
1144.. code-block:: idris
1146 addStudent : Person -> Class -> Class
1147 addStudent p c = record { students = p :: students c } c
1151 *Record> addStudent fred (ClassInfo [] "CS")
1152 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1154We could also use ``$=`` to define ``addStudent`` more concisely:
1156.. code-block:: idris
1158 addStudent' : Person -> Class -> Class
1159 addStudent' p c = record { students $= (p ::) } c
1164Idris also provides a convenient syntax for accessing and updating
1165nested records. For example, if a field is accessible with the
1166expression ``c (b (a x))``, it can be updated using the following
1169.. code-block:: idris
1171 record { a->b->c = val } x
1173This returns a new record, with the field accessed by the path
1174``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
1175a->b->c = val }`` itself has a function type. Symmetrically, the field
1176can also be accessed with the following syntax:
1178.. code-block:: idris
1180 record { a->b->c } x
1182The ``$=`` notation is also valid for nested record updates.
1187Records can also be dependent on values. Records have *parameters*, which
1188cannot be updated like the other fields. The parameters appear as arguments
1189to the resulting type, and are written following the record type
1190name. For example, a pair type could be defined as follows:
1192.. code-block:: idris
1194 record Prod a b where
1200Using the ``class`` record from earlier, the size of the class can be
1201restricted using a ``Vect`` and the size included in the type by parameterising
1202the record with the size. For example:
1205.. code-block:: idris
1207 record SizedClass (size : Nat) where
1208 constructor SizedClassInfo
1209 students : Vect size Person
1212**Note** that it is no longer possible to use the ``addStudent``
1213function from earlier, since that would change the size of the class. A
1214function to add a student must now specify in the type that the
1215size of the class has been increased by one. As the size is specified
1216using natural numbers, the new value can be incremented using the
1219.. code-block:: idris
1221 addStudent : Person -> SizedClass n -> SizedClass (S n)
1222 addStudent p c = SizedClassInfo (p :: students c) (className c)
1232Intermediate values can be calculated using ``let`` bindings:
1234.. code-block:: idris
1236 mirror : List a -> List a
1237 mirror xs = let xs' = reverse xs in
1240We can do simple pattern matching in ``let`` bindings too. For
1241example, we can extract fields from a record as follows, as well as by
1242pattern matching at the top level:
1244.. code-block:: idris
1246 data Person = MkPerson String Int
1248 showPerson : Person -> String
1249 showPerson p = let MkPerson name age = p in
1250 name ++ " is " ++ show age ++ " years old"
1255Idris provides *comprehension* notation as a convenient shorthand
1256for building lists. The general form is:
1260 [ expression | qualifiers ]
1262This generates the list of values produced by evaluating the
1263``expression``, according to the conditions given by the comma
1264separated ``qualifiers``. For example, we can build a list of
1265Pythagorean triples as follows:
1267.. code-block:: idris
1269 pythag : Int -> List (Int, Int, Int)
1270 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1273The ``[a..b]`` notation is another shorthand which builds a list of
1274numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1275list of numbers between ``a`` and ``c`` with the increment specified
1276by the difference between ``a`` and ``b``. This works for type ``Nat``,
1277``Int`` and ``Integer``, using the ``enumFromTo`` and ``enumFromThenTo``
1278function from the prelude.
1283Another way of inspecting intermediate values of *simple* types is to
1284use a ``case`` expression. The following function, for example, splits
1285a string into two at a given character:
1287.. code-block:: idris
1289 splitAt : Char -> String -> (String, String)
1290 splitAt c x = case break (== c) x of
1291 (x, y) => (x, strTail y)
1293``break`` is a library function which breaks a string into a pair of
1294strings at the point where the given function returns true. We then
1295deconstruct the pair it returns, and remove the first character of the
1298A ``case`` expression can match several cases, for example, to inspect
1299an intermediate value of type ``Maybe a``. Recall ``list_lookup``
1300which looks up an index in a list, returning ``Nothing`` if the index
1301is out of bounds. We can use this to write ``lookup_default``, which
1302looks up an index and returns a default value if the index is out of
1305.. code-block:: idris
1307 lookup_default : Nat -> List a -> a -> a
1308 lookup_default i xs def = case list_lookup i xs of
1312If the index is in bounds, we get the value at that index, otherwise
1313we get a default value:
1317 *UsefulTypes> lookup_default 2 [3,4,5,6] (-1)
1319 *UsefulTypes> lookup_default 4 [3,4,5,6] (-1)
1322**Restrictions:** The ``case`` construct is intended for simple
1323analysis of intermediate expressions to avoid the need to write
1324auxiliary functions, and is also used internally to implement pattern
1325matching ``let`` and lambda bindings. It will *only* work if:
1327- Each branch *matches* a value of the same type, and *returns* a
1328 value of the same type.
1330- The type of the result is "known". i.e. the type of the expression
1331 can be determined *without* type checking the ``case``-expression
1337Idris distinguishes between *total* and *partial* functions.
1338A total function is a function that either:
1340+ Terminates for all possible inputs, or
1341+ Produces a non-empty, finite, prefix of a possibly infinite result
1343If a function is total, we can consider its type a precise description of what
1344that function will do. For example, if we have a function with a return
1345type of ``String`` we know something different, depending on whether or not
1348+ If it's total, it will return a value of type ``String`` in finite time
1349+ If it's partial, then as long as it doesn't crash or enter an infinite loop,
1350 it will return a ``String``.
1352Idris makes this distinction so that it knows which functions are safe to
1353evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,
1354if it tries to evaluate a function during type checking which doesn't
1355terminate, then type checking won't terminate!
1356Therefore, only total functions will be evaluated during type checking.
1357Partial functions can still be used in types, but will not be evaluated
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