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. We can test these functions at the
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)
259In Idris, types are a first class language construct, meaning that they
260can be computed and manipulated (and passed to functions) just like any
261other language construct. For example, we could write a function which
266 isSingleton : Bool -> Type
267 isSingleton True = Nat
268 isSingleton False = List Nat
270This function calculates the appropriate type from a ``Bool`` which flags
271whether the type should be a singleton or not. We can use this function
272to calculate a type anywhere that a type can be used. For example, it
273can be used to calculate a return type:
277 mkSingle : (x : Bool) -> isSingleton x
281Or it can be used to have varying input types. The following function
282calculates either the sum of a list of ``Nat``, or returns the given
283``Nat``, depending on whether the singleton flag is true:
287 sum : (single : Bool) -> isSingleton single -> Nat
290 sum False (x :: xs) = x + sum False xs
295A standard example of a dependent data type is the type of “lists with
296length”, conventionally called vectors in the dependent type
297literature. They are available as part of the Idris library, by
298importing ``Data.Vect``, or we can declare them as follows:
302 data Vect : Nat -> Type -> Type where
304 (::) : a -> Vect k a -> Vect (S k) a
306Note that we have used the same constructor names as for ``List``.
307Ad-hoc name overloading such as this is accepted by Idris,
308provided that the names are declared in different namespaces (in
309practice, normally in different modules). Ambiguous constructor names
310can normally be resolved from context.
312This declares a family of types, and so the form of the declaration is
313rather different from the simple type declarations above. We
314explicitly state the type of the type constructor ``Vect`` — it takes
315a ``Nat`` and a type as an argument, where ``Type`` stands for the
316type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
317*parameterised* by ``Type``. Each constructor targets a different part
318of the family of types. ``Nil`` can only be used to construct vectors
319with zero length, and ``::`` to construct vectors with non-zero
320length. In the type of ``::``, we state explicitly that an element of
321type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
322``k``) combine to make a vector of length ``S k``.
324We can define functions on dependent types such as ``Vect`` in the same
325way as on simple types such as ``List`` and ``Nat`` above, by pattern
326matching. The type of a function over ``Vect`` will describe what
327happens to the lengths of the vectors involved. For example, ``++``,
328defined as follows, appends two ``Vect``:
332 (++) : Vect n a -> Vect m a -> Vect (n + m) a
334 (++) (x :: xs) ys = x :: xs ++ ys
336The type of ``(++)`` states that the resulting vector’s length will be
337the sum of the input lengths. If we get the definition wrong in such a
338way that this does not hold, Idris will not accept the definition.
343 (++) : Vect n a -> Vect m a -> Vect (n + m) a
345 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
347When run through the Idris type checker, this results in the
352 $ idris vbroken.idr --check
353 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
354 When elaborating an application of constructor Vect.:::
355 Type mismatch between
356 Vect (k + k) a (Type of xs ++ xs)
358 Vect (plus k m) a (Expected type)
361 Type mismatch between
367This error message suggests that there is a length mismatch between
368two vectors — we needed a vector of length ``k + m``, but provided a
369vector of length ``k + k``.
374Finite sets, as the name suggests, are sets with a finite number of
375elements. They are available as part of the Idris library, by
376importing ``Data.Fin``, or can be declared as follows:
380 data Fin : Nat -> Type where
382 FS : Fin k -> Fin (S k)
384From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
385So this is not a set in the sense of a collection that is a container of objects,
386rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
387Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
388``n`` is the argument used to instantiate the ``Fin`` type.
389For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
391Let us look at the constructors in greater detail.
393``FZ`` is the zeroth element of a finite set with ``S k`` elements;
394``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
395elements. ``Fin`` is indexed by a ``Nat``, which represents the number
396of elements in the set. Since we can’t construct an element of an
397empty set, neither constructor targets ``Fin Z``.
399As mentioned above, a useful application of the ``Fin`` family is to
400represent bounded natural numbers. Since the first ``n`` natural
401numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
402the set of integers greater than or equal to zero and less than ``n``.
404For example, the following function which looks up an element in a
405``Vect``, by a bounded index given as a ``Fin n``, is defined in the
410 index : Fin n -> Vect n a -> a
411 index FZ (x :: xs) = x
412 index (FS k) (x :: xs) = index k xs
414This function looks up a value at a given location in a vector. The
415location is bounded by the length of the vector (``n`` in each case),
416so there is no need for a run-time bounds check. The type checker
417guarantees that the location is no larger than the length of the
418vector, and of course no less than zero.
420Note also that there is no case for ``Nil`` here. This is because it
421is impossible. Since there is no element of ``Fin Z``, and the
422location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
423attempting to look up an element in an empty vector would give a
424compile time type error, since it would force ``n`` to be ``Z``.
429Let us take a closer look at the type of ``index``:
433 index : Fin n -> Vect n a -> a
435It takes two arguments, an element of the finite set of ``n`` elements,
436and a vector with ``n`` elements of type ``a``. But there are also two
437names, ``n`` and ``a``, which are not declared explicitly. These are
438*implicit* arguments to ``index``. We could also write the type of
443 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
445Implicit arguments, given in braces ``{}`` in the type declaration,
446are not given in applications of ``index``; their values can be
447inferred from the types of the ``Fin n`` and ``Vect n a``
448arguments. Any name beginning with a lower case letter which appears
449as a parameter or index in a
450type declaration, which is not applied to any arguments, will
451*always* be automatically
452bound as an implicit argument. Implicit arguments can still be given
453explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
458 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
460In fact, any argument, implicit or explicit, may be given a name. We
461could have declared the type of ``index`` as:
465 index : (i:Fin n) -> (xs:Vect n a) -> a
467It is a matter of taste whether you want to do this — sometimes it can
468help document a function by making the purpose of an argument more
474Sometimes it is useful to provide types of implicit arguments,
475particularly where there is a dependency ordering, or where the
476implicit arguments themselves have dependencies. For example, we may
477wish to state the types of the implicit arguments in the following
478definition, which defines a predicate on vectors (this is also defined
479in ``Data.Vect``, under the name ``Elem``):
483 data IsElem : a -> Vect n a -> Type where
484 Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
485 There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
487An instance of ``IsElem x xs`` states that ``x`` is an element of
488``xs``. We can construct such a predicate if the required element is
489``Here``, at the head of the vector, or ``There``, in the tail of the
495 testVec = 3 :: 4 :: 5 :: 6 :: Nil
497 inVect : IsElem 5 testVec
498 inVect = There (There Here)
500If the same implicit arguments are being used a lot, it can make a
501definition difficult to read. To avoid this problem, a ``using`` block
502gives the types and ordering of any implicit arguments which can
503appear within the block:
507 using (x:a, y:a, xs:Vect n a)
508 data IsElem : a -> Vect n a -> Type where
509 Here : IsElem x (x :: xs)
510 There : IsElem x xs -> IsElem x (y :: xs)
512Note: Declaration Order and ``mutual`` blocks
513~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
515In general, functions and data types must be defined before use, since
516dependent types allow functions to appear as part of types, and their
517reduction behaviour to affect type checking. However, this restriction
518can be relaxed by using a ``mutual`` block, which allows data types
519and functions to be defined simultaneously:
532In a ``mutual`` block, first all of the type declarations are added,
533then the function bodies. As a result, none of the function types can
534depend on the reduction behaviour of any of the functions in the
540Computer programs are of little use if they do not interact with the
541user or the system in some way. The difficulty in a pure language such
542as Idris — that is, a language where expressions do not have
543side-effects — is that I/O is inherently side-effecting. Therefore in
544Idris, such interactions are encapsulated in the type ``IO``:
548 data IO a -- IO operation returning a value of type a
550We’ll leave the definition of ``IO`` abstract, but effectively it
551describes what the I/O operations to be executed are, rather than how
552to execute them. The resulting operations are executed externally, by
553the run-time system. We’ve already seen one IO program:
558 main = putStrLn "Hello world"
560The type of ``putStrLn`` explains that it takes a string, and returns
561an element of the unit type ``()`` via an I/O action. There is a
562variant ``putStr`` which outputs a string without a newline:
566 putStrLn : String -> IO ()
567 putStr : String -> IO ()
569We can also read strings from user input:
575A number of other I/O operations are defined in the prelude, for
576example for reading and writing files, including:
580 data File -- abstract
581 data Mode = Read | Write | ReadWrite
583 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
584 closeFile : File -> IO ()
586 fGetLine : (h : File) -> IO (Either FileError String)
587 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
588 fEOF : File -> IO Bool
590Note that several of these return ``Either``, since they may fail.
597I/O programs will typically need to sequence actions, feeding the
598output of one computation into the input of the next. ``IO`` is an
599abstract type, however, so we can’t access the result of a computation
600directly. Instead, we sequence operations with ``do`` notation:
605 greet = do putStr "What is your name? "
607 putStrLn ("Hello " ++ name)
609The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
610type ``IO a``, and puts the result, of type ``a`` into the variable
611``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
612has type ``String``. Indentation is significant — each statement in
613the do block must begin in the same column. The ``return`` operation
614allows us to inject a value directly into an IO operation:
620As we will see later, ``do`` notation is more general than this, and
628Normally, arguments to functions are evaluated before the function
629itself (that is, Idris uses *eager* evaluation). However, this is
630not always the best approach. Consider the following function:
634 ifThenElse : Bool -> a -> a -> a;
635 ifThenElse True t e = t;
636 ifThenElse False t e = e;
638This function uses one of the ``t`` or ``e`` arguments, but not both
639(in fact, this is used to implement the ``if...then...else`` construct
640as we will see later. We would prefer if *only* the argument which was
641used was evaluated. To achieve this, Idris provides a ``Lazy``
642data type, which allows evaluation to be suspended:
646 data Lazy : Type -> Type where
647 Delay : (val : a) -> Lazy a
651A value of type ``Lazy a`` is unevaluated until it is forced by
652``Force``. The Idris type checker knows about the ``Lazy`` type,
653and inserts conversions where necessary between ``Lazy a`` and ``a``,
654and vice versa. We can therefore write ``ifThenElse`` as follows,
655without any explicit use of ``Force`` or ``Delay``:
659 ifThenElse : Bool -> Lazy a -> Lazy a -> a;
660 ifThenElse True t e = t;
661 ifThenElse False t e = e;
666Idris includes a number of useful data types and library functions
667(see the ``libs/`` directory in the distribution). This chapter
668describes a few of these. The functions described here are imported
669automatically by every Idris program, as part of ``Prelude.idr``.
674We have already seen the ``List`` and ``Vect`` data types:
678 data List a = Nil | (::) a (List a)
680 data Vect : Nat -> Type -> Type where
682 (::) : a -> Vect k a -> Vect (S k) a
684Note that the constructor names are the same for each — constructor
685names (in fact, names in general) can be overloaded, provided that
686they are declared in different namespaces (see Section
687:ref:`sect-namespaces`), and will typically be resolved according to
688their type. As syntactic sugar, any type with the constructor names
689``Nil`` and ``::`` can be written in list form. For example:
691- ``[]`` means ``Nil``
693- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
695The library also defines a number of functions for manipulating these
696types. ``map`` is overloaded both for ``List`` and ``Vect`` and
697applies a function to every element of the list or vector.
701 map : (a -> b) -> List a -> List b
703 map f (x :: xs) = f x :: map f xs
705 map : (a -> b) -> Vect n a -> Vect n b
707 map f (x :: xs) = f x :: map f xs
709For example, given the following vector of integers, and a function to
715 intVec = [1, 2, 3, 4, 5]
720the function ``map`` can be used as follows to double every element in
725 *usefultypes> show (map double intVec)
726 "[2, 4, 6, 8, 10]" : String
728For more details of the functions available on ``List`` and
729``Vect``, look in the library files:
731- ``libs/prelude/Prelude/List.idr``
733- ``libs/base/Data/List.idr``
735- ``libs/base/Data/Vect.idr``
737- ``libs/base/Data/VectType.idr``
739Functions include filtering, appending, reversing, and so on. Also
740remember that Idris is still in development, so if you don’t see
741the function you need, please feel free to add it and submit a patch!
743Aside: Anonymous functions and operator sections
744~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
746There are actually neater ways to write the above expression. One way
747would be to use an anonymous function:
751 *usefultypes> show (map (\x => x * 2) intVec)
752 "[2, 4, 6, 8, 10]" : String
754The notation ``\x => val`` constructs an anonymous function which takes
755one argument, ``x`` and returns the expression ``val``. Anonymous
756functions may take several arguments, separated by commas,
757e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
758e.g. ``\x : Int => x * 2``, and can pattern match,
759e.g. ``\(x, y) => x + y``. We could also use an operator section:
763 *usefultypes> show (map (* 2) intVec)
764 "[2, 4, 6, 8, 10]" : String
766``(*2)`` is shorthand for a function which multiplies a number
767by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
773``Maybe`` describes an optional value. Either there is a value of the
774given type, or there isn’t:
778 data Maybe a = Just a | Nothing
780``Maybe`` is one way of giving a type to an operation that may
781fail. For example, looking something up in a ``List`` (rather than a
782vector) may result in an out of bounds error:
786 list_lookup : Nat -> List a -> Maybe a
787 list_lookup _ Nil = Nothing
788 list_lookup Z (x :: xs) = Just x
789 list_lookup (S k) (x :: xs) = list_lookup k xs
791The ``maybe`` function is used to process values of type ``Maybe``,
792either by applying a function to the value, if there is one, or by
793providing a default value:
797 maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
799Note that the types of the first two arguments are wrapped in
800``Lazy``. Since only one of the two arguments will actually be used,
801we mark them as ``Lazy`` in case they are large expressions where it
802would be wasteful to compute and then discard them.
807Values can be paired with the following built-in data type:
811 data Pair a b = MkPair a b
813As syntactic sugar, we can write ``(a, b)`` which, according to
814context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
815contain an arbitrary number of values, represented as nested pairs:
822 jim : (String, Int, String)
823 jim = ("Jim", 25, "Cambridge")
827 *usefultypes> fst jim
829 *usefultypes> snd jim
830 (25, "Cambridge") : (Int, String)
831 *usefultypes> jim == ("Jim", (25, "Cambridge"))
837Dependent pairs allow the type of the second element of a pair to depend
838on the value of the first element. Traditionally, these are referred to
843 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
844 MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P
846Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
847of a pair of A and P, where the name ``a`` can occur inside ``P``.
848``( a ** p )`` constructs a value of this type. For example, we can
849pair a number with a ``Vect`` of a particular length.
853 vec : (n : Nat ** Vect n Int)
856If you like, you can write it out the long way, the two are precisely
861 vec : Sigma Nat (\n => Vect n Int)
862 vec = MkSigma 2 [3, 4]
864The type checker could of course infer the value of the first element
865from the length of the vector. We can write an underscore ``_`` in
866place of values which we expect the type checker to fill in, so the
867above definition could also be written as:
871 vec : (n : Nat ** Vect n Int)
874We might also prefer to omit the type of the first element of the
875pair, since, again, it can be inferred:
879 vec : (n ** Vect n Int)
882One use for dependent pairs is to return values of dependent types
883where the index is not necessarily known in advance. For example, if
884we filter elements out of a ``Vect`` according to some predicate, we
885will not know in advance what the length of the resulting vector will
890 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
892If the ``Vect`` is empty, the result is easy:
896 filter p Nil = (_ ** [])
898In the ``::`` case, we need to inspect the result of a recursive call
899to ``filter`` to extract the length and the vector from the result. To
900do this, we use ``with`` notation, which allows pattern matching on
905 filter p (x :: xs) with (filter p xs)
906 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
908We will see more on ``with`` notation later.
914*Records* are data types which collect several values (the record's
915*fields*) together. Idris provides syntax for defining records and
916automatically generating field access and update functions. Unlike
917the syntax used for data structures, records in Idris follow a
918different syntax to that seen with Haskell. For example, we can
919represent a person's name and age in a record:
925 firstName, middleName, lastName : String
929 fred = MkPerson "Fred" "Joe" "Bloggs" 30
932The constructor name is provided using the ``constructor`` keyword,
933and the *fields* are then given which are in an indented block
934following the `where` keyword (here, ``firstName``, ``middleName``,
935``lastName``, and ``age``). You can declare multiple fields on a
936single line, provided that they have the same type. The field names
937can be used to access the field values:
941 *record> firstName fred
945 *record> :t firstName
946 firstName : Person -> String
948We can also use the field names to update a record (or, more
949precisely, produce a copy of the record with the given fields
954 *record> record { firstName = "Jim" } fred
955 MkPerson "Jim" "Joe" "Bloggs" 30 : Person
956 *record> record { firstName = "Jim", age = 20 } fred
957 MkPerson "Jim" "Joe" "Bloggs" 20 : Person
959The syntax ``record { field = val, ... }`` generates a function which
960updates the given fields in a record.
962Records, and fields within records, can have dependent types. Updates
963are allowed to change the type of a field, provided that the result is
969 constructor ClassInfo
970 students : Vect n Person
973It is safe to update the ``students`` field to a vector of a different
974length because it will not affect the type of the record:
978 addStudent : Person -> Class -> Class
979 addStudent p c = record { students = p :: students c } c
983 *record> addStudent fred (ClassInfo [] "CS")
984 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
990Idris also provides a convenient syntax for accessing and updating
991nested records. For example, if a field is accessible with the
992expression ``c (b (a x))``, it can be updated using the following
997 record { a->b->c = val } x
999This returns a new record, with the field accessed by the path
1000``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
1001a->b->c = val }`` itself has a function type. Symmetrically, the field
1002can also be accessed with the following syntax:
1004.. code-block:: idris
1006 record { a->b->c } x
1012Records can also be dependent on values. Records *parameters*, which
1013are not subject to field updates. The parameters appear as arguments
1014to the resulting type, and are written following the record type
1015name. For example, a pair type could be defined as follows:
1017.. code-block:: idris
1019 record Prod a b where
1025Using the class record from the original introduction to records. The
1026size of the class can be restricted using a ``Vect`` and the size
1027promoted to the type level by parameterising the record with the size.
1031.. code-block:: idris
1033 record SizedClass (size : Nat) where
1034 constructor SizedClassInfo
1035 students : Vect size Person
1038**Note** that it is no longer possible to use the ``addStudent``
1039function from earlier, since that would change the size of the class. A
1040function to add a student must now specify in the type that the
1041size of the class has been increased by one. As the size is specified
1042using natural numbers, the new value can be incremented using the
1045.. code-block:: idris
1047 addStudent : Person -> SizedClass n -> SizedClass (S n)
1048 addStudent p c = SizedClassInfo (p :: students c) (className c)
1058Intermediate values can be calculated using ``let`` bindings:
1060.. code-block:: idris
1062 mirror : List a -> List a
1063 mirror xs = let xs' = reverse xs in
1066We can do simple pattern matching in ``let`` bindings too. For
1067example, we can extract fields from a record as follows, as well as by
1068pattern matching at the top level:
1070.. code-block:: idris
1072 data Person = MkPerson String Int
1074 showPerson : Person -> String
1075 showPerson p = let MkPerson name age = p in
1076 name ++ " is " ++ show age ++ " years old"
1081Idris provides *comprehension* notation as a convenient shorthand
1082for building lists. The general form is:
1086 [ expression | qualifiers ]
1088This generates the list of values produced by evaluating the
1089``expression``, according to the conditions given by the comma
1090separated ``qualifiers``. For example, we can build a list of
1091Pythagorean triples as follows:
1093.. code-block:: idris
1095 pythag : Int -> List (Int, Int, Int)
1096 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1099The ``[a..b]`` notation is another shorthand which builds a list of
1100numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
1101list of numbers between ``a`` and ``c`` with the increment specified
1102by the difference between ``a`` and ``b``. This works for any numeric
1103type, using the ``count`` function from the prelude.
1108Another way of inspecting intermediate values of *simple* types is to
1109use a ``case`` expression. The following function, for example, splits
1110a string into two at a given character:
1112.. code-block:: idris
1114 splitAt : Char -> String -> (String, String)
1115 splitAt c x = case break (== c) x of
1116 (x, y) => (x, strTail y)
1118``break`` is a library function which breaks a string into a pair of
1119strings at the point where the given function returns true. We then
1120deconstruct the pair it returns, and remove the first character of the
1123A ``case`` expression can match several cases, for example, to inspect
1124an intermediate value of type ``Maybe a``. Recall ``list_lookup``
1125which looks up an index in a list, returning ``Nothing`` if the index
1126is out of bounds. We can use this to write ``lookup_default``, which
1127looks up an index and returns a default value if the index is out of
1130.. code-block:: idris
1132 lookup_default : Nat -> List a -> a -> a
1133 lookup_default i xs def = case list_lookup i xs of
1137If the index is in bounds, we get the value at that index, otherwise
1138we get a default value:
1142 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
1144 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
1147**Restrictions:** The ``case`` construct is intended for simple
1148analysis of intermediate expressions to avoid the need to write
1149auxiliary functions, and is also used internally to implement pattern
1150matching ``let`` and lambda bindings. It will *only* work if:
1152- Each branch *matches* a value of the same type, and *returns* a
1153 value of the same type.
1155- The type of the result is "known". i.e. the type of the expression
1156 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