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 their
541reduction behaviour to affect type checking. However, this restriction
542can be relaxed by using a ``mutual`` block, which allows data types
543and functions to be defined simultaneously:
556In a ``mutual`` block, first all of the type declarations are added,
557then the function bodies. As a result, none of the function types can
558depend on the reduction behaviour of any of the functions in the
564Computer programs are of little use if they do not interact with the
565user or the system in some way. The difficulty in a pure language such
566as Idris — that is, a language where expressions do not have
567side-effects — is that I/O is inherently side-effecting. Therefore in
568Idris, such interactions are encapsulated in the type ``IO``:
572 data IO a -- IO operation returning a value of type a
574We’ll leave the definition of ``IO`` abstract, but effectively it
575describes what the I/O operations to be executed are, rather than how
576to execute them. The resulting operations are executed externally, by
577the run-time system. We’ve already seen one IO program:
582 main = putStrLn "Hello world"
584The type of ``putStrLn`` explains that it takes a string, and returns
585an element of the unit type ``()`` via an I/O action. There is a
586variant ``putStr`` which outputs a string without a newline:
590 putStrLn : String -> IO ()
591 putStr : String -> IO ()
593We can also read strings from user input:
599A number of other I/O operations are defined in the prelude, for
600example for reading and writing files, including:
604 data File -- abstract
605 data Mode = Read | Write | ReadWrite
607 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
608 closeFile : File -> IO ()
610 fGetLine : (h : File) -> IO (Either FileError String)
611 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
612 fEOF : File -> IO Bool
614Note that several of these return ``Either``, since they may fail.
621I/O programs will typically need to sequence actions, feeding the
622output of one computation into the input of the next. ``IO`` is an
623abstract type, however, so we can’t access the result of a computation
624directly. Instead, we sequence operations with ``do`` notation:
629 greet = do putStr "What is your name? "
631 putStrLn ("Hello " ++ name)
633The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
634type ``IO a``, and puts the result, of type ``a`` into the variable
635``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
636has type ``String``. Indentation is significant — each statement in
637the do block must begin in the same column. The ``return`` operation
638allows us to inject a value directly into an IO operation:
644As we will see later, ``do`` notation is more general than this, and
652Normally, arguments to functions are evaluated before the function
653itself (that is, Idris uses *eager* evaluation). However, this is
654not always the best approach. Consider the following function:
658 ifThenElse : Bool -> a -> a -> a;
659 ifThenElse True t e = t;
660 ifThenElse False t e = e;
662This function uses one of the ``t`` or ``e`` arguments, but not both
663(in fact, this is used to implement the ``if...then...else`` construct
664as we will see later. We would prefer if *only* the argument which was
665used was evaluated. To achieve this, Idris provides a ``Lazy``
666data type, which allows evaluation to be suspended:
670 data Lazy : Type -> Type where
671 Delay : (val : a) -> Lazy a
675A value of type ``Lazy a`` is unevaluated until it is forced by
676``Force``. The Idris type checker knows about the ``Lazy`` type,
677and inserts conversions where necessary between ``Lazy a`` and ``a``,
678and vice versa. We can therefore write ``ifThenElse`` as follows,
679without any explicit use of ``Force`` or ``Delay``:
683 ifThenElse : Bool -> Lazy a -> Lazy a -> a;
684 ifThenElse True t e = t;
685 ifThenElse False t e = e;
690Idris includes a number of useful data types and library functions
691(see the ``libs/`` directory in the distribution). This chapter
692describes a few of these. The functions described here are imported
693automatically by every Idris program, as part of ``Prelude.idr``.
698We have already seen the ``List`` and ``Vect`` data types:
702 data List a = Nil | (::) a (List a)
704 data Vect : Nat -> Type -> Type where
706 (::) : a -> Vect k a -> Vect (S k) a
708Note that the constructor names are the same for each — constructor
709names (in fact, names in general) can be overloaded, provided that
710they are declared in different namespaces (see Section
711:ref:`sect-namespaces`), and will typically be resolved according to
712their type. As syntactic sugar, any type with the constructor names
713``Nil`` and ``::`` can be written in list form. For example:
715- ``[]`` means ``Nil``
717- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
719The library also defines a number of functions for manipulating these
720types. ``map`` is overloaded both for ``List`` and ``Vect`` and
721applies a function to every element of the list or vector.
725 map : (a -> b) -> List a -> List b
727 map f (x :: xs) = f x :: map f xs
729 map : (a -> b) -> Vect n a -> Vect n b
731 map f (x :: xs) = f x :: map f xs
733For example, given the following vector of integers, and a function to
739 intVec = [1, 2, 3, 4, 5]
744the function ``map`` can be used as follows to double every element in
749 *usefultypes> show (map double intVec)
750 "[2, 4, 6, 8, 10]" : String
752For more details of the functions available on ``List`` and
753``Vect``, look in the library files:
755- ``libs/prelude/Prelude/List.idr``
757- ``libs/base/Data/List.idr``
759- ``libs/base/Data/Vect.idr``
761- ``libs/base/Data/VectType.idr``
763Functions include filtering, appending, reversing, and so on. Also
764remember that Idris is still in development, so if you don’t see
765the function you need, please feel free to add it and submit a patch!
767Aside: Anonymous functions and operator sections
768~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
770There are actually neater ways to write the above expression. One way
771would be to use an anonymous function:
775 *usefultypes> show (map (\x => x * 2) intVec)
776 "[2, 4, 6, 8, 10]" : String
778The notation ``\x => val`` constructs an anonymous function which takes
779one argument, ``x`` and returns the expression ``val``. Anonymous
780functions may take several arguments, separated by commas,
781e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
782e.g. ``\x : Int => x * 2``, and can pattern match,
783e.g. ``\(x, y) => x + y``. We could also use an operator section:
787 *usefultypes> show (map (* 2) intVec)
788 "[2, 4, 6, 8, 10]" : String
790``(*2)`` is shorthand for a function which multiplies a number
791by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
797``Maybe`` describes an optional value. Either there is a value of the
798given type, or there isn’t:
802 data Maybe a = Just a | Nothing
804``Maybe`` is one way of giving a type to an operation that may
805fail. For example, looking something up in a ``List`` (rather than a
806vector) may result in an out of bounds error:
810 list_lookup : Nat -> List a -> Maybe a
811 list_lookup _ Nil = Nothing
812 list_lookup Z (x :: xs) = Just x
813 list_lookup (S k) (x :: xs) = list_lookup k xs
815The ``maybe`` function is used to process values of type ``Maybe``,
816either by applying a function to the value, if there is one, or by
817providing a default value:
821 maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
823Note that the types of the first two arguments are wrapped in
824``Lazy``. Since only one of the two arguments will actually be used,
825we mark them as ``Lazy`` in case they are large expressions where it
826would be wasteful to compute and then discard them.
831Values can be paired with the following built-in data type:
835 data Pair a b = MkPair a b
837As syntactic sugar, we can write ``(a, b)`` which, according to
838context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
839contain an arbitrary number of values, represented as nested pairs:
846 jim : (String, Int, String)
847 jim = ("Jim", 25, "Cambridge")
851 *usefultypes> fst jim
853 *usefultypes> snd jim
854 (25, "Cambridge") : (Int, String)
855 *usefultypes> jim == ("Jim", (25, "Cambridge"))
861Dependent pairs allow the type of the second element of a pair to depend
862on the value of the first element. Traditionally, these are referred to
867 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
868 MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P
870Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
871of a pair of A and P, where the name ``a`` can occur inside ``P``.
872``( a ** p )`` constructs a value of this type. For example, we can
873pair a number with a ``Vect`` of a particular length.
877 vec : (n : Nat ** Vect n Int)
880If you like, you can write it out the long way, the two are precisely
885 vec : Sigma Nat (\n => Vect n Int)
886 vec = MkSigma 2 [3, 4]
888The type checker could of course infer the value of the first element
889from the length of the vector. We can write an underscore ``_`` in
890place of values which we expect the type checker to fill in, so the
891above definition could also be written as:
895 vec : (n : Nat ** Vect n Int)
898We might also prefer to omit the type of the first element of the
899pair, since, again, it can be inferred:
903 vec : (n ** Vect n Int)
906One use for dependent pairs is to return values of dependent types
907where the index is not necessarily known in advance. For example, if
908we filter elements out of a ``Vect`` according to some predicate, we
909will not know in advance what the length of the resulting vector will
914 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
916If the ``Vect`` is empty, the result is easy:
920 filter p Nil = (_ ** [])
922In the ``::`` case, we need to inspect the result of a recursive call
923to ``filter`` to extract the length and the vector from the result. To
924do this, we use ``with`` notation, which allows pattern matching on
929 filter p (x :: xs) with (filter p xs)
930 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
932We will see more on ``with`` notation later.
938*Records* are data types which collect several values (the record's
939*fields*) together. Idris provides syntax for defining records and
940automatically generating field access and update functions. Unlike
941the syntax used for data structures, records in Idris follow a
942different syntax to that seen with Haskell. For example, we can
943represent a person's name and age in a record:
949 firstName, middleName, lastName : String
953 fred = MkPerson "Fred" "Joe" "Bloggs" 30
956The constructor name is provided using the ``constructor`` keyword,
957and the *fields* are then given which are in an indented block
958following the `where` keyword (here, ``firstName``, ``middleName``,
959``lastName``, and ``age``). You can declare multiple fields on a
960single line, provided that they have the same type. The field names
961can be used to access the field values:
965 *record> firstName fred
969 *record> :t firstName
970 firstName : Person -> String
972We can also use the field names to update a record (or, more
973precisely, produce a copy of the record with the given fields
978 *record> record { firstName = "Jim" } fred
979 MkPerson "Jim" "Joe" "Bloggs" 30 : Person
980 *record> record { firstName = "Jim", age = 20 } fred
981 MkPerson "Jim" "Joe" "Bloggs" 20 : Person
983The syntax ``record { field = val, ... }`` generates a function which
984updates the given fields in a record.
986Each record is defined in its own namespace, which means that field names
987can be reused in multiple records.
989Records, and fields within records, can have dependent types. Updates
990are allowed to change the type of a field, provided that the result is
996 constructor ClassInfo
997 students : Vect n Person
1000It is safe to update the ``students`` field to a vector of a different
1001length because it will not affect the type of the record:
1003.. code-block:: idris
1005 addStudent : Person -> Class -> Class
1006 addStudent p c = record { students = p :: students c } c
1010 *record> addStudent fred (ClassInfo [] "CS")
1011 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1017Idris also provides a convenient syntax for accessing and updating
1018nested records. For example, if a field is accessible with the
1019expression ``c (b (a x))``, it can be updated using the following
1022.. code-block:: idris
1024 record { a->b->c = val } x
1026This returns a new record, with the field accessed by the path
1027``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
1028a->b->c = val }`` itself has a function type. Symmetrically, the field
1029can also be accessed with the following syntax:
1031.. code-block:: idris
1033 record { a->b->c } x
1039Records can also be dependent on values. Records *parameters*, which
1040are not subject to field updates. The parameters appear as arguments
1041to the resulting type, and are written following the record type
1042name. For example, a pair type could be defined as follows:
1044.. code-block:: idris
1046 record Prod a b where
1052Using the class record from the original introduction to records. The
1053size of the class can be restricted using a ``Vect`` and the size
1054promoted to the type level by parameterising the record with the size.
1058.. code-block:: idris
1060 record SizedClass (size : Nat) where
1061 constructor SizedClassInfo
1062 students : Vect size Person
1065**Note** that it is no longer possible to use the ``addStudent``
1066function from earlier, since that would change the size of the class. A
1067function to add a student must now specify in the type that the
1068size of the class has been increased by one. As the size is specified
1069using natural numbers, the new value can be incremented using the
1072.. code-block:: idris
1074 addStudent : Person -> SizedClass n -> SizedClass (S n)
1075 addStudent p c = SizedClassInfo (p :: students c) (className c)
1085Intermediate values can be calculated using ``let`` bindings:
1087.. code-block:: idris
1089 mirror : List a -> List a
1090 mirror xs = let xs' = reverse xs in
1093We can do simple pattern matching in ``let`` bindings too. For
1094example, we can extract fields from a record as follows, as well as by
1095pattern matching at the top level:
1097.. code-block:: idris
1099 data Person = MkPerson String Int
1101 showPerson : Person -> String
1102 showPerson p = let MkPerson name age = p in
1103 name ++ " is " ++ show age ++ " years old"
1108Idris provides *comprehension* notation as a convenient shorthand
1109for building lists. The general form is:
1113 [ expression | qualifiers ]
1115This generates the list of values produced by evaluating the
1116``expression``, according to the conditions given by the comma
1117separated ``qualifiers``. For example, we can build a list of
1118Pythagorean triples as follows:
1120.. code-block:: idris
1122 pythag : Int -> List (Int, Int, Int)
1123 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1126The ``[a..b]`` notation is another shorthand which builds a list of
1127numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1128list of numbers between ``a`` and ``c`` with the increment specified
1129by the difference between ``a`` and ``b``. This works for any numeric
1130type, using the ``count`` function from the prelude.
1135Another way of inspecting intermediate values of *simple* types is to
1136use a ``case`` expression. The following function, for example, splits
1137a string into two at a given character:
1139.. code-block:: idris
1141 splitAt : Char -> String -> (String, String)
1142 splitAt c x = case break (== c) x of
1143 (x, y) => (x, strTail y)
1145``break`` is a library function which breaks a string into a pair of
1146strings at the point where the given function returns true. We then
1147deconstruct the pair it returns, and remove the first character of the
1150A ``case`` expression can match several cases, for example, to inspect
1151an intermediate value of type ``Maybe a``. Recall ``list_lookup``
1152which looks up an index in a list, returning ``Nothing`` if the index
1153is out of bounds. We can use this to write ``lookup_default``, which
1154looks up an index and returns a default value if the index is out of
1157.. code-block:: idris
1159 lookup_default : Nat -> List a -> a -> a
1160 lookup_default i xs def = case list_lookup i xs of
1164If the index is in bounds, we get the value at that index, otherwise
1165we get a default value:
1169 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
1171 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
1174**Restrictions:** The ``case`` construct is intended for simple
1175analysis of intermediate expressions to avoid the need to write
1176auxiliary functions, and is also used internally to implement pattern
1177matching ``let`` and lambda bindings. It will *only* work if:
1179- Each branch *matches* a value of the same type, and *returns* a
1180 value of the same type.
1182- The type of the result is "known". i.e. the type of the expression
1183 can be determined *without* type checking the ``case``-expression
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