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 Prims.idr``:
26 foo = "Sausage machine"
34An Idris file consists of an optional module declaration (here
35``module Prims``) followed by an optional list of imports and a
36collection of declarations and definitions. In this example no imports
37have been specified. However Idris programs can consist of several
38modules and the definitions in each module each have their own
39namespace. This is discussed further in Section
40:ref:`sect-namespaces`. When writing Idris programs both the order in which
41definitions are given and indentation are significant. Functions and
42data types must be defined before use, incidentally each definition must
43have a type declaration, for example see ``x : Int``, ``foo :
44String``, from the above listing. New declarations must begin at the
45same level of indentation as the preceding declaration.
46Alternatively, a semicolon ``;`` can be used to terminate declarations.
48A library module ``prelude`` is automatically imported by every
49Idris program, including facilities for IO, arithmetic, data
50structures and various common functions. The prelude defines several
51arithmetic and comparison operators, which we can use at the prompt.
52Evaluating things at the prompt gives an answer, and the type of the
62All of the usual arithmetic and comparison operators are defined for
63the primitive types. They are overloaded using interfaces, as we
64will discuss in Section :ref:`sect-interfaces` and can be extended to
65work on user defined types. Boolean expressions can be tested with the
66``if...then...else`` construct, for example:
70 *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
71 "The answer!" : String
76Data types are declared in a similar way and with similar syntax to
77Haskell. Natural numbers and lists, for example, can be declared as
82 data Nat = Z | S Nat -- Natural numbers
83 -- (zero and successor)
84 data List a = Nil | (::) a (List a) -- Polymorphic lists
86The above declarations are taken from the standard library. Unary
87natural numbers can be either zero (``Z``), or the successor of
88another natural number (``S k``). Lists can either be empty (``Nil``)
89or a value added to the front of another list (``x :: xs``). In the
90declaration for ``List``, we used an infix operator ``::``. New
91operators such as this can be added using a fixity declaration, as
98Functions, data constructors and type constructors may all be given
99infix operators as names. They may be used in prefix form if enclosed
100in brackets, e.g. ``(::)``. Infix operators can use any of the
107Some operators built from these symbols can't be user defined. These are
108``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,
109``==>``, ``\``, ``%``, ``~``, ``?``, and ``!``.
114Functions are implemented by pattern matching, again using a similar
115syntax to Haskell. The main difference is that Idris requires type
116declarations for all functions, using a single colon ``:`` (rather
117than Haskell’s double colon ``::``). Some natural number arithmetic
118functions can be defined as follows, again taken from the standard
124 plus : Nat -> Nat -> Nat
126 plus (S k) y = S (plus k y)
128 -- Unary multiplication
129 mult : Nat -> Nat -> Nat
131 mult (S k) y = plus y (mult k y)
133The standard arithmetic operators ``+`` and ``*`` are also overloaded
134for use by ``Nat``, and are implemented using the above functions.
135Unlike Haskell, there is no restriction on whether types and function
136names must begin with a capital letter or not. Function names
137(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
138``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
139all part of the same namespace. By convention, however,
140data types and constructor names typically begin with a capital letter.
141We can test these functions at the Idris prompt:
145 Idris> plus (S (S Z)) (S (S Z))
147 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
152 When displaying an element of ``Nat`` such as ``(S (S (S (S Z))))``,
153 Idris displays it as ``4``.
154 The result of ``plus (S (S Z)) (S (S Z))``
155 is actually ``(S (S (S (S Z))))``
156 which is the natural number ``4``.
157 This can be checked at the Idris prompt:
161 Idris> (S (S (S (S Z))))
164Like arithmetic operations, integer literals are also overloaded using
165interfaces, meaning that we can also test the functions as follows:
171 Idris> mult 3 (plus 2 2)
174You may wonder, by the way, why we have unary natural numbers when our
175computers have perfectly good integer arithmetic built in. The reason
176is primarily that unary numbers have a very convenient structure which
177is easy to reason about, and easy to relate to other data structures
178as we will see later. Nevertheless, we do not want this convenience to
179be at the expense of efficiency. Fortunately, Idris knows about
180the relationship between ``Nat`` (and similarly structured types) and
181numbers. This means it can optimise the representation, and functions
182such as ``plus`` and ``mult``.
187Functions can also be defined *locally* using ``where`` clauses. For
188example, to define a function which reverses a list, we can use an
189auxiliary function which accumulates the new, reversed list, and which
190does not need to be visible globally:
194 reverse : List a -> List a
195 reverse xs = revAcc [] xs where
196 revAcc : List a -> List a -> List a
198 revAcc acc (x :: xs) = revAcc (x :: acc) xs
200Indentation is significant — functions in the ``where`` block must be
201indented further than the outer function.
205 Any names which are visible in the outer scope are also visible in
206 the ``where`` clause (unless they have been redefined, such as ``xs``
207 here). A name which appears only in the type will be in scope in the
208 ``where`` clause if it is a *parameter* to one of the types, i.e. it
209 is fixed across the entire structure.
211As well as functions, ``where`` blocks can include local data
212declarations, such as the following where ``MyLT`` is not accessible
213outside the definition of ``foo``:
225 isLT = if x < 20 then Yes else No
227In general, functions defined in a ``where`` clause need a type
228declaration just like any top level function. However, the type
229declaration for a function ``f`` *can* be omitted if:
231- ``f`` appears in the right hand side of the top level definition
233- The type of ``f`` can be completely determined from its first application
236So, for example, the following definitions are legal:
242 even (S k) = odd k where
247 test = [c (S 1), c Z, d (S Z)]
249 d y = c (y + 1 + z y)
257Idris programs can contain *holes* which stand for incomplete parts of
258programs. For example, we could leave a hole for the greeting in our
259"Hello world" program:
264 main = putStrLn ?greeting
266The syntax ``?greeting`` introduces a hole, which stands for a part of
267a program which is not yet written. This is a valid Idris program, and you
268can check the type of ``greeting``:
273 --------------------------------------
276Checking the type of a hole also shows the types of any variables in scope.
277For example, given an incomplete definition of ``even``:
283 even (S k) = ?even_rhs
285We can check the type of ``even_rhs`` and see the expected return type,
286and the type of the variable ``k``:
292 --------------------------------------
295Holes are useful because they help us write functions *incrementally*.
296Rather than writing an entire function in one go, we can leave some parts
297unwritten and use Idris to tell us what is necessary to complete the
308In Idris, types are first class, meaning that they can be computed and
309manipulated (and passed to functions) just like any other language construct.
310For example, we could write a function which computes a type:
314 isSingleton : Bool -> Type
315 isSingleton True = Nat
316 isSingleton False = List Nat
318This function calculates the appropriate type from a ``Bool`` which flags
319whether the type should be a singleton or not. We can use this function
320to calculate a type anywhere that a type can be used. For example, it
321can be used to calculate a return type:
325 mkSingle : (x : Bool) -> isSingleton x
329Or it can be used to have varying input types. The following function
330calculates either the sum of a list of ``Nat``, or returns the given
331``Nat``, depending on whether the singleton flag is true:
335 sum : (single : Bool) -> isSingleton single -> Nat
338 sum False (x :: xs) = x + sum False xs
343A standard example of a dependent data type is the type of “lists with
344length”, conventionally called vectors in the dependent type
345literature. They are available as part of the Idris library, by
346importing ``Data.Vect``, or we can declare them as follows:
350 data Vect : Nat -> Type -> Type where
352 (::) : a -> Vect k a -> Vect (S k) a
354Note that we have used the same constructor names as for ``List``.
355Ad-hoc name overloading such as this is accepted by Idris,
356provided that the names are declared in different namespaces (in
357practice, normally in different modules). Ambiguous constructor names
358can normally be resolved from context.
360This declares a family of types, and so the form of the declaration is
361rather different from the simple type declarations above. We
362explicitly state the type of the type constructor ``Vect`` — it takes
363a ``Nat`` and a type as an argument, where ``Type`` stands for the
364type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
365*parameterised* by ``Type``. Each constructor targets a different part
366of the family of types. ``Nil`` can only be used to construct vectors
367with zero length, and ``::`` to construct vectors with non-zero
368length. In the type of ``::``, we state explicitly that an element of
369type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
370``k``) combine to make a vector of length ``S k``.
372We can define functions on dependent types such as ``Vect`` in the same
373way as on simple types such as ``List`` and ``Nat`` above, by pattern
374matching. The type of a function over ``Vect`` will describe what
375happens to the lengths of the vectors involved. For example, ``++``,
376defined as follows, appends two ``Vect``:
380 (++) : Vect n a -> Vect m a -> Vect (n + m) a
382 (++) (x :: xs) ys = x :: xs ++ ys
384The type of ``(++)`` states that the resulting vector’s length will be
385the sum of the input lengths. If we get the definition wrong in such a
386way that this does not hold, Idris will not accept the definition.
391 (++) : Vect n a -> Vect m a -> Vect (n + m) a
393 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
395When run through the Idris type checker, this results in the
400 $ idris VBroken.idr --check
402 When checking right hand side of Vect.++ with expected type
405 When checking an application of constructor Vect.:::
406 Type mismatch between
407 Vect (k + k) a (Type of xs ++ xs)
409 Vect (plus k m) a (Expected type)
412 Type mismatch between
418This error message suggests that there is a length mismatch between
419two vectors — we needed a vector of length ``k + m``, but provided a
420vector of length ``k + k``.
425Finite sets, as the name suggests, are sets with a finite number of
426elements. They are available as part of the Idris library, by
427importing ``Data.Fin``, or can be declared as follows:
431 data Fin : Nat -> Type where
433 FS : Fin k -> Fin (S k)
435From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
436So this is not a set in the sense of a collection that is a container of objects,
437rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
438Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
439``n`` is the argument used to instantiate the ``Fin`` type.
440For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
442Let us look at the constructors in greater detail.
444``FZ`` is the zeroth element of a finite set with ``S k`` elements;
445``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
446elements. ``Fin`` is indexed by a ``Nat``, which represents the number
447of elements in the set. Since we can’t construct an element of an
448empty set, neither constructor targets ``Fin Z``.
450As mentioned above, a useful application of the ``Fin`` family is to
451represent bounded natural numbers. Since the first ``n`` natural
452numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
453the set of integers greater than or equal to zero and less than ``n``.
455For example, the following function which looks up an element in a
456``Vect``, by a bounded index given as a ``Fin n``, is defined in the
461 index : Fin n -> Vect n a -> a
462 index FZ (x :: xs) = x
463 index (FS k) (x :: xs) = index k xs
465This function looks up a value at a given location in a vector. The
466location is bounded by the length of the vector (``n`` in each case),
467so there is no need for a run-time bounds check. The type checker
468guarantees that the location is no larger than the length of the
469vector, and of course no less than zero.
471Note also that there is no case for ``Nil`` here. This is because it
472is impossible. Since there is no element of ``Fin Z``, and the
473location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
474attempting to look up an element in an empty vector would give a
475compile time type error, since it would force ``n`` to be ``Z``.
480Let us take a closer look at the type of ``index``:
484 index : Fin n -> Vect n a -> a
486It takes two arguments, an element of the finite set of ``n`` elements,
487and a vector with ``n`` elements of type ``a``. But there are also two
488names, ``n`` and ``a``, which are not declared explicitly. These are
489*implicit* arguments to ``index``. We could also write the type of
494 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
496Implicit arguments, given in braces ``{}`` in the type declaration,
497are not given in applications of ``index``; their values can be
498inferred from the types of the ``Fin n`` and ``Vect n a``
499arguments. Any name beginning with a lower case letter which appears
500as a parameter or index in a
501type declaration, which is not applied to any arguments, will
502*always* be automatically
503bound as an implicit argument. Implicit arguments can still be given
504explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
509 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
511In fact, any argument, implicit or explicit, may be given a name. We
512could have declared the type of ``index`` as:
516 index : (i:Fin n) -> (xs:Vect n a) -> a
518It is a matter of taste whether you want to do this — sometimes it can
519help document a function by making the purpose of an argument more
522Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
523``{var = pat}`` gets an implicit variable and attempts to pattern match on “pat”;
528 isEmpty : Vect n a -> Bool
529 isEmpty {n = Z} _ = True
530 isEmpty {n = S k} _ = False
535Sometimes it is useful to provide types of implicit arguments,
536particularly where there is a dependency ordering, or where the
537implicit arguments themselves have dependencies. For example, we may
538wish to state the types of the implicit arguments in the following
539definition, which defines a predicate on vectors (this is also defined
540in ``Data.Vect``, under the name ``Elem``):
544 data IsElem : a -> Vect n a -> Type where
545 Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
546 There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
548An instance of ``IsElem x xs`` states that ``x`` is an element of
549``xs``. We can construct such a predicate if the required element is
550``Here``, at the head of the vector, or ``There``, in the tail of the
556 testVec = 3 :: 4 :: 5 :: 6 :: Nil
558 inVect : IsElem 5 Main.testVec
559 inVect = There (There Here)
561.. important:: Implicit Arguments and Scope
563 Within the type signature the typechecker will treat all variables
564 that start with an lowercase letter **and** are not applied to
565 something else as an implicit variable. To get the above code
566 example to compile you will need to provide a qualified name for
567 ``testVec``. In the example above, we have assumed that the code
568 lives within the ``Main`` module.
570If the same implicit arguments are being used a lot, it can make a
571definition difficult to read. To avoid this problem, a ``using`` block
572gives the types and ordering of any implicit arguments which can
573appear within the block:
577 using (x:a, y:a, xs:Vect n a)
578 data IsElem : a -> Vect n a -> Type where
579 Here : IsElem x (x :: xs)
580 There : IsElem x xs -> IsElem x (y :: xs)
582Note: Declaration Order and ``mutual`` blocks
583~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585In general, functions and data types must be defined before use, since
586dependent types allow functions to appear as part of types, and type
587checking can rely on how particular functions are defined (though this
588is only true of total functions; see Section :ref:`sect-totality`).
589However, this restriction can be relaxed by using a ``mutual`` block,
590which allows data types and functions to be defined simultaneously:
603In a ``mutual`` block, first all of the type declarations are added,
604then the function bodies. As a result, none of the function types can
605depend on the reduction behaviour of any of the functions in the
611Computer programs are of little use if they do not interact with the
612user or the system in some way. The difficulty in a pure language such
613as Idris — that is, a language where expressions do not have
614side-effects — is that I/O is inherently side-effecting. Therefore in
615Idris, such interactions are encapsulated in the type ``IO``:
619 data IO a -- IO operation returning a value of type a
621We’ll leave the definition of ``IO`` abstract, but effectively it
622describes what the I/O operations to be executed are, rather than how
623to execute them. The resulting operations are executed externally, by
624the run-time system. We’ve already seen one IO program:
629 main = putStrLn "Hello world"
631The type of ``putStrLn`` explains that it takes a string, and returns
632an element of the unit type ``()`` via an I/O action. There is a
633variant ``putStr`` which outputs a string without a newline:
637 putStrLn : String -> IO ()
638 putStr : String -> IO ()
640We can also read strings from user input:
646A number of other I/O operations are defined in the prelude, for
647example for reading and writing files, including:
651 data File -- abstract
652 data Mode = Read | Write | ReadWrite
654 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
655 closeFile : File -> IO ()
657 fGetLine : (h : File) -> IO (Either FileError String)
658 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
659 fEOF : File -> IO Bool
661Note that several of these return ``Either``, since they may fail.
668I/O programs will typically need to sequence actions, feeding the
669output of one computation into the input of the next. ``IO`` is an
670abstract type, however, so we can’t access the result of a computation
671directly. Instead, we sequence operations with ``do`` notation:
676 greet = do putStr "What is your name? "
678 putStrLn ("Hello " ++ name)
680The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
681type ``IO a``, and puts the result, of type ``a`` into the variable
682``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
683has type ``String``. Indentation is significant — each statement in
684the do block must begin in the same column. The ``pure`` operation
685allows us to inject a value directly into an IO operation:
691As we will see later, ``do`` notation is more general than this, and
699Normally, arguments to functions are evaluated before the function
700itself (that is, Idris uses *eager* evaluation). However, this is
701not always the best approach. Consider the following function:
705 ifThenElse : Bool -> a -> a -> a
706 ifThenElse True t e = t
707 ifThenElse False t e = e
709This function uses one of the ``t`` or ``e`` arguments, but not both
710(in fact, this is used to implement the ``if...then...else`` construct
711as we will see later). We would prefer if *only* the argument which was
712used was evaluated. To achieve this, Idris provides a ``Lazy``
713data type, which allows evaluation to be suspended:
717 data Lazy : Type -> Type where
718 Delay : (val : a) -> Lazy a
722A value of type ``Lazy a`` is unevaluated until it is forced by
723``Force``. The Idris type checker knows about the ``Lazy`` type,
724and inserts conversions where necessary between ``Lazy a`` and ``a``,
725and vice versa. We can therefore write ``ifThenElse`` as follows,
726without any explicit use of ``Force`` or ``Delay``:
730 ifThenElse : Bool -> Lazy a -> Lazy a -> a
731 ifThenElse True t e = t
732 ifThenElse False t e = e
737Codata types allow us to define infinite data structures by marking recursive
738arguments as potentially infinite. For
739a codata type ``T``, each of its constructor arguments of type ``T`` are transformed
740into an argument of type ``Inf T``. This makes each of the ``T`` arguments
741lazy, and allows infinite data structures of type ``T`` to be built. One
742example of a codata type is Stream, which is defined as follows.
746 codata Stream : Type -> Type where
747 (::) : (e : a) -> Stream a -> Stream a
749This gets translated into the following by the compiler.
753 data Stream : Type -> Type where
754 (::) : (e : a) -> Inf (Stream a) -> Stream a
756The following is an example of how the codata type ``Stream`` can be used to
757form an infinite data structure. In this case we are creating an infinite stream
765It is important to note that codata does not allow the creation of infinite
766mutually recursive data structures. For example the following will create an
767infinite loop and cause a stack overflow.
772 codata Blue a = B a (Red a)
773 codata Red a = R a (Blue a)
783 findB : (a -> Bool) -> Blue a -> a
784 findB f (B x r) = if f x then x else findR f r
786 findR : (a -> Bool) -> Red a -> a
787 findR f (R x b) = if f x then x else findB f b
790 main = do printLn $ findB (== 1) blue
792To fix this we must add explicit ``Inf`` declarations to the constructor
793parameter types, since codata will not add it to constructor parameters of a
794**different** type from the one being defined. For example, the following
800 data Blue : Type -> Type where
801 B : a -> Inf (Red a) -> Blue a
803 data Red : Type -> Type where
804 R : a -> Inf (Blue a) -> Red a
814 findB : (a -> Bool) -> Blue a -> a
815 findB f (B x r) = if f x then x else findR f r
817 findR : (a -> Bool) -> Red a -> a
818 findR f (R x b) = if f x then x else findB f b
821 main = do printLn $ findB (== 1) blue
826Idris includes a number of useful data types and library functions
827(see the ``libs/`` directory in the distribution, and the
828`documentation <https://www.idris-lang.org/documentation/>`_). This section
829describes a few of these. The functions described here are imported
830automatically by every Idris program, as part of ``Prelude.idr``.
835We have already seen the ``List`` and ``Vect`` data types:
839 data List a = Nil | (::) a (List a)
841 data Vect : Nat -> Type -> Type where
843 (::) : a -> Vect k a -> Vect (S k) a
845Note that the constructor names are the same for each — constructor
846names (in fact, names in general) can be overloaded, provided that
847they are declared in different namespaces (see Section
848:ref:`sect-namespaces`), and will typically be resolved according to
849their type. As syntactic sugar, any type with the constructor names
850``Nil`` and ``::`` can be written in list form. For example:
852- ``[]`` means ``Nil``
854- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
856The library also defines a number of functions for manipulating these
857types. ``map`` is overloaded both for ``List`` and ``Vect`` and
858applies a function to every element of the list or vector.
862 map : (a -> b) -> List a -> List b
864 map f (x :: xs) = f x :: map f xs
866 map : (a -> b) -> Vect n a -> Vect n b
868 map f (x :: xs) = f x :: map f xs
870For example, given the following vector of integers, and a function to
876 intVec = [1, 2, 3, 4, 5]
881the function ``map`` can be used as follows to double every element in
886 *UsefulTypes> show (map double intVec)
887 "[2, 4, 6, 8, 10]" : String
889For more details of the functions available on ``List`` and
890``Vect``, look in the library files:
892- ``libs/prelude/Prelude/List.idr``
894- ``libs/base/Data/List.idr``
896- ``libs/base/Data/Vect.idr``
898- ``libs/base/Data/VectType.idr``
900Functions include filtering, appending, reversing, and so on.
902Aside: Anonymous functions and operator sections
903~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905There are actually neater ways to write the above expression. One way
906would be to use an anonymous function:
910 *UsefulTypes> show (map (\x => x * 2) intVec)
911 "[2, 4, 6, 8, 10]" : String
913The notation ``\x => val`` constructs an anonymous function which takes
914one argument, ``x`` and returns the expression ``val``. Anonymous
915functions may take several arguments, separated by commas,
916e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
917e.g. ``\x : Int => x * 2``, and can pattern match,
918e.g. ``\(x, y) => x + y``. We could also use an operator section:
922 *UsefulTypes> show (map (* 2) intVec)
923 "[2, 4, 6, 8, 10]" : String
925``(*2)`` is shorthand for a function which multiplies a number
926by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
932``Maybe`` describes an optional value. Either there is a value of the
933given type, or there isn’t:
937 data Maybe a = Just a | Nothing
939``Maybe`` is one way of giving a type to an operation that may
940fail. For example, looking something up in a ``List`` (rather than a
941vector) may result in an out of bounds error:
945 list_lookup : Nat -> List a -> Maybe a
946 list_lookup _ Nil = Nothing
947 list_lookup Z (x :: xs) = Just x
948 list_lookup (S k) (x :: xs) = list_lookup k xs
950The ``maybe`` function is used to process values of type ``Maybe``,
951either by applying a function to the value, if there is one, or by
952providing a default value:
956 maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
958Note that the types of the first two arguments are wrapped in
959``Lazy``. Since only one of the two arguments will actually be used,
960we mark them as ``Lazy`` in case they are large expressions where it
961would be wasteful to compute and then discard them.
966Values can be paired with the following built-in data type:
970 data Pair a b = MkPair a b
972As syntactic sugar, we can write ``(a, b)`` which, according to
973context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
974contain an arbitrary number of values, represented as nested pairs:
981 jim : (String, Int, String)
982 jim = ("Jim", 25, "Cambridge")
986 *UsefulTypes> fst jim
988 *UsefulTypes> snd jim
989 (25, "Cambridge") : (Int, String)
990 *UsefulTypes> jim == ("Jim", (25, "Cambridge"))
996Dependent pairs allow the type of the second element of a pair to depend
997on the value of the first element:
1001 data DPair : (a : Type) -> (P : a -> Type) -> Type where
1002 MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P
1004Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
1005of a pair of A and P, where the name ``a`` can occur inside ``P``.
1006``( a ** p )`` constructs a value of this type. For example, we can
1007pair a number with a ``Vect`` of a particular length:
1009.. code-block:: idris
1011 vec : (n : Nat ** Vect n Int)
1014If you like, you can write it out the long way, the two are precisely
1017.. code-block:: idris
1019 vec : DPair Nat (\n => Vect n Int)
1020 vec = MkDPair 2 [3, 4]
1022The type checker could of course infer the value of the first element
1023from the length of the vector. We can write an underscore ``_`` in
1024place of values which we expect the type checker to fill in, so the
1025above definition could also be written as:
1027.. code-block:: idris
1029 vec : (n : Nat ** Vect n Int)
1032We might also prefer to omit the type of the first element of the
1033pair, since, again, it can be inferred:
1035.. code-block:: idris
1037 vec : (n ** Vect n Int)
1040One use for dependent pairs is to return values of dependent types
1041where the index is not necessarily known in advance. For example, if
1042we filter elements out of a ``Vect`` according to some predicate, we
1043will not know in advance what the length of the resulting vector will
1046.. code-block:: idris
1048 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
1050If the ``Vect`` is empty, the result is easy:
1052.. code-block:: idris
1054 filter p Nil = (_ ** [])
1056In the ``::`` case, we need to inspect the result of a recursive call
1057to ``filter`` to extract the length and the vector from the result. To
1058do this, we use ``with`` notation, which allows pattern matching on
1061.. code-block:: idris
1063 filter p (x :: xs) with (filter p xs)
1064 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
1066We will see more on ``with`` notation later.
1068Dependent pairs are sometimes referred to as “Sigma types”.
1073*Records* are data types which collect several values (the record's
1074*fields*) together. Idris provides syntax for defining records and
1075automatically generating field access and update functions. Unlike
1076the syntax used for data structures, records in Idris follow a
1077different syntax to that seen with Haskell. For example, we can
1078represent a person’s name and age in a record:
1080.. code-block:: idris
1083 constructor MkPerson
1084 firstName, middleName, lastName : String
1088 fred = MkPerson "Fred" "Joe" "Bloggs" 30
1090The constructor name is provided using the ``constructor`` keyword,
1091and the *fields* are then given which are in an indented block
1092following the `where` keyword (here, ``firstName``, ``middleName``,
1093``lastName``, and ``age``). You can declare multiple fields on a
1094single line, provided that they have the same type. The field names
1095can be used to access the field values:
1099 *Record> firstName fred
1103 *Record> :t firstName
1104 firstName : Person -> String
1106We can also use the field names to update a record (or, more
1107precisely, produce a copy of the record with the given fields
1112 *Record> record { firstName = "Jim" } fred
1113 MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1114 *Record> record { firstName = "Jim", age $= (+ 1) } fred
1115 MkPerson "Jim" "Joe" "Bloggs" 31 : Person
1117The syntax ``record { field = val, ... }`` generates a function which
1118updates the given fields in a record. ``=`` assigns a new value to a field,
1119and ``$=`` applies a function to update its value.
1121Each record is defined in its own namespace, which means that field names
1122can be reused in multiple records.
1124Records, and fields within records, can have dependent types. Updates
1125are allowed to change the type of a field, provided that the result is
1128.. code-block:: idris
1131 constructor ClassInfo
1132 students : Vect n Person
1135It is safe to update the ``students`` field to a vector of a different
1136length because it will not affect the type of the record:
1138.. code-block:: idris
1140 addStudent : Person -> Class -> Class
1141 addStudent p c = record { students = p :: students c } c
1145 *Record> addStudent fred (ClassInfo [] "CS")
1146 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1148We could also use ``$=`` to define ``addStudent`` more concisely:
1150.. code-block:: idris
1152 addStudent' : Person -> Class -> Class
1153 addStudent' p c = record { students $= (p ::) } c
1158Idris also provides a convenient syntax for accessing and updating
1159nested records. For example, if a field is accessible with the
1160expression ``c (b (a x))``, it can be updated using the following
1163.. code-block:: idris
1165 record { a->b->c = val } x
1167This returns a new record, with the field accessed by the path
1168``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
1169a->b->c = val }`` itself has a function type. Symmetrically, the field
1170can also be accessed with the following syntax:
1172.. code-block:: idris
1174 record { a->b->c } x
1176The ``$=`` notation is also valid for nested record updates.
1181Records can also be dependent on values. Records have *parameters*, which
1182cannot be updated like the other fields. The parameters appear as arguments
1183to the resulting type, and are written following the record type
1184name. For example, a pair type could be defined as follows:
1186.. code-block:: idris
1188 record Prod a b where
1193Using the ``Class`` record from earlier, the size of the class can be
1194restricted using a ``Vect`` and the size included in the type by parameterising
1195the record with the size. For example:
1197.. code-block:: idris
1199 record SizedClass (size : Nat) where
1200 constructor SizedClassInfo
1201 students : Vect size Person
1204**Note** that it is no longer possible to use the ``addStudent``
1205function from earlier, since that would change the size of the class. A
1206function to add a student must now specify in the type that the
1207size of the class has been increased by one. As the size is specified
1208using natural numbers, the new value can be incremented using the
1211.. code-block:: idris
1213 addStudent : Person -> SizedClass n -> SizedClass (S n)
1214 addStudent p c = SizedClassInfo (p :: students c) (className c)
1224Intermediate values can be calculated using ``let`` bindings:
1226.. code-block:: idris
1228 mirror : List a -> List a
1229 mirror xs = let xs' = reverse xs in
1232We can do simple pattern matching in ``let`` bindings too. For
1233example, we can extract fields from a record as follows, as well as by
1234pattern matching at the top level:
1236.. code-block:: idris
1238 data Person = MkPerson String Int
1240 showPerson : Person -> String
1241 showPerson p = let MkPerson name age = p in
1242 name ++ " is " ++ show age ++ " years old"
1247Idris provides *comprehension* notation as a convenient shorthand
1248for building lists. The general form is:
1252 [ expression | qualifiers ]
1254This generates the list of values produced by evaluating the
1255``expression``, according to the conditions given by the comma
1256separated ``qualifiers``. For example, we can build a list of
1257Pythagorean triples as follows:
1259.. code-block:: idris
1261 pythag : Int -> List (Int, Int, Int)
1262 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1265The ``[a..b]`` notation is another shorthand which builds a list of
1266numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1267list of numbers between ``a`` and ``c`` with the increment specified
1268by the difference between ``a`` and ``b``. This works for type ``Nat``,
1269``Int`` and ``Integer``, using the ``enumFromTo`` and ``enumFromThenTo``
1270function from the prelude.
1275Another way of inspecting intermediate values of *simple* types is to
1276use a ``case`` expression. The following function, for example, splits
1277a string into two at a given character:
1279.. code-block:: idris
1281 splitAt : Char -> String -> (String, String)
1282 splitAt c x = case break (== c) x of
1283 (x, y) => (x, strTail y)
1285``break`` is a library function which breaks a string into a pair of
1286strings at the point where the given function returns true. We then
1287deconstruct the pair it returns, and remove the first character of the
1290A ``case`` expression can match several cases, for example, to inspect
1291an intermediate value of type ``Maybe a``. Recall ``list_lookup``
1292which looks up an index in a list, returning ``Nothing`` if the index
1293is out of bounds. We can use this to write ``lookup_default``, which
1294looks up an index and returns a default value if the index is out of
1297.. code-block:: idris
1299 lookup_default : Nat -> List a -> a -> a
1300 lookup_default i xs def = case list_lookup i xs of
1304If the index is in bounds, we get the value at that index, otherwise
1305we get a default value:
1309 *UsefulTypes> lookup_default 2 [3,4,5,6] (-1)
1311 *UsefulTypes> lookup_default 4 [3,4,5,6] (-1)
1314**Restrictions:** The ``case`` construct is intended for simple
1315analysis of intermediate expressions to avoid the need to write
1316auxiliary functions, and is also used internally to implement pattern
1317matching ``let`` and lambda bindings. It will *only* work if:
1319- Each branch *matches* a value of the same type, and *returns* a
1320 value of the same type.
1322- The type of the result is “known”. i.e. the type of the expression
1323 can be determined *without* type checking the ``case``-expression
1329Idris distinguishes between *total* and *partial* functions.
1330A total function is a function that either:
1332+ Terminates for all possible inputs, or
1333+ Produces a non-empty, finite, prefix of a possibly infinite result
1335If a function is total, we can consider its type a precise description of what
1336that function will do. For example, if we have a function with a return
1337type of ``String`` we know something different, depending on whether or not
1340+ If it's total, it will return a value of type ``String`` in finite time;
1341+ If it's partial, then as long as it doesn't crash or enter an infinite loop,
1342 it will return a ``String``.
1344Idris makes this distinction so that it knows which functions are safe to
1345evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,
1346if it tries to evaluate a function during type checking which doesn't
1347terminate, then type checking won't terminate!
1348Therefore, only total functions will be evaluated during type checking.
1349Partial 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