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 type classes, as we
65will discuss in Section :ref:`sect-classes` 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 Idris automatically desugars the ``Nat`` representation into a
153 more human readable format. The result of ``plus (S (S Z)) (S (S Z))``
154 is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be
155 checked at the Idris prompt:
159 Idris> (S (S (S (S Z))))
162Like arithmetic operations, integer literals are also overloaded using
163type classes, meaning that we can also test the functions as follows:
169 Idris> mult 3 (plus 2 2)
172You may wonder, by the way, why we have unary natural numbers when our
173computers have perfectly good integer arithmetic built in. The reason
174is primarily that unary numbers have a very convenient structure which
175is easy to reason about, and easy to relate to other data structures
176as we will see later. Nevertheless, we do not want this convenience to
177be at the expense of efficiency. Fortunately, Idris knows about
178the relationship between ``Nat`` (and similarly structured types) and
179numbers. This means it can optimise the representation, and functions
180such as ``plus`` and ``mult``.
185Functions can also be defined *locally* using ``where`` clauses. For
186example, to define a function which reverses a list, we can use an
187auxiliary function which accumulates the new, reversed list, and which
188does not need to be visible globally:
192 reverse : List a -> List a
193 reverse xs = revAcc [] xs where
194 revAcc : List a -> List a -> List a
196 revAcc acc (x :: xs) = revAcc (x :: acc) xs
198Indentation is significant — functions in the ``where`` block must be
199indented further than the outer function.
203 Any names which are visible in the outer scope are also visible in
204 the ``where`` clause (unless they have been redefined, such as ``xs``
205 here). A name which appears only in the type will be in scope in the
206 ``where`` clause if it is a *parameter* to one of the types, i.e. it
207 is fixed across the entire structure.
209As well as functions, ``where`` blocks can include local data
210declarations, such as the following where ``MyLT`` is not accessible
211outside the definition of ``foo``:
223 isLT = if x < 20 then Yes else No
225In general, functions defined in a ``where`` clause need a type
226declaration just like any top level function. However, the type
227declaration for a function ``f`` *can* be omitted if:
229- ``f`` appears in the right hand side of the top level definition
231- The type of ``f`` can be completely determined from its first application
234So, for example, the following definitions are legal:
240 even (S k) = odd k where
245 test = [c (S 1), c Z, d (S Z)]
247 d y = c (y + 1 + z y)
257In Idris, types are a first class language construct, meaning that they
258can be computed and manipulated (and passed to functions) just like any
259other language construct. For example, we could write a function which
264 isSingleton : Bool -> Type
265 isSingleton True = Nat
266 isSingleton False = List Nat
268This function calculates the appropriate type from a ``Bool`` which flags
269whether the type should be a singleton or not. We can use this function
270to calculate a type anywhere that a type can be used. For example, it
271can be used to calculate a return type:
275 mkSingle : (x : Bool) -> isSingleton x
279Or it can be used to have varying input types. The following function
280calculates either the sum of a list of ``Nat``, or returns the given
281``Nat``, depending on whether the singleton flag is true:
285 sum : (single : Bool) -> isSingleton single -> Nat
288 sum False (x :: xs) = x + sum False xs
293A standard example of a dependent data type is the type of “lists with
294length”, conventionally called vectors in the dependent type
295literature. They are available as part of the Idris library, by
296importing ``Data.Vect``, or we can declare them as follows:
300 data Vect : Nat -> Type -> Type where
302 (::) : a -> Vect k a -> Vect (S k) a
304Note that we have used the same constructor names as for ``List``.
305Ad-hoc name overloading such as this is accepted by Idris,
306provided that the names are declared in different namespaces (in
307practice, normally in different modules). Ambiguous constructor names
308can normally be resolved from context.
310This declares a family of types, and so the form of the declaration is
311rather different from the simple type declarations above. We
312explicitly state the type of the type constructor ``Vect`` — it takes
313a ``Nat`` and a type as an argument, where ``Type`` stands for the
314type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
315*parameterised* by ``Type``. Each constructor targets a different part
316of the family of types. ``Nil`` can only be used to construct vectors
317with zero length, and ``::`` to construct vectors with non-zero
318length. In the type of ``::``, we state explicitly that an element of
319type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
320``k``) combine to make a vector of length ``S k``.
322We can define functions on dependent types such as ``Vect`` in the same
323way as on simple types such as ``List`` and ``Nat`` above, by pattern
324matching. The type of a function over ``Vect`` will describe what
325happens to the lengths of the vectors involved. For example, ``++``,
326defined as follows, appends two ``Vect``:
330 (++) : Vect n a -> Vect m a -> Vect (n + m) a
332 (++) (x :: xs) ys = x :: xs ++ ys
334The type of ``(++)`` states that the resulting vector’s length will be
335the sum of the input lengths. If we get the definition wrong in such a
336way that this does not hold, Idris will not accept the definition.
341 (++) : Vect n a -> Vect m a -> Vect (n + m) a
343 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
345When run through the Idris type checker, this results in the
350 $ idris vbroken.idr --check
351 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
352 When elaborating an application of constructor Vect.:::
353 Type mismatch between
354 Vect (k + k) a (Type of xs ++ xs)
356 Vect (plus k m) a (Expected type)
359 Type mismatch between
365This error message suggests that there is a length mismatch between
366two vectors — we needed a vector of length ``k + m``, but provided a
367vector of length ``k + k``.
372Finite sets, as the name suggests, are sets with a finite number of
373elements. They are available as part of the Idris library, by
374importing ``Data.Fin``, or can be declared as follows:
378 data Fin : Nat -> Type where
380 FS : Fin k -> Fin (S k)
382From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
383So this is not a set in the sense of a collection that is a container of objects,
384rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
385Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
386``n`` is the argument used to instantiate the ``Fin`` type.
387For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
389Let us look at the constructors in greater detail.
391``FZ`` is the zeroth element of a finite set with ``S k`` elements;
392``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
393elements. ``Fin`` is indexed by a ``Nat``, which represents the number
394of elements in the set. Since we can’t construct an element of an
395empty set, neither constructor targets ``Fin Z``.
397As mentioned above, a useful application of the ``Fin`` family is to
398represent bounded natural numbers. Since the first ``n`` natural
399numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
400the set of integers greater than or equal to zero and less than ``n``.
402For example, the following function which looks up an element in a
403``Vect``, by a bounded index given as a ``Fin n``, is defined in the
408 index : Fin n -> Vect n a -> a
409 index FZ (x :: xs) = x
410 index (FS k) (x :: xs) = index k xs
412This function looks up a value at a given location in a vector. The
413location is bounded by the length of the vector (``n`` in each case),
414so there is no need for a run-time bounds check. The type checker
415guarantees that the location is no larger than the length of the
416vector, and of course no less than zero.
418Note also that there is no case for ``Nil`` here. This is because it
419is impossible. Since there is no element of ``Fin Z``, and the
420location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
421attempting to look up an element in an empty vector would give a
422compile time type error, since it would force ``n`` to be ``Z``.
427Let us take a closer look at the type of ``index``:
431 index : Fin n -> Vect n a -> a
433It takes two arguments, an element of the finite set of ``n`` elements,
434and a vector with ``n`` elements of type ``a``. But there are also two
435names, ``n`` and ``a``, which are not declared explicitly. These are
436*implicit* arguments to ``index``. We could also write the type of
441 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
443Implicit arguments, given in braces ``{}`` in the type declaration,
444are not given in applications of ``index``; their values can be
445inferred from the types of the ``Fin n`` and ``Vect n a``
446arguments. Any name beginning with a lower case letter which appears
447as a parameter or index in a
448type declaration, which is not applied to any arguments, will
449*always* be automatically
450bound as an implicit argument. Implicit arguments can still be given
451explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
456 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
458In fact, any argument, implicit or explicit, may be given a name. We
459could have declared the type of ``index`` as:
463 index : (i:Fin n) -> (xs:Vect n a) -> a
465It is a matter of taste whether you want to do this — sometimes it can
466help document a function by making the purpose of an argument more
472Sometimes it is useful to provide types of implicit arguments,
473particularly where there is a dependency ordering, or where the
474implicit arguments themselves have dependencies. For example, we may
475wish to state the types of the implicit arguments in the following
476definition, which defines a predicate on vectors:
480 data Elem : a -> Vect n a -> Type where
481 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
482 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
484An instance of ``Elem x xs`` states that ``x`` is an element of
485``xs``. We can construct such a predicate if the required element is
486``Here``, at the head of the vector, or ``There``, in the tail of the
492 testVec = 3 :: 4 :: 5 :: 6 :: Nil
494 inVect : Elem 5 testVec
495 inVect = There (There Here)
497If the same implicit arguments are being used a lot, it can make a
498definition difficult to read. To avoid this problem, a ``using`` block
499gives the types and ordering of any implicit arguments which can
500appear within the block:
504 using (x:a, y:a, xs:Vect n a)
505 data Elem : a -> Vect n a -> Type where
506 Here : Elem x (x :: xs)
507 There : Elem x xs -> Elem x (y :: xs)
509Note: Declaration Order and ``mutual`` blocks
510~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
512In general, functions and data types must be defined before use, since
513dependent types allow functions to appear as part of types, and their
514reduction behaviour to affect type checking. However, this restriction
515can be relaxed by using a ``mutual`` block, which allows data types
516and functions to be defined simultaneously:
529In a ``mutual`` block, first all of the type declarations are added,
530then the function bodies. As a result, none of the function types can
531depend on the reduction behaviour of any of the functions in the
537Computer programs are of little use if they do not interact with the
538user or the system in some way. The difficulty in a pure language such
539as Idris — that is, a language where expressions do not have
540side-effects — is that I/O is inherently side-effecting. Therefore in
541Idris, such interactions are encapsulated in the type ``IO``:
545 data IO a -- IO operation returning a value of type a
547We’ll leave the definition of ``IO`` abstract, but effectively it
548describes what the I/O operations to be executed are, rather than how
549to execute them. The resulting operations are executed externally, by
550the run-time system. We’ve already seen one IO program:
555 main = putStrLn "Hello world"
557The type of ``putStrLn`` explains that it takes a string, and returns
558an element of the unit type ``()`` via an I/O action. There is a
559variant ``putStr`` which outputs a string without a newline:
563 putStrLn : String -> IO ()
564 putStr : String -> IO ()
566We can also read strings from user input:
572A number of other I/O operations are defined in the prelude, for
573example for reading and writing files, including:
577 data File -- abstract
578 data Mode = Read | Write | ReadWrite
580 openFile : String -> Mode -> IO File
581 closeFile : File -> IO ()
583 fread : File -> IO String
584 fwrite : File -> String -> IO ()
585 feof : File -> IO Bool
587 readFile : String -> IO String
594I/O programs will typically need to sequence actions, feeding the
595output of one computation into the input of the next. ``IO`` is an
596abstract type, however, so we can’t access the result of a computation
597directly. Instead, we sequence operations with ``do`` notation:
602 greet = do putStr "What is your name? "
604 putStrLn ("Hello " ++ name)
606The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
607type ``IO a``, and puts the result, of type ``a`` into the variable
608``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
609has type ``String``. Indentation is significant — each statement in
610the do block must begin in the same column. The ``return`` operation
611allows us to inject a value directly into an IO operation:
617As we will see later, ``do`` notation is more general than this, and
625Normally, arguments to functions are evaluated before the function
626itself (that is, Idris uses *eager* evaluation). However, this is
627not always the best approach. Consider the following function:
631 ifThenElse : Bool -> a -> a -> a;
632 ifThenElse True t e = t;
633 ifThenElse False t e = e;
635This function uses one of the ``t`` or ``e`` arguments, but not both
636(in fact, this is used to implement the ``if...then...else`` construct
637as we will see later. We would prefer if *only* the argument which was
638used was evaluated. To achieve this, Idris provides a ``Lazy``
639data type, which allows evaluation to be suspended:
643 data Lazy : Type -> Type where
644 Delay : (val : a) -> Lazy a
648A value of type ``Lazy a`` is unevaluated until it is forced by
649``Force``. The Idris type checker knows about the ``Lazy`` type,
650and inserts conversions where necessary between ``Lazy a`` and ``a``,
651and vice versa. We can therefore write ``ifThenElse`` as follows,
652without any explicit use of ``Force`` or ``Delay``:
656 ifThenElse : Bool -> Lazy a -> Lazy a -> a;
657 ifThenElse True t e = t;
658 ifThenElse False t e = e;
663Idris includes a number of useful data types and library functions
664(see the ``libs/`` directory in the distribution). This chapter
665describes a few of these. The functions described here are imported
666automatically by every Idris program, as part of ``Prelude.idr``.
671We have already seen the ``List`` and ``Vect`` data types:
675 data List a = Nil | (::) a (List a)
677 data Vect : Nat -> Type -> Type where
679 (::) : a -> Vect k a -> Vect (S k) a
681Note that the constructor names are the same for each — constructor
682names (in fact, names in general) can be overloaded, provided that
683they are declared in different namespaces (see Section
684:ref:`sect-namespaces`), and will typically be resolved according to
685their type. As syntactic sugar, any type with the constructor names
686``Nil`` and ``::`` can be written in list form. For example:
688- ``[]`` means ``Nil``
690- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
692The library also defines a number of functions for manipulating these
693types. ``map`` is overloaded both for ``List`` and ``Vect`` and
694applies a function to every element of the list or vector.
698 map : (a -> b) -> List a -> List b
700 map f (x :: xs) = f x :: map f xs
702 map : (a -> b) -> Vect n a -> Vect n b
704 map f (x :: xs) = f x :: map f xs
706For example, given the following vector of integers, and a function to
712 intVec = [1, 2, 3, 4, 5]
717the function ``map`` can be used as follows to double every element in
722 *usefultypes> show (map double intVec)
723 "[2, 4, 6, 8, 10]" : String
725You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
726directory. For more details of the functions available on ``List`` and
727``Vect``, look in the library files:
729- ``libs/prelude/Prelude/List.idr``
731- ``libs/base/Data/List.idr``
733- ``libs/base/Data/Vect.idr``
735- ``libs/base/Data/VectType.idr``
737Functions include filtering, appending, reversing, and so on. Also
738remember that Idris is still in development, so if you don’t see
739the function you need, please feel free to add it and submit a patch!
741Aside: Anonymous functions and operator sections
742~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
744There are actually neater ways to write the above expression. One way
745would be to use an anonymous function:
749 *usefultypes> show (map (\x => x * 2) intVec)
750 "[2, 4, 6, 8, 10]" : String
752The notation ``\x => val`` constructs an anonymous function which takes
753one argument, ``x`` and returns the expression ``val``. Anonymous
754functions may take several arguments, separated by commas,
755e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
756e.g. ``\x : Int => x * 2``, and can pattern match,
757e.g. ``\(x, y) => x + y``. We could also use an operator section:
761 *usefultypes> show (map (* 2) intVec)
762 "[2, 4, 6, 8, 10]" : String
764``(*2)`` is shorthand for a function which multiplies a number
765by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
771``Maybe`` describes an optional value. Either there is a value of the
772given type, or there isn’t:
776 data Maybe a = Just a | Nothing
778``Maybe`` is one way of giving a type to an operation that may
779fail. For example, looking something up in a ``List`` (rather than a
780vector) may result in an out of bounds error:
784 list_lookup : Nat -> List a -> Maybe a
785 list_lookup _ Nil = Nothing
786 list_lookup Z (x :: xs) = Just x
787 list_lookup (S k) (x :: xs) = list_lookup k xs
789The ``maybe`` function is used to process values of type ``Maybe``,
790either by applying a function to the value, if there is one, or by
791providing a default value:
795 maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
797Note that the types of the first two arguments are wrapped in
798``Lazy``. Since only one of the two arguments will actually be used,
799we mark them as ``Lazy`` in case they are large expressions where it
800would be wasteful to compute and then discard them.
805Values can be paired with the following built-in data type:
809 data Pair a b = MkPair a b
811As syntactic sugar, we can write ``(a, b)`` which, according to
812context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
813contain an arbitrary number of values, represented as nested pairs:
820 jim : (String, Int, String)
821 jim = ("Jim", 25, "Cambridge")
825 *usefultypes> fst jim
827 *usefultypes> snd jim
828 (25, "Cambridge") : (Int, String)
829 *usefultypes> jim == ("Jim", (25, "Cambridge"))
835Dependent pairs allow the type of the second element of a pair to depend
836on the value of the first element. Traditionally, these are referred to
841 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
842 MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P
844Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
845of a pair of A and P, where the name ``a`` can occur inside ``P``.
846``( a ** p )`` constructs a value of this type. For example, we can
847pair a number with a ``Vect`` of a particular length.
851 vec : (n : Nat ** Vect n Int)
854If you like, you can write it out the long way, the two are precisely
859 vec : Sigma Nat (\n => Vect n Int)
860 vec = MkSigma 2 [3, 4]
862The type checker could of course infer the value of the first element
863from the length of the vector. We can write an underscore ``_`` in
864place of values which we expect the type checker to fill in, so the
865above definition could also be written as:
869 vec : (n : Nat ** Vect n Int)
872We might also prefer to omit the type of the first element of the
873pair, since, again, it can be inferred:
877 vec : (n ** Vect n Int)
880One use for dependent pairs is to return values of dependent types
881where the index is not necessarily known in advance. For example, if
882we filter elements out of a ``Vect`` according to some predicate, we
883will not know in advance what the length of the resulting vector will
888 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
890If the ``Vect`` is empty, the result is easy:
894 filter p Nil = (_ ** [])
896In the ``::`` case, we need to inspect the result of a recursive call
897to ``filter`` to extract the length and the vector from the result. To
898do this, we use ``with`` notation, which allows pattern matching on
903 filter p (x :: xs) with (filter p xs)
904 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
906We will see more on ``with`` notation later.
912*Records* are data types which collect several values (the record's
913*fields*) together. Idris provides syntax for defining records and
914automatically generating field access and update functions. Unlike
915the syntax used for data structures, records in Idris follow a
916different syntax to that seen with Haskell. For example, we can
917represent a person's name and age in a record:
923 firstName, middleName, lastName : String
927 fred = MkPerson "Fred" "Joe" "Bloggs" 30
930The constructor name is provided using the ``constructor`` keyword,
931and the *fields* are then given which are in an indented block
932following the `where` keyword (here, ``firstName``, ``middleName``,
933``lastName``, and ``age``). You can declare multiple fields on a
934single line, provided that they have the same type. The field names
935can be used to access the field values:
939 *record> firstName fred
943 *record> :t firstName
944 firstName : Person -> String
946We can also use the field names to update a record (or, more
947precisely, produce a copy of the record with the given fields
952 *record> record { firstName = "Jim" } fred
953 MkPerson "Jim" "Joe" "Bloggs" 30 : Person
954 *record> record { firstName = "Jim", age = 20 } fred
955 MkPerson "Jim" "Joe" "Bloggs" 20 : Person
957The syntax ``record { field = val, ... }`` generates a function which
958updates the given fields in a record.
960Records, and fields within records, can have dependent types. Updates
961are allowed to change the type of a field, provided that the result is
967 constructor ClassInfo
968 students : Vect n Person
971It is safe to update the ``students`` field to a vector of a different
972length because it will not affect the type of the record:
976 addStudent : Person -> Class -> Class
977 addStudent p c = record { students = p :: students c } c
981 *record> addStudent fred (ClassInfo [] "CS")
982 ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
988Idris also provides a convenient syntax for accessing and updating
989nested records. For example, if a field is accessible with the
990expression ``c (b (a x))``, it can be updated using the following
995 record { a->b->c = val } x
997This returns a new record, with the field accessed by the path
998``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
999a->b->c = val }`` itself has a function type. Symmetrically, the field
1000can also be accessed with the following syntax:
1002.. code-block:: idris
1004 record { a->b->c } x
1010Records can also be dependent on values. Records *parameters*, which
1011are not subject to field updates. The parameters appear as arguments
1012to the resulting type, and are written following the record type
1013name. For example, a pair type could be defined as follows:
1015.. code-block:: idris
1017 record Prod a b where
1023Using the class record from the original introduction to records. The
1024size of the class can be restricted using a ``Vect`` and the size
1025promoted to the type level by parameterising the record with the size.
1029.. code-block:: idris
1031 record SizedClass (size : Nat) where
1032 constructor SizedClassInfo
1033 students : Vect size Person
1036**Note** that it is no longer possible to use the ``addStudent``
1037function from earlier, since that would change the size of the class. A
1038function to add a student must now specify in the type that the
1039size of the class has been increased by one. As the size is specified
1040using natural numbers, the new value can be incremented using the
1043.. code-block:: idris
1045 addStudent : Person -> SizedClass n -> SizedClass (S n)
1046 addStudent p c = record { students = p :: students c } c
1056Intermediate values can be calculated using ``let`` bindings:
1058.. code-block:: idris
1060 data Person = MkPerson String Int
1062 showPerson : Person -> String
1063 showPerson p = let MkPerson name age = p in
1064 name ++ " is " ++ show age ++ " years old"
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