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 (none here,
37however Idris programs can consist of several modules, and the
38definitions in each module each have their own namespace, as we will
39discuss in Section :ref:`sect-namespaces`) and a collection of
40declarations and definitions. The order of definitions is significant
41— functions and data types must be defined before use. Each definition
42must have a type declaration, for example see ``x : Int``, ``foo :
43String``, from the above listing. Indentation is significant — a new
44declaration begins at the same level of indentation as the preceding
45declaration. Alternatively, declarations may be terminated with a
48A library module ``prelude`` is automatically imported by every
49Idris program, including facilities for IO, arithmetic, data
50structures and various common functions. The prelude defines several
51arithmetic and comparison operators, which we can use at the prompt.
52Evaluating things at the prompt gives an answer, and the type of the
62All of the usual arithmetic and comparison operators are defined for
63the primitive types. They are overloaded using type classes, as we
64will discuss in Section :ref:`sect-classes` and can be extended to
65work on user defined types. Boolean expressions can be tested with the
66``if...then...else`` construct:
70 *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
71 "The answer!" : String
76Data types are declared in a similar way to Haskell data types, with a
77similar syntax. Natural numbers and lists, for example, can be
82 data Nat = Z | S Nat -- Natural numbers
83 -- (zero and successor)
84 data List a = Nil | (::) a (List a) -- Polymorphic lists
86The above declarations are taken from the standard library. Unary
87natural numbers can be either zero (``Z``), or the successor of
88another natural number (``S k``). Lists can either be empty (``Nil``)
89or a value added to the front of another list (``x :: xs``). In the
90declaration for ``List``, we used an infix operator ``::``. New
91operators such as this can be added using a fixity declaration, as
98Functions, data constructors and type constructors may all be given
99infix operators as names. They may be used in prefix form if enclosed
100in brackets, e.g. ``(::)``. Infix operators can use any of the
110Functions are implemented by pattern matching, again using a similar
111syntax to Haskell. The main difference is that Idris requires type
112declarations for all functions, using a single colon ``:`` (rather
113than Haskell’s double colon ``::``). Some natural number arithmetic
114functions can be defined as follows, again taken from the standard
120 plus : Nat -> Nat -> Nat
122 plus (S k) y = S (plus k y)
124 -- Unary multiplication
125 mult : Nat -> Nat -> Nat
127 mult (S k) y = plus y (mult k y)
129The standard arithmetic operators ``+`` and ``*`` are also overloaded
130for use by ``Nat``, and are implemented using the above functions.
131Unlike Haskell, there is no restriction on whether types and function
132names must begin with a capital letter or not. Function names
133(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
134``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
135all part of the same namespace. We can test these functions at the
140 Idris> plus (S (S Z)) (S (S Z))
142 Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
147 Idris automatically desugars the ``Nat`` representation into a
148 more human readable format. The result of ``plus (S (S Z)) (S (S Z))``
149 is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be
150 checked at the Idris prompt:
154 Idris> (S (S (S (S Z))))
157Like arithmetic operations, integer literals are also overloaded using
158type classes, meaning that we can also test the functions as follows:
164 Idris> mult 3 (plus 2 2)
167You may wonder, by the way, why we have unary natural numbers when our
168computers have perfectly good integer arithmetic built in. The reason
169is primarily that unary numbers have a very convenient structure which
170is easy to reason about, and easy to relate to other data structures
171as we will see later. Nevertheless, we do not want this convenience to
172be at the expense of efficiency. Fortunately, Idris knows about
173the relationship between ``Nat`` (and similarly structured types) and
174numbers. This means it can optimise the representation, and functions
175such as ``plus`` and ``mult``.
180Functions can also be defined *locally* using ``where`` clauses. For
181example, to define a function which reverses a list, we can use an
182auxiliary function which accumulates the new, reversed list, and which
183does not need to be visible globally:
187 reverse : List a -> List a
188 reverse xs = revAcc [] xs where
189 revAcc : List a -> List a -> List a
191 revAcc acc (x :: xs) = revAcc (x :: acc) xs
193Indentation is significant — functions in the ``where`` block must be
194indented further than the outer function.
196**Scope:** Any names which are visible in the outer scope are also
197visible in the ``where`` clause (unless they have been redefined, such
198as ``xs`` here). A name which appears only in the type will be in scope
199in the ``where`` clause if it is a *parameter* to one of the types,
200i.e. it is fixed across the entire structure.
202As well as functions, ``where`` blocks can include local data
203declarations, such as the following where ``MyLT`` is not accessible
204outside the definition of ``foo``:
216 isLT = if x < 20 then Yes else No
218In general, functions defined in a ``where`` clause need a type
219declaration just like any top level function. However, the type
220declaration for a function ``f`` *can* be omitted if:
222- ``f`` appears in the right hand side of the top level definition
224- The type of ``f`` can be completely determined from its first application
227So, for example, the following definitions are legal:
233 even (S k) = odd k where
238 test = [c (S 1), c Z, d (S Z)]
240 d y = c (y + 1 + z y)
249A standard example of a dependent type is the type of “lists with
250length”, conventionally called vectors in the dependent type
251literature. They are available as part of the Idris library, by
252importing ``Data.Vect``, or we can declare them as follows:
256 data Vect : Nat -> Type -> Type where
258 (::) : a -> Vect k a -> Vect (S k) a
260Note that we have used the same constructor names as for ``List``.
261Ad-hoc name overloading such as this is accepted by Idris,
262provided that the names are declared in different namespaces (in
263practice, normally in different modules). Ambiguous constructor names
264can normally be resolved from context.
266This declares a family of types, and so the form of the declaration is
267rather different from the simple type declarations above. We
268explicitly state the type of the type constructor ``Vect`` — it takes
269a ``Nat`` and a type as an argument, where ``Type`` stands for the
270type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
271*parameterised* by ``Type``. Each constructor targets a different part
272of the family of types. ``Nil`` can only be used to construct vectors
273with zero length, and ``::`` to construct vectors with non-zero
274length. In the type of ``::``, we state explicitly that an element of
275type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
276``k``) combine to make a vector of length ``S k``.
278We can define functions on dependent types such as ``Vect`` in the same
279way as on simple types such as ``List`` and ``Nat`` above, by pattern
280matching. The type of a function over ``Vect`` will describe what
281happens to the lengths of the vectors involved. For example, ``++``,
282defined as follows, appends two ``Vect``:
286 (++) : Vect n a -> Vect m a -> Vect (n + m) a
288 (++) (x :: xs) ys = x :: xs ++ ys
290The type of ``(++)`` states that the resulting vector’s length will be
291the sum of the input lengths. If we get the definition wrong in such a
292way that this does not hold, Idris will not accept the definition.
297 (++) : Vect n a -> Vect m a -> Vect (n + m) a
299 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
301When run through the Idris type checker, this results in the
306 $ idris vbroken.idr --check
307 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
308 When elaborating an application of constructor Vect.:::
320This error message suggests that there is a length mismatch between
321two vectors — we needed a vector of length ``k + m``, but provided a
322vector of length ``k + k``.
327Finite sets, as the name suggests, are sets with a finite number of
328elements. They are available as part of the Idris library, by
329importing ``Data.Fin``, or can be declared as follows:
333 data Fin : Nat -> Type where
335 FS : Fin k -> Fin (S k)
337From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
338So this is not a set in the sense of a collection that is a container of objects,
339rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
340Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
341``n`` is the argument used to instantiate the ``Fin`` type.
342For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
344Let us look at the constructors in greater detail.
346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
348elements. ``Fin`` is indexed by a ``Nat``, which represents the number
349of elements in the set. Since we can’t construct an element of an
350empty set, neither constructor targets ``Fin Z``.
352As mentioned above, a useful application of the ``Fin`` family is to represent bounded
353natural numbers. Since the first ``n`` natural numbers form a finite
354set of ``n`` elements, we can treat ``Fin n`` as the set of integers
355greater than or equal to zero and less than ``n``.
357For example, the following function which looks up an element in a
358``Vect``, by a bounded index given as a ``Fin n``, is defined in the
363 index : Fin n -> Vect n a -> a
364 index FZ (x :: xs) = x
365 index (FS k) (x :: xs) = index k xs
367This function looks up a value at a given location in a vector. The
368location is bounded by the length of the vector (``n`` in each case),
369so there is no need for a run-time bounds check. The type checker
370guarantees that the location is no larger than the length of the
371vector, and of course no less than zero.
373Note also that there is no case for ``Nil`` here. This is because it
374is impossible. Since there is no element of ``Fin Z``, and the
375location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
376attempting to look up an element in an empty vector would give a
377compile time type error, since it would force ``n`` to be ``Z``.
382Let us take a closer look at the type of ``index``:
386 index : Fin n -> Vect n a -> a
388It takes two arguments, an element of the finite set of ``n`` elements,
389and a vector with ``n`` elements of type ``a``. But there are also two
390names, ``n`` and ``a``, which are not declared explicitly. These are
391*implicit* arguments to ``index``. We could also write the type of
396 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
398Implicit arguments, given in braces ``{}`` in the type declaration,
399are not given in applications of ``index``; their values can be
400inferred from the types of the ``Fin n`` and ``Vect n a``
401arguments. Any name with a which appears as a parameter or index in a
402type declaration, but which is otherwise free, will be automatically
403bound as an implicit argument. Implicit arguments can still be given
404explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
409 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
411In fact, any argument, implicit or explicit, may be given a name. We
412could have declared the type of ``index`` as:
416 index : (i:Fin n) -> (xs:Vect n a) -> a
418It is a matter of taste whether you want to do this — sometimes it can
419help document a function by making the purpose of an argument more
425Sometimes it is useful to provide types of implicit arguments,
426particularly where there is a dependency ordering, or where the
427implicit arguments themselves have dependencies. For example, we may
428wish to state the types of the implicit arguments in the following
429definition, which defines a predicate on vectors:
433 data Elem : a -> Vect n a -> Type where
434 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
435 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
437An instance of ``Elem x xs`` states that ``x`` is an element of
438``xs``. We can construct such a predicate if the required element is
439``Here``, at the head of the vector, or ``There``, in the tail of the
445 testVec = 3 :: 4 :: 5 :: 6 :: Nil
447 inVect : Elem 5 testVec
448 inVect = There (There Here)
450If the same implicit arguments are being used a lot, it can make a
451definition difficult to read. To avoid this problem, a ``using`` block
452gives the types and ordering of any implicit arguments which can
453appear within the block:
457 using (x:a, y:a, xs:Vect n a)
458 data Elem : a -> Vect n a -> Type where
459 Here : Elem x (x :: xs)
460 There : Elem x xs -> Elem x (y :: xs)
462Note: Declaration Order and ``mutual`` blocks
463---------------------------------------------
465In general, functions and data types must be defined before use, since
466dependent types allow functions to appear as part of types, and their
467reduction behaviour to affect type checking. However, this restriction
468can be relaxed by using a ``mutual`` block, which allows data types
469and functions to be defined simultaneously:
482In a ``mutual`` block, first all of the type declarations are added,
483then the function bodies. As a result, none of the function types can
484depend on the reduction behaviour of any of the functions in the
490Computer programs are of little use if they do not interact with the
491user or the system in some way. The difficulty in a pure language such
492as Idris — that is, a language where expressions do not have
493side-effects — is that I/O is inherently side-effecting. Therefore in
494Idris, such interactions are encapsulated in the type ``IO``:
498 data IO a -- IO operation returning a value of type a
500We’ll leave the definition of ``IO`` abstract, but effectively it
501describes what the I/O operations to be executed are, rather than how
502to execute them. The resulting operations are executed externally, by
503the run-time system. We’ve already seen one IO program:
508 main = putStrLn "Hello world"
510The type of ``putStrLn`` explains that it takes a string, and returns
511an element of the unit type ``()`` via an I/O action. There is a
512variant ``putStr`` which outputs a string without a newline:
516 putStrLn : String -> IO ()
517 putStr : String -> IO ()
519We can also read strings from user input:
525A number of other I/O operations are defined in the prelude, for
526example for reading and writing files, including:
530 data File -- abstract
531 data Mode = Read | Write | ReadWrite
533 openFile : String -> Mode -> IO File
534 closeFile : File -> IO ()
536 fread : File -> IO String
537 fwrite : File -> String -> IO ()
538 feof : File -> IO Bool
540 readFile : String -> IO String
547I/O programs will typically need to sequence actions, feeding the
548output of one computation into the input of the next. ``IO`` is an
549abstract type, however, so we can’t access the result of a computation
550directly. Instead, we sequence operations with ``do`` notation:
555 greet = do putStr "What is your name? "
557 putStrLn ("Hello " ++ name)
559The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
560type ``IO a``, and puts the result, of type ``a`` into the variable
561``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
562has type ``String``. Indentation is significant — each statement in
563the do block must begin in the same column. The ``return`` operation
564allows us to inject a value directly into an IO operation:
570As we will see later, ``do`` notation is more general than this, and
578Normally, arguments to functions are evaluated before the function
579itself (that is, Idris uses *eager* evaluation). However, this is
580not always the best approach. Consider the following function:
584 boolCase : Bool -> a -> a -> a;
585 boolCase True t e = t;
586 boolCase False t e = e;
588This function uses one of the ``t`` or ``e`` arguments, but not both
589(in fact, this is used to implement the ``if...then...else`` construct
590as we will see later. We would prefer if *only* the argument which was
591used was evaluated. To achieve this, Idris provides a ``Lazy``
592data type, which allows evaluation to be suspended:
596 data Lazy : Type -> Type where
597 Delay : (val : a) -> Lazy a
601A value of type ``Lazy a`` is unevaluated until it is forced by
602``Force``. The Idris type checker knows about the ``Lazy`` type,
603and inserts conversions where necessary between ``Lazy a`` and ``a``,
604and vice versa. We can therefore write ``boolCase`` as follows,
605without any explicit use of ``Force`` or ``Delay``:
609 boolCase : Bool -> Lazy a -> Lazy a -> a;
610 boolCase True t e = t;
611 boolCase False t e = e;
616Idris includes a number of useful data types and library functions
617(see the ``libs/`` directory in the distribution). This chapter
618describes a few of these. The functions described here are imported
619automatically by every Idris program, as part of ``Prelude.idr``.
624We have already seen the ``List`` and ``Vect`` data types:
628 data List a = Nil | (::) a (List a)
630 data Vect : Nat -> Type -> Type where
632 (::) : a -> Vect k a -> Vect (S k) a
634Note that the constructor names are the same for each — constructor
635names (in fact, names in general) can be overloaded, provided that
636they are declared in different namespaces (see Section
637:ref:`sect-namespaces`), and will typically be resolved according to
638their type. As syntactic sugar, any type with the constructor names
639``Nil`` and ``::`` can be written in list form. For example:
641- ``[]`` means ``Nil``
643- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
645The library also defines a number of functions for manipulating these
646types. ``map`` is overloaded both for ``List`` and ``Vect`` and
647applies a function to every element of the list or vector.
651 map : (a -> b) -> List a -> List b
653 map f (x :: xs) = f x :: map f xs
655 map : (a -> b) -> Vect n a -> Vect n b
657 map f (x :: xs) = f x :: map f xs
659For example, given the following vector of integers, and a function to
665 intVec = [1, 2, 3, 4, 5]
670the function ``map`` can be used as follows to double every element in
675 *usefultypes> show (map double intVec)
676 "[2, 4, 6, 8, 10]" : String
678You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
679directory. For more details of the functions available on ``List`` and
680``Vect``, look in the library files:
682- ``libs/prelude/Prelude/List.idr``
684- ``libs/base/Data/List.idr``
686- ``libs/base/Data/Vect.idr``
688- ``libs/base/Data/VectType.idr``
690Functions include filtering, appending, reversing, and so on. Also
691remember that Idris is still in development, so if you don’t see
692the function you need, please feel free to add it and submit a patch!
694Aside: Anonymous functions and operator sections
695------------------------------------------------
697There are actually neater ways to write the above expression. One way
698would be to use an anonymous function:
702 *usefultypes> show (map (\x => x * 2) intVec)
703 "[2, 4, 6, 8, 10]" : String
705The notation ``\x => val`` constructs an anonymous function which takes
706one argument, ``x`` and returns the expression ``val``. Anonymous
707functions may take several arguments, separated by commas,
708e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
709e.g. ``\x : Int => x * 2``, and can pattern match,
710e.g. ``\(x, y) => x + y``. We could also use an operator section:
714 *usefultypes> show (map (* 2) intVec)
715 "[2, 4, 6, 8, 10]" : String
717``(*2)`` is shorthand for a function which multiplies a number
718by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
724``Maybe`` describes an optional value. Either there is a value of the
725given type, or there isn’t:
729 data Maybe a = Just a | Nothing
731``Maybe`` is one way of giving a type to an operation that may
732fail. For example, looking something up in a ``List`` (rather than a
733vector) may result in an out of bounds error:
737 list_lookup : Nat -> List a -> Maybe a
738 list_lookup _ Nil = Nothing
739 list_lookup Z (x :: xs) = Just x
740 list_lookup (S k) (x :: xs) = list_lookup k xs
742The ``maybe`` function is used to process values of type ``Maybe``,
743either by applying a function to the value, if there is one, or by
744providing a default value:
748 maybe : Lazy b -> (a -> b) -> Maybe a -> b
750Note that the type of the first argument is ``Lazy b`` rather than
751simply ``b``. Since the default value might not be used, we mark it as
752``Lazy`` in case it is a large expression where evaluating it then
753discarding it would be wasteful.
755Tuples and Dependent Pairs
756--------------------------
758Values can be paired with the following built-in data type:
762 data Pair a b = MkPair a b
764As syntactic sugar, we can write ``(a, b)`` which, according to
765context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
766contain an arbitrary number of values, represented as nested pairs:
773 jim : (String, Int, String)
774 jim = ("Jim", 25, "Cambridge")
779Dependent pairs allow the type of the second element of a pair to depend
780on the value of the first element. Traditionally, these are referred to
785 data Sigma : (A : Type) -> (P : A -> Type) -> Type where
786 MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
788Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
789of a pair of A and P, where the name ``a`` can occur inside ``P``.
790``( a ** p )`` constructs a value of this type. For example, we can
791pair a number with a ``Vect`` of a particular length.
795 vec : (n : Nat ** Vect n Int)
798If you like, you can write it out the long way, the two are precisely
803 vec : Sigma Nat (\n => Vect n Int)
804 vec = MkSigma 2 [3, 4]
806The type checker could of course infer the value of the first element
807from the length of the vector. We can write an underscore ``_`` in
808place of values which we expect the type checker to fill in, so the
809above definition could also be written as:
813 vec : (n : Nat ** Vect n Int)
816We might also prefer to omit the type of the first element of the
817pair, since, again, it can be inferred:
821 vec : (n ** Vect n Int)
824One use for dependent pairs is to return values of dependent types
825where the index is not necessarily known in advance. For example, if
826we filter elements out of a ``Vect`` according to some predicate, we
827will not know in advance what the length of the resulting vector will
832 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
834If the ``Vect`` is empty, the result is easy:
838 filter p Nil = (_ ** [])
840In the ``::`` case, we need to inspect the result of a recursive call
841to ``filter`` to extract the length and the vector from the result. To
842do this, we use ``with`` notation, which allows pattern matching on
847 filter p (x :: xs) with (filter p xs)
848 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
850We will see more on ``with`` notation later.
860Intermediate values can be calculated using ``let`` bindings:
864 data Person = MkPerson String Int
866 showPerson : Person -> String
867 showPerson p = let MkPerson name age = p in
868 name ++ " is " ++ show age ++ " years old"
870 splitAt : Char -> String -> (String, String)
871 splitAt c x = case break (== c) x of
872 (x, y) => (x, strTail y)
874We can do simple pattern matching in ``let`` bindings too. For
875example, we can extract fields from a record as follows, as well as by
876pattern matching at the top level:
880 data Person = MkPerson String Int
882 showPerson : Person -> String
883 showPerson p = let MkPerson name age = p in
884 name ++ " is " ++ show age ++ " years old"
889Idris provides *comprehension* notation as a convenient shorthand
890for building lists. The general form is:
894 [ expression | qualifiers ]
896This generates the list of values produced by evaluating the
897``expression``, according to the conditions given by the comma
898separated ``qualifiers``. For example, we can build a list of
899Pythagorean triples as follows:
903 pythag : Int -> List (Int, Int, Int)
904 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
907The ``[a..b]`` notation is another shorthand which builds a list of
908numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
909list of numbers between ``a`` and ``c`` with the increment specified
910by the difference between ``a`` and ``b``. This works for any numeric
911type, using the ``count`` function from the prelude.
916Another way of inspecting intermediate values of *simple* types is to
917use a ``case`` expression. The following function, for example, splits
918a string into two at a given character:
922 splitAt : Char -> String -> (String, String)
923 splitAt c x = case break (== c) x of
924 (x, y) => (x, strTail y)
926``break`` is a library function which breaks a string into a pair of
927strings at the point where the given function returns true. We then
928deconstruct the pair it returns, and remove the first character of the
931A ``case`` expression can match several cases, for example, to inspect
932an intermediate value of type ``Maybe a``. Recall ``list_lookup``
933which looks up an index in a list, returning ``Nothing`` if the index
934is out of bounds. We can use this to write ``lookup_default``, which
935looks up an index and returns a default value if the index is out of
940 lookup_default : Nat -> List a -> a -> a
941 lookup_default i xs def = case list_lookup i xs of
945If the index is in bounds, we get the value at that index, otherwise
946we get a default value:
950 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
952 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
955**Restrictions:** The ``case`` construct is intended for simple
956analysis of intermediate expressions to avoid the need to write
957auxiliary functions, and is also used internally to implement pattern
958matching ``let`` and lambda bindings. It will *only* work if:
960- Each branch *matches* a value of the same type, and *returns* a
961 value of the same type.
963- The type of the result is "known". i.e. the type of the expression
964 can be determined *without* type checking the ``case``-expression
970*Records* are data types which collect several values (the record's
971*fields*) together. Idris provides syntax for defining records and
972*automatically generating field access and update functions. For
973*example, we can represent a person's name and age in a record:
977 record Person : Type where
978 MkPerson : (name : String) ->
979 (age : Int) -> Person
982 fred = MkPerson "Fred" 30
984Record declarations are like ``data`` declarations, except that they
985are introduced by the ``record`` keyword, and can only have one
986constructor. The names of the binders in the constructor type
987(``name`` and ``age``) here are the field names, which we can use to
988access the field values:
997 name : Person -> String
999We can also use the field names to update a record (or, more
1000precisely, produce a new record with the given fields updated).
1004 *record> record { name = "Jim" } fred
1005 MkPerson "Jim" 30 : Person
1006 *record> record { name = "Jim", age = 20 } fred
1007 MkPerson "Jim" 20 : Person
1009The syntax ``record { field = val, ... }`` generates a function which
1010updates the given fields in a record.
1012Records, and fields within records, can have dependent types. Updates
1013are allowed to change the type of a field, provided that the result is
1014well-typed, and the result does not affect the type of the record as a
1017.. code-block:: idris
1019 record Class : Type where
1020 ClassInfo : (students : Vect n Person) ->
1021 (className : String) ->
1024It is safe to update the ``students`` field to a vector of a different
1025length because it will not affect the type of the record:
1027.. code-block:: idris
1029 addStudent : Person -> Class -> Class
1030 addStudent p c = record { students = p :: students c } c
1034 *record> addStudent fred (ClassInfo [] "CS")
1035 ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1041Idris also provides a convenient syntax for accessing and updating
1042nested records. For example, if a field is accessible with the
1043expression ``c (b (a x))``, it can be updated using the following
1046.. code-block:: idris
1048 record { a->b->c = val } x
1050This returns a new record, with the field accessed by the path
1051``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
1052a->b->c = val }`` itself has a function type. Symmetrically, the field
1053can also be accessed with the following syntax:
1055.. code-block:: idris
1057 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