10Idris 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 ``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)
260In Idris, types are a first class language construct, meaning that they
261can be computed and manipulated (and passed to functions) just like any
262other language construct. For example, we could write a function which
267 isSingleton : Bool -> Type
268 isSingleton True = Nat
269 isSingleton False = List Nat
271This function calculates the appropriate type from a ``Bool`` which flags
272whether the type should be a singleton or not. We can use this function
273to calculate a type anywhere that a type can be used. For example, it
274can be used to calculate a return type:
278 mkSingle : (x : Bool) -> isSingleton x
282Or it can be used to have varying input types. The following function
283calculates either the sum of a list of ``Nat``, or returns the given
284``Nat``, depending on whether the singleton flag is true:
288 sum : (single : Bool) -> isSingleton single -> Nat
291 sum False (x :: xs) = x + sum False xs
296A standard example of a dependent data type is the type of “lists with
297length”, conventionally called vectors in the dependent type
298literature. They are available as part of the Idris library, by
299importing ``Data.Vect``, or we can declare them as follows:
303 data Vect : Nat -> Type -> Type where
305 (::) : a -> Vect k a -> Vect (S k) a
307Note that we have used the same constructor names as for ``List``.
308Ad-hoc name overloading such as this is accepted by Idris,
309provided that the names are declared in different namespaces (in
310practice, normally in different modules). Ambiguous constructor names
311can normally be resolved from context.
313This declares a family of types, and so the form of the declaration is
314rather different from the simple type declarations above. We
315explicitly state the type of the type constructor ``Vect`` — it takes
316a ``Nat`` and a type as an argument, where ``Type`` stands for the
317type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
318*parameterised* by ``Type``. Each constructor targets a different part
319of the family of types. ``Nil`` can only be used to construct vectors
320with zero length, and ``::`` to construct vectors with non-zero
321length. In the type of ``::``, we state explicitly that an element of
322type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
323``k``) combine to make a vector of length ``S k``.
325We can define functions on dependent types such as ``Vect`` in the same
326way as on simple types such as ``List`` and ``Nat`` above, by pattern
327matching. The type of a function over ``Vect`` will describe what
328happens to the lengths of the vectors involved. For example, ``++``,
329defined as follows, appends two ``Vect``:
333 (++) : Vect n a -> Vect m a -> Vect (n + m) a
335 (++) (x :: xs) ys = x :: xs ++ ys
337The type of ``(++)`` states that the resulting vector’s length will be
338the sum of the input lengths. If we get the definition wrong in such a
339way that this does not hold, Idris will not accept the definition.
344 (++) : Vect n a -> Vect m a -> Vect (n + m) a
346 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
348When run through the Idris type checker, this results in the
353 $ idris vbroken.idr --check
354 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
355 When elaborating an application of constructor Vect.:::
356 Type mismatch between
357 Vect (k + k) a (Type of xs ++ xs)
359 Vect (plus k m) a (Expected type)
362 Type mismatch between
368This error message suggests that there is a length mismatch between
369two vectors — we needed a vector of length ``k + m``, but provided a
370vector of length ``k + k``.
375Finite sets, as the name suggests, are sets with a finite number of
376elements. They are available as part of the Idris library, by
377importing ``Data.Fin``, or can be declared as follows:
381 data Fin : Nat -> Type where
383 FS : Fin k -> Fin (S k)
385From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
386So this is not a set in the sense of a collection that is a container of objects,
387rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
388Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
389``n`` is the argument used to instantiate the ``Fin`` type.
390For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
392Let us look at the constructors in greater detail.
394``FZ`` is the zeroth element of a finite set with ``S k`` elements;
395``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
396elements. ``Fin`` is indexed by a ``Nat``, which represents the number
397of elements in the set. Since we can’t construct an element of an
398empty set, neither constructor targets ``Fin Z``.
400As mentioned above, a useful application of the ``Fin`` family is to
401represent bounded natural numbers. Since the first ``n`` natural
402numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
403the set of integers greater than or equal to zero and less than ``n``.
405For example, the following function which looks up an element in a
406``Vect``, by a bounded index given as a ``Fin n``, is defined in the
411 index : Fin n -> Vect n a -> a
412 index FZ (x :: xs) = x
413 index (FS k) (x :: xs) = index k xs
415This function looks up a value at a given location in a vector. The
416location is bounded by the length of the vector (``n`` in each case),
417so there is no need for a run-time bounds check. The type checker
418guarantees that the location is no larger than the length of the
419vector, and of course no less than zero.
421Note also that there is no case for ``Nil`` here. This is because it
422is impossible. Since there is no element of ``Fin Z``, and the
423location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
424attempting to look up an element in an empty vector would give a
425compile time type error, since it would force ``n`` to be ``Z``.
430Let us take a closer look at the type of ``index``:
434 index : Fin n -> Vect n a -> a
436It takes two arguments, an element of the finite set of ``n`` elements,
437and a vector with ``n`` elements of type ``a``. But there are also two
438names, ``n`` and ``a``, which are not declared explicitly. These are
439*implicit* arguments to ``index``. We could also write the type of
444 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
446Implicit arguments, given in braces ``{}`` in the type declaration,
447are not given in applications of ``index``; their values can be
448inferred from the types of the ``Fin n`` and ``Vect n a``
449arguments. Any name beginning with a lower case letter which appears
450as a parameter or index in a
451type declaration, which is not applied to any arguments, will
452*always* be automatically
453bound as an implicit argument. Implicit arguments can still be given
454explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
459 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
461In fact, any argument, implicit or explicit, may be given a name. We
462could have declared the type of ``index`` as:
466 index : (i:Fin n) -> (xs:Vect n a) -> a
468It is a matter of taste whether you want to do this — sometimes it can
469help document a function by making the purpose of an argument more
472Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
473``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";
478 isEmpty : Vect n a -> Bool
479 isEmpty {n = Z} _ = True
480 isEmpty {n = S k} _ = False
485Sometimes it is useful to provide types of implicit arguments,
486particularly where there is a dependency ordering, or where the
487implicit arguments themselves have dependencies. For example, we may
488wish to state the types of the implicit arguments in the following
489definition, which defines a predicate on vectors (this is also defined
490in ``Data.Vect``, under the name ``Elem``):
494 data IsElem : a -> Vect n a -> Type where
495 Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
496 There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
498An instance of ``IsElem x xs`` states that ``x`` is an element of
499``xs``. We can construct such a predicate if the required element is
500``Here``, at the head of the vector, or ``There``, in the tail of the
506 testVec = 3 :: 4 :: 5 :: 6 :: Nil
508 inVect : IsElem 5 Main.testVec
509 inVect = There (There Here)
512.. important:: Implicit Arguments and Scope
514 Within the type signature the typechecker will treat all variables
515 that start with an lowercase letter **and** are not applied to
516 something else as an implicit variable. To get the above code
517 example to compile you will need to provide a qualified name for
518 ``testVec``. In the example above, we have assumed that the code
519 lives within the ``Main`` module.
522If the same implicit arguments are being used a lot, it can make a
523definition difficult to read. To avoid this problem, a ``using`` block
524gives the types and ordering of any implicit arguments which can
525appear within the block:
529 using (x:a, y:a, xs:Vect n a)
530 data IsElem : a -> Vect n a -> Type where
531 Here : IsElem x (x :: xs)
532 There : IsElem x xs -> IsElem x (y :: xs)
536Note: Declaration Order and ``mutual`` blocks
537~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
539In general, functions and data types must be defined before use, since
540dependent types allow functions to appear as part of types, and type
541checking can rely on how particular functions are defined (though this
542is only true of total functions; see Section :ref:`sect-totality`)).
543However, this restriction can be relaxed by using a ``mutual`` block,
544which allows data types and functions to be defined simultaneously:
557In a ``mutual`` block, first all of the type declarations are added,
558then the function bodies. As a result, none of the function types can
559depend on the reduction behaviour of any of the functions in the
565Computer programs are of little use if they do not interact with the
566user or the system in some way. The difficulty in a pure language such
567as Idris — that is, a language where expressions do not have
568side-effects — is that I/O is inherently side-effecting. Therefore in
569Idris, such interactions are encapsulated in the type ``IO``:
573 data IO a -- IO operation returning a value of type a
575We’ll leave the definition of ``IO`` abstract, but effectively it
576describes what the I/O operations to be executed are, rather than how
577to execute them. The resulting operations are executed externally, by
578the run-time system. We’ve already seen one IO program:
583 main = putStrLn "Hello world"
585The type of ``putStrLn`` explains that it takes a string, and returns
586an element of the unit type ``()`` via an I/O action. There is a
587variant ``putStr`` which outputs a string without a newline:
591 putStrLn : String -> IO ()
592 putStr : String -> IO ()
594We can also read strings from user input:
600A number of other I/O operations are defined in the prelude, for
601example for reading and writing files, including:
605 data File -- abstract
606 data Mode = Read | Write | ReadWrite
608 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
609 closeFile : File -> IO ()
611 fGetLine : (h : File) -> IO (Either FileError String)
612 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
613 fEOF : File -> IO Bool
615Note that several of these return ``Either``, since they may fail.
622I/O programs will typically need to sequence actions, feeding the
623output of one computation into the input of the next. ``IO`` is an
624abstract type, however, so we can’t access the result of a computation
625directly. Instead, we sequence operations with ``do`` notation:
630 greet = do putStr "What is your name? "
632 putStrLn ("Hello " ++ name)
634The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
635type ``IO a``, and puts the result, of type ``a`` into the variable
636``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
637has type ``String``. Indentation is significant — each statement in
638the do block must begin in the same column. The ``return`` operation
639allows us to inject a value directly into an IO operation:
645As we will see later, ``do`` notation is more general than this, and
653Normally, arguments to functions are evaluated before the function
654itself (that is, Idris uses *eager* evaluation). However, this is
655not always the best approach. Consider the following function:
659 ifThenElse : Bool -> a -> a -> a;
660 ifThenElse True t e = t;
661 ifThenElse False t e = e;
663This function uses one of the ``t`` or ``e`` arguments, but not both
664(in fact, this is used to implement the ``if...then...else`` construct
665as we will see later. We would prefer if *only* the argument which was
666used was evaluated. To achieve this, Idris provides a ``Lazy``
667data type, which allows evaluation to be suspended:
671 data Lazy : Type -> Type where
672 Delay : (val : a) -> Lazy a
676A value of type ``Lazy a`` is unevaluated until it is forced by
677``Force``. The Idris type checker knows about the ``Lazy`` type,
678and inserts conversions where necessary between ``Lazy a`` and ``a``,
679and vice versa. We can therefore write ``ifThenElse`` as follows,
680without any explicit use of ``Force`` or ``Delay``:
684 ifThenElse : Bool -> Lazy a -> Lazy a -> a;
685 ifThenElse True t e = t;
686 ifThenElse False t e = e;
691Codata types are like regular data types, except that they allow for us to
692define infinite data structures. More precisely, for a type ``T``, each of its
693constructor arguments of type ``T`` are transformed into a coinductive parameter
694``Inf T``. This makes each of the ``T`` arguments lazy, and allows infinite data
695structures of type ``T`` to be built. One example of a codata type is Stream,
696which is defined as follows.
700 codata Stream : Type -> Type where
701 (::) : (e : a) -> Stream a -> Stream a
703This gets translated into the following by the compiler.
707 data Stream : Type -> Type where
708 (::) : (e : a) -> Inf (Stream a) -> Stream a
710The following is an example of how the codata type ``Stream`` can be used to
711form an infinite data structure. In this case we are creating an infinite stream
719It is important to note that codata does not allow the creation of infinite
720mutually recursive data structures. For example the following will create an
721infinite loop and cause a stack overflow.
726 codata Blue a = B a (Red a)
727 codata Red a = R a (Blue a)
737 findB : (a -> Bool) -> Blue a -> a
738 findB f (B x r) = if f x then x else findR f r
740 findR : (a -> Bool) -> Red a -> a
741 findR f (R x b) = if f x then x else findB f b
744 main = do printLn $ findB (== 1) blue
746To fix this we must add explicit ``Inf`` declarations to the constructor
747parameter types, since codata will not add it to constructor parameters of a
748**different** type from the one being defined. For example, the following
754 data Blue : Type -> Type where
755 B : a -> Inf (Red a) -> Blue a
757 data Red : Type -> Type where
758 R : a -> Inf (Blue a) -> Red a
768 findB : (a -> Bool) -> Blue a -> a
769 findB f (B x r) = if f x then x else findR f r
771 findR : (a -> Bool) -> Red a -> a
772 findR f (R x b) = if f x then x else findB f b
775 main = do printLn $ findB (== 1) blue
780Idris includes a number of useful data types and library functions
781(see the ``libs/`` directory in the distribution). This chapter
782describes a few of these. The functions described here are imported
783automatically by every Idris program, as part of ``Prelude.idr``.
788We have already seen the ``List`` and ``Vect`` data types:
792 data List a = Nil | (::) a (List a)
794 data Vect : Nat -> Type -> Type where
796 (::) : a -> Vect k a -> Vect (S k) a
798Note that the constructor names are the same for each — constructor
799names (in fact, names in general) can be overloaded, provided that
800they are declared in different namespaces (see Section
801:ref:`sect-namespaces`), and will typically be resolved according to
802their type. As syntactic sugar, any type with the constructor names
803``Nil`` and ``::`` can be written in list form. For example:
805- ``[]`` means ``Nil``
807- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
809The library also defines a number of functions for manipulating these
810types. ``map`` is overloaded both for ``List`` and ``Vect`` and
811applies a function to every element of the list or vector.
815 map : (a -> b) -> List a -> List b
817 map f (x :: xs) = f x :: map f xs
819 map : (a -> b) -> Vect n a -> Vect n b
821 map f (x :: xs) = f x :: map f xs
823For example, given the following vector of integers, and a function to
829 intVec = [1, 2, 3, 4, 5]
834the function ``map`` can be used as follows to double every element in
839 *usefultypes> show (map double intVec)
840 "[2, 4, 6, 8, 10]" : String
842For more details of the functions available on ``List`` and
843``Vect``, look in the library files:
845- ``libs/prelude/Prelude/List.idr``
847- ``libs/base/Data/List.idr``
849- ``libs/base/Data/Vect.idr``
851- ``libs/base/Data/VectType.idr``
853Functions include filtering, appending, reversing, and so on. Also
854remember that Idris is still in development, so if you don’t see
855the function you need, please feel free to add it and submit a patch!
857Aside: Anonymous functions and operator sections
858~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
860There are actually neater ways to write the above expression. One way
861would be to use an anonymous function:
865 *usefultypes> show (map (\x => x * 2) intVec)
866 "[2, 4, 6, 8, 10]" : String
868The notation ``\x => val`` constructs an anonymous function which takes
869one argument, ``x`` and returns the expression ``val``. Anonymous
870functions may take several arguments, separated by commas,
871e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
872e.g. ``\x : Int => x * 2``, and can pattern match,
873e.g. ``\(x, y) => x + y``. We could also use an operator section:
877 *usefultypes> show (map (* 2) intVec)
878 "[2, 4, 6, 8, 10]" : String
880``(*2)`` is shorthand for a function which multiplies a number
881by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
887``Maybe`` describes an optional value. Either there is a value of the
888given type, or there isn’t:
892 data Maybe a = Just a | Nothing
894``Maybe`` is one way of giving a type to an operation that may
895fail. For example, looking something up in a ``List`` (rather than a
896vector) may result in an out of bounds error:
900 list_lookup : Nat -> List a -> Maybe a
901 list_lookup _ Nil = Nothing
902 list_lookup Z (x :: xs) = Just x
903 list_lookup (S k) (x :: xs) = list_lookup k xs
905The ``maybe`` function is used to process values of type ``Maybe``,
906either by applying a function to the value, if there is one, or by
907providing a default value:
911 maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
913Note that the types of the first two arguments are wrapped in
914``Lazy``. Since only one of the two arguments will actually be used,
915we mark them as ``Lazy`` in case they are large expressions where it
916would be wasteful to compute and then discard them.
921Values can be paired with the following built-in data type:
925 data Pair a b = MkPair a b
927As syntactic sugar, we can write ``(a, b)`` which, according to
928context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
929contain an arbitrary number of values, represented as nested pairs:
936 jim : (String, Int, String)
937 jim = ("Jim", 25, "Cambridge")
941 *usefultypes> fst jim
943 *usefultypes> snd jim
944 (25, "Cambridge") : (Int, String)
945 *usefultypes> jim == ("Jim", (25, "Cambridge"))
951Dependent pairs allow the type of the second element of a pair to depend
952on the value of the first element. Traditionally, these are referred to
957 data DPair : (a : Type) -> (P : a -> Type) -> Type where
958 MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P
960Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
961of a pair of A and P, where the name ``a`` can occur inside ``P``.
962``( a ** p )`` constructs a value of this type. For example, we can
963pair a number with a ``Vect`` of a particular length.
967 vec : (n : Nat ** Vect n Int)
970If you like, you can write it out the long way, the two are precisely
975 vec : DPair Nat (\n => Vect n Int)
976 vec = MkDPair 2 [3, 4]
978The type checker could of course infer the value of the first element
979from the length of the vector. We can write an underscore ``_`` in
980place of values which we expect the type checker to fill in, so the
981above definition could also be written as:
985 vec : (n : Nat ** Vect n Int)
988We might also prefer to omit the type of the first element of the
989pair, since, again, it can be inferred:
993 vec : (n ** Vect n Int)
996One use for dependent pairs is to return values of dependent types
997where the index is not necessarily known in advance. For example, if
998we filter elements out of a ``Vect`` according to some predicate, we
999will not know in advance what the length of the resulting vector will
1002.. code-block:: idris
1004 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
1006If the ``Vect`` is empty, the result is easy:
1008.. code-block:: idris
1010 filter p Nil = (_ ** [])
1012In the ``::`` case, we need to inspect the result of a recursive call
1013to ``filter`` to extract the length and the vector from the result. To
1014do this, we use ``with`` notation, which allows pattern matching on
1017.. code-block:: idris
1019 filter p (x :: xs) with (filter p xs)
1020 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
1022We will see more on ``with`` notation later.
1028*Records* are data types which collect several values (the record's
1029*fields*) together. Idris provides syntax for defining records and
1030automatically generating field access and update functions. Unlike
1031the syntax used for data structures, records in Idris follow a
1032different syntax to that seen with Haskell. For example, we can
1033represent a person's name and age in a record:
1035.. code-block:: idris
1038 constructor MkPerson
1039 firstName, middleName, lastName : String
1043 fred = MkPerson "Fred" "Joe" "Bloggs" 30
1046The constructor name is provided using the ``constructor`` keyword,
1047and the *fields* are then given which are in an indented block
1048following the `where` keyword (here, ``firstName``, ``middleName``,
1049``lastName``, and ``age``). You can declare multiple fields on a
1050single line, provided that they have the same type. The field names
1051can be used to access the field values:
1055 *record> firstName fred
1059 *record> :t firstName
1060 firstName : Person -> String
1062We can also use the field names to update a record (or, more
1063precisely, produce a copy of the record with the given fields
1068 *record> record { firstName = "Jim" } fred
1069 MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1070 *record> record { firstName = "Jim", age = 20 } fred
1071 MkPerson "Jim" "Joe" "Bloggs" 20 : Person
1073The syntax ``record { field = val, ... }`` generates a function which
1074updates the given fields in a record.
1076Each record is defined in its own namespace, which means that field names
1077can be reused in multiple records.
1079Records, and fields within records, can have dependent types. Updates
1080are allowed to change the type of a field, provided that the result is
1083.. code-block:: idris
1086 constructor ClassInfo
1087 students : Vect n Person
1090It is safe to update the ``students`` field to a vector of a different
1091length because it will not affect the type of the record:
1093.. code-block:: idris
1095 addStudent : Person -> Class -> Class
1096 addStudent p c = record { students = p :: students c } c
1100 *record> addStudent fred (ClassInfo [] "CS")
1101 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1107Idris also provides a convenient syntax for accessing and updating
1108nested records. For example, if a field is accessible with the
1109expression ``c (b (a x))``, it can be updated using the following
1112.. code-block:: idris
1114 record { a->b->c = val } x
1116This returns a new record, with the field accessed by the path
1117``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
1118a->b->c = val }`` itself has a function type. Symmetrically, the field
1119can also be accessed with the following syntax:
1121.. code-block:: idris
1123 record { a->b->c } x
1129Records can also be dependent on values. Records *parameters*, which
1130are not subject to field updates. The parameters appear as arguments
1131to the resulting type, and are written following the record type
1132name. For example, a pair type could be defined as follows:
1134.. code-block:: idris
1136 record Prod a b where
1142Using the class record from the original introduction to records. The
1143size of the class can be restricted using a ``Vect`` and the size
1144promoted to the type level by parameterising the record with the size.
1148.. code-block:: idris
1150 record SizedClass (size : Nat) where
1151 constructor SizedClassInfo
1152 students : Vect size Person
1155**Note** that it is no longer possible to use the ``addStudent``
1156function from earlier, since that would change the size of the class. A
1157function to add a student must now specify in the type that the
1158size of the class has been increased by one. As the size is specified
1159using natural numbers, the new value can be incremented using the
1162.. code-block:: idris
1164 addStudent : Person -> SizedClass n -> SizedClass (S n)
1165 addStudent p c = SizedClassInfo (p :: students c) (className c)
1175Intermediate values can be calculated using ``let`` bindings:
1177.. code-block:: idris
1179 mirror : List a -> List a
1180 mirror xs = let xs' = reverse xs in
1183We can do simple pattern matching in ``let`` bindings too. For
1184example, we can extract fields from a record as follows, as well as by
1185pattern matching at the top level:
1187.. code-block:: idris
1189 data Person = MkPerson String Int
1191 showPerson : Person -> String
1192 showPerson p = let MkPerson name age = p in
1193 name ++ " is " ++ show age ++ " years old"
1198Idris provides *comprehension* notation as a convenient shorthand
1199for building lists. The general form is:
1203 [ expression | qualifiers ]
1205This generates the list of values produced by evaluating the
1206``expression``, according to the conditions given by the comma
1207separated ``qualifiers``. For example, we can build a list of
1208Pythagorean triples as follows:
1210.. code-block:: idris
1212 pythag : Int -> List (Int, Int, Int)
1213 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1216The ``[a..b]`` notation is another shorthand which builds a list of
1217numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1218list of numbers between ``a`` and ``c`` with the increment specified
1219by the difference between ``a`` and ``b``. This works for any numeric
1220type, using the ``count`` function from the prelude.
1225Another way of inspecting intermediate values of *simple* types is to
1226use a ``case`` expression. The following function, for example, splits
1227a string into two at a given character:
1229.. code-block:: idris
1231 splitAt : Char -> String -> (String, String)
1232 splitAt c x = case break (== c) x of
1233 (x, y) => (x, strTail y)
1235``break`` is a library function which breaks a string into a pair of
1236strings at the point where the given function returns true. We then
1237deconstruct the pair it returns, and remove the first character of the
1240A ``case`` expression can match several cases, for example, to inspect
1241an intermediate value of type ``Maybe a``. Recall ``list_lookup``
1242which looks up an index in a list, returning ``Nothing`` if the index
1243is out of bounds. We can use this to write ``lookup_default``, which
1244looks up an index and returns a default value if the index is out of
1247.. code-block:: idris
1249 lookup_default : Nat -> List a -> a -> a
1250 lookup_default i xs def = case list_lookup i xs of
1254If the index is in bounds, we get the value at that index, otherwise
1255we get a default value:
1259 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
1261 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
1264**Restrictions:** The ``case`` construct is intended for simple
1265analysis of intermediate expressions to avoid the need to write
1266auxiliary functions, and is also used internally to implement pattern
1267matching ``let`` and lambda bindings. It will *only* work if:
1269- Each branch *matches* a value of the same type, and *returns* a
1270 value of the same type.
1272- The type of the result is "known". i.e. the type of the expression
1273 can be determined *without* type checking the ``case``-expression
1279A *total* function is a function that terminates for all possible
1280inputs, or one that is guaranteed to produce some output before making
1281a recursive call. For example, Idris' ``head`` function is total for
1286 Idris> :t Prelude.List.head
1287 head : (l : List a) -> {auto ok : NonEmpty l} -> a
1289The ``{auto ok : NonEmpty l}`` tells us that Idris won't compile if we
1290try to call ``head`` on an empty list. The implementation is as follows:
1292.. code-block:: idris
1294 ||| Get the first element of a non-empty list
1295 ||| @ ok proof that the list is non-empty
1296 head : (l : List a) -> {auto ok : NonEmpty l} -> a
1297 head [] {ok=IsNonEmpty} impossible
1298 head (x::xs) {ok=p} = x
1300(Note that this implementation is in contrast to Haskell's ``head``,
1301which is *not* total and will fail at runtime rather than compile time.)
1302The following Idris code will compile:
1304.. code-block:: idris
1310 let x : Integer = head [1,2,3]
1313And will print ``1``. However, the same code with ``head []`` won't compile:
1317 test.idr:5:26:When checking right hand side of main with expected type
1320 When checking argument ok to function Prelude.List.head:
1321 Can't find a value of type
1324We can't bind and print ``x`` because ``head []`` doesn't type check.
1326However, we might imagine a function, ``unsafeHead``, that is identical to
1327Idris' ``head`` function except that it is *not* total: it will error out
1328at runtime if called on an empty list. (This is similar to the behavior of
1329Haskell's ``head`` function.) ``unsafeHead`` might look like this:
1331.. code-block:: idris
1332 -- Unsafe head example!
1333 unsafeHead : List a -> a
1334 unsafeHead (x::xs) = x
1336And although it typechecks and compiles, it will not reduce (that is, evaluation
1337of the function will cause it to change):
1341 unsafe> the Integer $ unsafeHead [1, 2, 3]
1343 unsafe> the Integer $ unsafeHead []
1344 unsafeHead [] : Integer
1346Functions that are not total are known as *partial functions*. As
1347mentioned in the note about ``mutual`` blocks, non-total definitions
1348aren't reduced when type checking because they are not well-defined
1349for all possible inputs.
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