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, incidently 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
111Functions are implemented by pattern matching, again using a similar
112syntax to Haskell. The main difference is that Idris requires type
113declarations for all functions, using a single colon ``:`` (rather
114than Haskell’s double colon ``::``). Some natural number arithmetic
115functions can be defined as follows, again taken from the standard
121 plus : Nat -> Nat -> Nat
123 plus (S k) y = S (plus k y)
125 -- Unary multiplication
126 mult : Nat -> Nat -> Nat
128 mult (S k) y = plus y (mult k y)
130The standard arithmetic operators ``+`` and ``*`` are also overloaded
131for use by ``Nat``, and are implemented using the above functions.
132Unlike Haskell, there is no restriction on whether types and function
133names must begin with a capital letter or not. Function names
134(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
135``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
136all part of the same namespace. We can test these functions at the
141 Idris> plus (S (S Z)) (S (S Z))
143 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
148 Idris automatically desugars the ``Nat`` representation into a
149 more human readable format. The result of ``plus (S (S Z)) (S (S Z))``
150 is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be
151 checked at the Idris prompt:
155 Idris> (S (S (S (S Z))))
158Like arithmetic operations, integer literals are also overloaded using
159type classes, meaning that we can also test the functions as follows:
165 Idris> mult 3 (plus 2 2)
168You may wonder, by the way, why we have unary natural numbers when our
169computers have perfectly good integer arithmetic built in. The reason
170is primarily that unary numbers have a very convenient structure which
171is easy to reason about, and easy to relate to other data structures
172as we will see later. Nevertheless, we do not want this convenience to
173be at the expense of efficiency. Fortunately, Idris knows about
174the relationship between ``Nat`` (and similarly structured types) and
175numbers. This means it can optimise the representation, and functions
176such as ``plus`` and ``mult``.
181Functions can also be defined *locally* using ``where`` clauses. For
182example, to define a function which reverses a list, we can use an
183auxiliary function which accumulates the new, reversed list, and which
184does not need to be visible globally:
188 reverse : List a -> List a
189 reverse xs = revAcc [] xs where
190 revAcc : List a -> List a -> List a
192 revAcc acc (x :: xs) = revAcc (x :: acc) xs
194Indentation is significant — functions in the ``where`` block must be
195indented further than the outer function.
199 Any names which are visible in the outer scope are also visible in
200 the ``where`` clause (unless they have been redefined, such as ``xs``
201 here). A name which appears only in the type will be in scope in the
202 ``where`` clause if it is a *parameter* to one of the types, i.e. it
203 is fixed across the entire structure.
205As well as functions, ``where`` blocks can include local data
206declarations, such as the following where ``MyLT`` is not accessible
207outside the definition of ``foo``:
219 isLT = if x < 20 then Yes else No
221In general, functions defined in a ``where`` clause need a type
222declaration just like any top level function. However, the type
223declaration for a function ``f`` *can* be omitted if:
225- ``f`` appears in the right hand side of the top level definition
227- The type of ``f`` can be completely determined from its first application
230So, for example, the following definitions are legal:
236 even (S k) = odd k where
241 test = [c (S 1), c Z, d (S Z)]
243 d y = c (y + 1 + z y)
252A standard example of a dependent type is the type of “lists with
253length”, conventionally called vectors in the dependent type
254literature. They are available as part of the Idris library, by
255importing ``Data.Vect``, or we can declare them as follows:
259 data Vect : Nat -> Type -> Type where
261 (::) : a -> Vect k a -> Vect (S k) a
263Note that we have used the same constructor names as for ``List``.
264Ad-hoc name overloading such as this is accepted by Idris,
265provided that the names are declared in different namespaces (in
266practice, normally in different modules). Ambiguous constructor names
267can normally be resolved from context.
269This declares a family of types, and so the form of the declaration is
270rather different from the simple type declarations above. We
271explicitly state the type of the type constructor ``Vect`` — it takes
272a ``Nat`` and a type as an argument, where ``Type`` stands for the
273type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
274*parameterised* by ``Type``. Each constructor targets a different part
275of the family of types. ``Nil`` can only be used to construct vectors
276with zero length, and ``::`` to construct vectors with non-zero
277length. In the type of ``::``, we state explicitly that an element of
278type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
279``k``) combine to make a vector of length ``S k``.
281We can define functions on dependent types such as ``Vect`` in the same
282way as on simple types such as ``List`` and ``Nat`` above, by pattern
283matching. The type of a function over ``Vect`` will describe what
284happens to the lengths of the vectors involved. For example, ``++``,
285defined as follows, appends two ``Vect``:
289 (++) : Vect n a -> Vect m a -> Vect (n + m) a
291 (++) (x :: xs) ys = x :: xs ++ ys
293The type of ``(++)`` states that the resulting vector’s length will be
294the sum of the input lengths. If we get the definition wrong in such a
295way that this does not hold, Idris will not accept the definition.
300 (++) : Vect n a -> Vect m a -> Vect (n + m) a
302 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
304When run through the Idris type checker, this results in the
309 $ idris vbroken.idr --check
310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
311 When elaborating an application of constructor Vect.:::
313 Vect (k + k) a (Type of xs ++ xs)
315 Vect (plus k m) a (Expected type)
324This error message suggests that there is a length mismatch between
325two vectors — we needed a vector of length ``k + m``, but provided a
326vector of length ``k + k``.
331Finite sets, as the name suggests, are sets with a finite number of
332elements. They are available as part of the Idris library, by
333importing ``Data.Fin``, or can be declared as follows:
337 data Fin : Nat -> Type where
339 FS : Fin k -> Fin (S k)
341From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
342So this is not a set in the sense of a collection that is a container of objects,
343rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
344Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
345``n`` is the argument used to instantiate the ``Fin`` type.
346For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
348Let us look at the constructors in greater detail.
350``FZ`` is the zeroth element of a finite set with ``S k`` elements;
351``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
352elements. ``Fin`` is indexed by a ``Nat``, which represents the number
353of elements in the set. Since we can’t construct an element of an
354empty set, neither constructor targets ``Fin Z``.
356As mentioned above, a useful application of the ``Fin`` family is to represent bounded
357natural numbers. Since the first ``n`` natural numbers form a finite
358set of ``n`` elements, we can treat ``Fin n`` as the set of integers
359greater than or equal to zero and less than ``n``.
361For example, the following function which looks up an element in a
362``Vect``, by a bounded index given as a ``Fin n``, is defined in the
367 index : Fin n -> Vect n a -> a
368 index FZ (x :: xs) = x
369 index (FS k) (x :: xs) = index k xs
371This function looks up a value at a given location in a vector. The
372location is bounded by the length of the vector (``n`` in each case),
373so there is no need for a run-time bounds check. The type checker
374guarantees that the location is no larger than the length of the
375vector, and of course no less than zero.
377Note also that there is no case for ``Nil`` here. This is because it
378is impossible. Since there is no element of ``Fin Z``, and the
379location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
380attempting to look up an element in an empty vector would give a
381compile time type error, since it would force ``n`` to be ``Z``.
386Let us take a closer look at the type of ``index``:
390 index : Fin n -> Vect n a -> a
392It takes two arguments, an element of the finite set of ``n`` elements,
393and a vector with ``n`` elements of type ``a``. But there are also two
394names, ``n`` and ``a``, which are not declared explicitly. These are
395*implicit* arguments to ``index``. We could also write the type of
400 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
402Implicit arguments, given in braces ``{}`` in the type declaration,
403are not given in applications of ``index``; their values can be
404inferred from the types of the ``Fin n`` and ``Vect n a``
405arguments. Any name with a which appears as a parameter or index in a
406type declaration, but which is otherwise free, will be automatically
407bound as an implicit argument. Implicit arguments can still be given
408explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
413 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
415In fact, any argument, implicit or explicit, may be given a name. We
416could have declared the type of ``index`` as:
420 index : (i:Fin n) -> (xs:Vect n a) -> a
422It is a matter of taste whether you want to do this — sometimes it can
423help document a function by making the purpose of an argument more
429Sometimes it is useful to provide types of implicit arguments,
430particularly where there is a dependency ordering, or where the
431implicit arguments themselves have dependencies. For example, we may
432wish to state the types of the implicit arguments in the following
433definition, which defines a predicate on vectors:
437 data Elem : a -> Vect n a -> Type where
438 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
439 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
441An instance of ``Elem x xs`` states that ``x`` is an element of
442``xs``. We can construct such a predicate if the required element is
443``Here``, at the head of the vector, or ``There``, in the tail of the
449 testVec = 3 :: 4 :: 5 :: 6 :: Nil
451 inVect : Elem 5 testVec
452 inVect = There (There Here)
454If the same implicit arguments are being used a lot, it can make a
455definition difficult to read. To avoid this problem, a ``using`` block
456gives the types and ordering of any implicit arguments which can
457appear within the block:
461 using (x:a, y:a, xs:Vect n a)
462 data Elem : a -> Vect n a -> Type where
463 Here : Elem x (x :: xs)
464 There : Elem x xs -> Elem x (y :: xs)
466Note: Declaration Order and ``mutual`` blocks
467---------------------------------------------
469In general, functions and data types must be defined before use, since
470dependent types allow functions to appear as part of types, and their
471reduction behaviour to affect type checking. However, this restriction
472can be relaxed by using a ``mutual`` block, which allows data types
473and functions to be defined simultaneously:
486In a ``mutual`` block, first all of the type declarations are added,
487then the function bodies. As a result, none of the function types can
488depend on the reduction behaviour of any of the functions in the
494Computer programs are of little use if they do not interact with the
495user or the system in some way. The difficulty in a pure language such
496as Idris — that is, a language where expressions do not have
497side-effects — is that I/O is inherently side-effecting. Therefore in
498Idris, such interactions are encapsulated in the type ``IO``:
502 data IO a -- IO operation returning a value of type a
504We’ll leave the definition of ``IO`` abstract, but effectively it
505describes what the I/O operations to be executed are, rather than how
506to execute them. The resulting operations are executed externally, by
507the run-time system. We’ve already seen one IO program:
512 main = putStrLn "Hello world"
514The type of ``putStrLn`` explains that it takes a string, and returns
515an element of the unit type ``()`` via an I/O action. There is a
516variant ``putStr`` which outputs a string without a newline:
520 putStrLn : String -> IO ()
521 putStr : String -> IO ()
523We can also read strings from user input:
529A number of other I/O operations are defined in the prelude, for
530example for reading and writing files, including:
534 data File -- abstract
535 data Mode = Read | Write | ReadWrite
537 openFile : String -> Mode -> IO File
538 closeFile : File -> IO ()
540 fread : File -> IO String
541 fwrite : File -> String -> IO ()
542 feof : File -> IO Bool
544 readFile : String -> IO String
551I/O programs will typically need to sequence actions, feeding the
552output of one computation into the input of the next. ``IO`` is an
553abstract type, however, so we can’t access the result of a computation
554directly. Instead, we sequence operations with ``do`` notation:
559 greet = do putStr "What is your name? "
561 putStrLn ("Hello " ++ name)
563The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
564type ``IO a``, and puts the result, of type ``a`` into the variable
565``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
566has type ``String``. Indentation is significant — each statement in
567the do block must begin in the same column. The ``return`` operation
568allows us to inject a value directly into an IO operation:
574As we will see later, ``do`` notation is more general than this, and
582Normally, arguments to functions are evaluated before the function
583itself (that is, Idris uses *eager* evaluation). However, this is
584not always the best approach. Consider the following function:
588 boolCase : Bool -> a -> a -> a;
589 boolCase True t e = t;
590 boolCase False t e = e;
592This function uses one of the ``t`` or ``e`` arguments, but not both
593(in fact, this is used to implement the ``if...then...else`` construct
594as we will see later. We would prefer if *only* the argument which was
595used was evaluated. To achieve this, Idris provides a ``Lazy``
596data type, which allows evaluation to be suspended:
600 data Lazy : Type -> Type where
601 Delay : (val : a) -> Lazy a
605A value of type ``Lazy a`` is unevaluated until it is forced by
606``Force``. The Idris type checker knows about the ``Lazy`` type,
607and inserts conversions where necessary between ``Lazy a`` and ``a``,
608and vice versa. We can therefore write ``boolCase`` as follows,
609without any explicit use of ``Force`` or ``Delay``:
613 boolCase : Bool -> Lazy a -> Lazy a -> a;
614 boolCase True t e = t;
615 boolCase False t e = e;
620Idris includes a number of useful data types and library functions
621(see the ``libs/`` directory in the distribution). This chapter
622describes a few of these. The functions described here are imported
623automatically by every Idris program, as part of ``Prelude.idr``.
628We have already seen the ``List`` and ``Vect`` data types:
632 data List a = Nil | (::) a (List a)
634 data Vect : Nat -> Type -> Type where
636 (::) : a -> Vect k a -> Vect (S k) a
638Note that the constructor names are the same for each — constructor
639names (in fact, names in general) can be overloaded, provided that
640they are declared in different namespaces (see Section
641:ref:`sect-namespaces`), and will typically be resolved according to
642their type. As syntactic sugar, any type with the constructor names
643``Nil`` and ``::`` can be written in list form. For example:
645- ``[]`` means ``Nil``
647- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
649The library also defines a number of functions for manipulating these
650types. ``map`` is overloaded both for ``List`` and ``Vect`` and
651applies a function to every element of the list or vector.
655 map : (a -> b) -> List a -> List b
657 map f (x :: xs) = f x :: map f xs
659 map : (a -> b) -> Vect n a -> Vect n b
661 map f (x :: xs) = f x :: map f xs
663For example, given the following vector of integers, and a function to
669 intVec = [1, 2, 3, 4, 5]
674the function ``map`` can be used as follows to double every element in
679 *usefultypes> show (map double intVec)
680 "[2, 4, 6, 8, 10]" : String
682You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
683directory. For more details of the functions available on ``List`` and
684``Vect``, look in the library files:
686- ``libs/prelude/Prelude/List.idr``
688- ``libs/base/Data/List.idr``
690- ``libs/base/Data/Vect.idr``
692- ``libs/base/Data/VectType.idr``
694Functions include filtering, appending, reversing, and so on. Also
695remember that Idris is still in development, so if you don’t see
696the function you need, please feel free to add it and submit a patch!
698Aside: Anonymous functions and operator sections
699------------------------------------------------
701There are actually neater ways to write the above expression. One way
702would be to use an anonymous function:
706 *usefultypes> show (map (\x => x * 2) intVec)
707 "[2, 4, 6, 8, 10]" : String
709The notation ``\x => val`` constructs an anonymous function which takes
710one argument, ``x`` and returns the expression ``val``. Anonymous
711functions may take several arguments, separated by commas,
712e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
713e.g. ``\x : Int => x * 2``, and can pattern match,
714e.g. ``\(x, y) => x + y``. We could also use an operator section:
718 *usefultypes> show (map (* 2) intVec)
719 "[2, 4, 6, 8, 10]" : String
721``(*2)`` is shorthand for a function which multiplies a number
722by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
728``Maybe`` describes an optional value. Either there is a value of the
729given type, or there isn’t:
733 data Maybe a = Just a | Nothing
735``Maybe`` is one way of giving a type to an operation that may
736fail. For example, looking something up in a ``List`` (rather than a
737vector) may result in an out of bounds error:
741 list_lookup : Nat -> List a -> Maybe a
742 list_lookup _ Nil = Nothing
743 list_lookup Z (x :: xs) = Just x
744 list_lookup (S k) (x :: xs) = list_lookup k xs
746The ``maybe`` function is used to process values of type ``Maybe``,
747either by applying a function to the value, if there is one, or by
748providing a default value:
752 maybe : Lazy b -> (a -> b) -> Maybe a -> b
754Note that the type of the first argument is ``Lazy b`` rather than
755simply ``b``. Since the default value might not be used, we mark it as
756``Lazy`` in case it is a large expression where evaluating it then
757discarding it would be wasteful.
759Tuples and Dependent Pairs
760--------------------------
762Values can be paired with the following built-in data type:
766 data Pair a b = MkPair a b
768As syntactic sugar, we can write ``(a, b)`` which, according to
769context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
770contain an arbitrary number of values, represented as nested pairs:
777 jim : (String, Int, String)
778 jim = ("Jim", 25, "Cambridge")
783Dependent pairs allow the type of the second element of a pair to depend
784on the value of the first element. Traditionally, these are referred to
789 data Sigma : (A : Type) -> (P : A -> Type) -> Type where
790 MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
792Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
793of a pair of A and P, where the name ``a`` can occur inside ``P``.
794``( a ** p )`` constructs a value of this type. For example, we can
795pair a number with a ``Vect`` of a particular length.
799 vec : (n : Nat ** Vect n Int)
802If you like, you can write it out the long way, the two are precisely
807 vec : Sigma Nat (\n => Vect n Int)
808 vec = MkSigma 2 [3, 4]
810The type checker could of course infer the value of the first element
811from the length of the vector. We can write an underscore ``_`` in
812place of values which we expect the type checker to fill in, so the
813above definition could also be written as:
817 vec : (n : Nat ** Vect n Int)
820We might also prefer to omit the type of the first element of the
821pair, since, again, it can be inferred:
825 vec : (n ** Vect n Int)
828One use for dependent pairs is to return values of dependent types
829where the index is not necessarily known in advance. For example, if
830we filter elements out of a ``Vect`` according to some predicate, we
831will not know in advance what the length of the resulting vector will
836 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
838If the ``Vect`` is empty, the result is easy:
842 filter p Nil = (_ ** [])
844In the ``::`` case, we need to inspect the result of a recursive call
845to ``filter`` to extract the length and the vector from the result. To
846do this, we use ``with`` notation, which allows pattern matching on
851 filter p (x :: xs) with (filter p xs)
852 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
854We will see more on ``with`` notation later.
864Intermediate values can be calculated using ``let`` bindings:
868 data Person = MkPerson String Int
870 showPerson : Person -> String
871 showPerson p = let MkPerson name age = p in
872 name ++ " is " ++ show age ++ " years old"
874 splitAt : Char -> String -> (String, String)
875 splitAt c x = case break (== c) x of
876 (x, y) => (x, strTail y)
878We can do simple pattern matching in ``let`` bindings too. For
879example, we can extract fields from a record as follows, as well as by
880pattern matching at the top level:
884 data Person = MkPerson String Int
886 showPerson : Person -> String
887 showPerson p = let MkPerson name age = p in
888 name ++ " is " ++ show age ++ " years old"
893Idris provides *comprehension* notation as a convenient shorthand
894for building lists. The general form is:
898 [ expression | qualifiers ]
900This generates the list of values produced by evaluating the
901``expression``, according to the conditions given by the comma
902separated ``qualifiers``. For example, we can build a list of
903Pythagorean triples as follows:
907 pythag : Int -> List (Int, Int, Int)
908 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
911The ``[a..b]`` notation is another shorthand which builds a list of
912numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
913list of numbers between ``a`` and ``c`` with the increment specified
914by the difference between ``a`` and ``b``. This works for any numeric
915type, using the ``count`` function from the prelude.
920Another way of inspecting intermediate values of *simple* types is to
921use a ``case`` expression. The following function, for example, splits
922a string into two at a given character:
926 splitAt : Char -> String -> (String, String)
927 splitAt c x = case break (== c) x of
928 (x, y) => (x, strTail y)
930``break`` is a library function which breaks a string into a pair of
931strings at the point where the given function returns true. We then
932deconstruct the pair it returns, and remove the first character of the
935A ``case`` expression can match several cases, for example, to inspect
936an intermediate value of type ``Maybe a``. Recall ``list_lookup``
937which looks up an index in a list, returning ``Nothing`` if the index
938is out of bounds. We can use this to write ``lookup_default``, which
939looks up an index and returns a default value if the index is out of
944 lookup_default : Nat -> List a -> a -> a
945 lookup_default i xs def = case list_lookup i xs of
949If the index is in bounds, we get the value at that index, otherwise
950we get a default value:
954 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
956 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
959**Restrictions:** The ``case`` construct is intended for simple
960analysis of intermediate expressions to avoid the need to write
961auxiliary functions, and is also used internally to implement pattern
962matching ``let`` and lambda bindings. It will *only* work if:
964- Each branch *matches* a value of the same type, and *returns* a
965 value of the same type.
967- The type of the result is "known". i.e. the type of the expression
968 can be determined *without* type checking the ``case``-expression
974*Records* are data types which collect several values (the record's
975*fields*) together. Idris provides syntax for defining records and
976*automatically generating field access and update functions*. For
977example, we can represent a person's name and age in a record:
981 record Person : Type where
982 MkPerson : (name : String) ->
983 (age : Int) -> Person
986 fred = MkPerson "Fred" 30
988Record declarations are like ``data`` declarations, except that they
989are introduced by the ``record`` keyword, and can only have one
990constructor. The names of the binders in the constructor type
991(``name`` and ``age``) here are the field names, which we can use to
992access the field values:
1001 name : Person -> String
1003We can also use the field names to update a record (or, more
1004precisely, produce a new record with the given fields updated).
1008 *record> record { name = "Jim" } fred
1009 MkPerson "Jim" 30 : Person
1010 *record> record { name = "Jim", age = 20 } fred
1011 MkPerson "Jim" 20 : Person
1013The syntax ``record { field = val, ... }`` generates a function which
1014updates the given fields in a record.
1016Records, and fields within records, can have dependent types. Updates
1017are allowed to change the type of a field, provided that the result is
1018well-typed, and the result does not affect the type of the record as a
1021.. code-block:: idris
1023 record Class : Type where
1024 ClassInfo : (students : Vect n Person) ->
1025 (className : String) ->
1028It is safe to update the ``students`` field to a vector of a different
1029length because it will not affect the type of the record:
1031.. code-block:: idris
1033 addStudent : Person -> Class -> Class
1034 addStudent p c = record { students = p :: students c } c
1038 *record> addStudent fred (ClassInfo [] "CS")
1039 ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1045Idris also provides a convenient syntax for accessing and updating
1046nested records. For example, if a field is accessible with the
1047expression ``c (b (a x))``, it can be updated using the following
1050.. code-block:: idris
1052 record { a->b->c = val } x
1054This returns a new record, with the field accessed by the path
1055``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
1056a->b->c = val }`` itself has a function type. Symmetrically, the field
1057can also be accessed with the following syntax:
1059.. code-block:: idris
1061 record { a->b->c } x
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