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
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)
337``FZ`` is the zeroth element of a finite set with ``S k`` elements;
338``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
339elements. ``Fin`` is indexed by a ``Nat``, which represents the number
340of elements in the set. Obviously we can’t construct an element of an
341empty set, so neither constructor targets ``Fin Z``.
343A useful application of the ``Fin`` family is to represent bounded
344natural numbers. Since the first ``n`` natural numbers form a finite
345set of ``n`` elements, we can treat ``Fin n`` as the set of natural
346numbers bounded by ``n``.
348For example, the following function which looks up an element in a
349``Vect``, by a bounded index given as a ``Fin n``, is defined in the
354 index : Fin n -> Vect n a -> a
355 index FZ (x :: xs) = x
356 index (FS k) (x :: xs) = index k xs
358This function looks up a value at a given location in a vector. The
359location is bounded by the length of the vector (``n`` in each case),
360so there is no need for a run-time bounds check. The type checker
361guarantees that the location is no larger than the length of the
364Note also that there is no case for ``Nil`` here. This is because it
365is impossible. Since there is no element of ``Fin Z``, and the
366location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
367attempting to look up an element in an empty vector would give a
368compile time type error, since it would force ``n`` to be ``Z``.
373Let us take a closer look at the type of ``index``:
377 index : Fin n -> Vect n a -> a
379It takes two arguments, an element of the finite set of ``n`` elements,
380and a vector with ``n`` elements of type ``a``. But there are also two
381names, ``n`` and ``a``, which are not declared explicitly. These are
382*implicit* arguments to ``index``. We could also write the type of
387 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
389Implicit arguments, given in braces ``{}`` in the type declaration,
390are not given in applications of ``index``; their values can be
391inferred from the types of the ``Fin n`` and ``Vect n a``
392arguments. Any name with a which appears as a parameter or index in a
393type declaration, but which is otherwise free, will be automatically
394bound as an implicit argument. Implicit arguments can still be given
395explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
400 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
402In fact, any argument, implicit or explicit, may be given a name. We
403could have declared the type of ``index`` as:
407 index : (i:Fin n) -> (xs:Vect n a) -> a
409It is a matter of taste whether you want to do this — sometimes it can
410help document a function by making the purpose of an argument more
416Sometimes it is useful to provide types of implicit arguments,
417particularly where there is a dependency ordering, or where the
418implicit arguments themselves have dependencies. For example, we may
419wish to state the types of the implicit arguments in the following
420definition, which defines a predicate on vectors:
424 data Elem : a -> Vect n a -> Type where
425 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
426 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
428An instance of ``Elem x xs`` states that ``x`` is an element of
429``xs``. We can construct such a predicate if the required element is
430``Here``, at the head of the vector, or ``There``, in the tail of the
436 testVec = 3 :: 4 :: 5 :: 6 :: Nil
438 inVect : Elem 5 testVec
439 inVect = There (There Here)
441If the same implicit arguments are being used a lot, it can make a
442definition difficult to read. To avoid this problem, a ``using`` block
443gives the types and ordering of any implicit arguments which can
444appear within the block:
448 using (x:a, y:a, xs:Vect n a)
449 data Elem : a -> Vect n a -> Type where
450 Here : Elem x (x :: xs)
451 There : Elem x xs -> Elem x (y :: xs)
453Note: Declaration Order and ``mutual`` blocks
454~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456In general, functions and data types must be defined before use, since
457dependent types allow functions to appear as part of types, and their
458reduction behaviour to affect type checking. However, this restriction
459can be relaxed by using a ``mutual`` block, which allows data types
460and functions to be defined simultaneously:
473In a ``mutual`` block, first all of the type declarations are added,
474then the function bodies. As a result, none of the function types can
475depend on the reduction behaviour of any of the functions in the
481Computer programs are of little use if they do not interact with the
482user or the system in some way. The difficulty in a pure language such
483as Idris — that is, a language where expressions do not have
484side-effects — is that I/O is inherently side-effecting. Therefore in
485Idris, such interactions are encapsulated in the type ``IO``:
489 data IO a -- IO operation returning a value of type a
491We’ll leave the definition of ``IO`` abstract, but effectively it
492describes what the I/O operations to be executed are, rather than how
493to execute them. The resulting operations are executed externally, by
494the run-time system. We’ve already seen one IO program:
499 main = putStrLn "Hello world"
501The type of ``putStrLn`` explains that it takes a string, and returns
502an element of the unit type ``()`` via an I/O action. There is a
503variant ``putStr`` which outputs a string without a newline:
507 putStrLn : String -> IO ()
508 putStr : String -> IO ()
510We can also read strings from user input:
516A number of other I/O operations are defined in the prelude, for
517example for reading and writing files, including:
521 data File -- abstract
522 data Mode = Read | Write | ReadWrite
524 openFile : String -> Mode -> IO File
525 closeFile : File -> IO ()
527 fread : File -> IO String
528 fwrite : File -> String -> IO ()
529 feof : File -> IO Bool
531 readFile : String -> IO String
538I/O programs will typically need to sequence actions, feeding the
539output of one computation into the input of the next. ``IO`` is an
540abstract type, however, so we can’t access the result of a computation
541directly. Instead, we sequence operations with ``do`` notation:
546 greet = do putStr "What is your name? "
548 putStrLn ("Hello " ++ name)
550The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
551type ``IO a``, and puts the result, of type ``a`` into the variable
552``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
553has type ``String``. Indentation is significant — each statement in
554the do block must begin in the same column. The ``return`` operation
555allows us to inject a value directly into an IO operation:
561As we will see later, ``do`` notation is more general than this, and
569Normally, arguments to functions are evaluated before the function
570itself (that is, Idris uses *eager* evaluation). However, this is
571not always the best approach. Consider the following function:
575 boolCase : Bool -> a -> a -> a;
576 boolCase True t e = t;
577 boolCase False t e = e;
579This function uses one of the ``t`` or ``e`` arguments, but not both
580(in fact, this is used to implement the ``if...then...else`` construct
581as we will see later. We would prefer if *only* the argument which was
582used was evaluated. To achieve this, Idris provides a ``Lazy``
583data type, which allows evaluation to be suspended:
587 data Lazy : Type -> Type where
588 Delay : (val : a) -> Lazy a
592A value of type ``Lazy a`` is unevaluated until it is forced by
593``Force``. The Idris type checker knows about the ``Lazy`` type,
594and inserts conversions where necessary between ``Lazy a`` and ``a``,
595and vice versa. We can therefore write ``boolCase`` as follows,
596without any explicit use of ``Force`` or ``Delay``:
600 boolCase : Bool -> Lazy a -> Lazy a -> a;
601 boolCase True t e = t;
602 boolCase False t e = e;
607Idris includes a number of useful data types and library functions
608(see the ``libs/`` directory in the distribution). This chapter
609describes a few of these. The functions described here are imported
610automatically by every Idris program, as part of ``Prelude.idr``.
615We have already seen the ``List`` and ``Vect`` data types:
619 data List a = Nil | (::) a (List a)
621 data Vect : Nat -> Type -> Type where
623 (::) : a -> Vect k a -> Vect (S k) a
625Note that the constructor names are the same for each — constructor
626names (in fact, names in general) can be overloaded, provided that
627they are declared in different namespaces (see Section
628:ref:`sect-namespaces`), and will typically be resolved according to
629their type. As syntactic sugar, any type with the constructor names
630``Nil`` and ``::`` can be written in list form. For example:
632- ``[]`` means ``Nil``
634- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
636The library also defines a number of functions for manipulating these
637types. ``map`` is overloaded both for ``List`` and ``Vect`` and
638applies a function to every element of the list or vector.
642 map : (a -> b) -> List a -> List b
644 map f (x :: xs) = f x :: map f xs
646 map : (a -> b) -> Vect n a -> Vect n b
648 map f (x :: xs) = f x :: map f xs
650For example, given the following vector of integers, and a function to
656 intVec = [1, 2, 3, 4, 5]
661the function ``map`` can be used as follows to double every element in
666 *usefultypes> show (map double intVec)
667 "[2, 4, 6, 8, 10]" : String
669You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
670directory. For more details of the functions available on ``List`` and
671``Vect``, look in the library files:
673- ``libs/prelude/Prelude/List.idr``
675- ``libs/base/Data/List.idr``
677- ``libs/base/Data/Vect.idr``
679- ``libs/base/Data/VectType.idr``
681Functions include filtering, appending, reversing, and so on. Also
682remember that Idris is still in development, so if you don’t see
683the function you need, please feel free to add it and submit a patch!
685Aside: Anonymous functions and operator sections
686~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688There are actually neater ways to write the above expression. One way
689would be to use an anonymous function:
693 *usefultypes> show (map (\x => x * 2) intVec)
694 "[2, 4, 6, 8, 10]" : String
696The notation ``\x => val`` constructs an anonymous function which takes
697one argument, ``x`` and returns the expression ``val``. Anonymous
698functions may take several arguments, separated by commas,
699e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
700e.g. ``\x : Int => x * 2``, and can pattern match,
701e.g. ``\(x, y) => x + y``. We could also use an operator section:
705 *usefultypes> show (map (* 2) intVec)
706 "[2, 4, 6, 8, 10]" : String
708``(*2)`` is shorthand for a function which multiplies a number
709by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
715``Maybe`` describes an optional value. Either there is a value of the
716given type, or there isn’t:
720 data Maybe a = Just a | Nothing
722``Maybe`` is one way of giving a type to an operation that may
723fail. For example, looking something up in a ``List`` (rather than a
724vector) may result in an out of bounds error:
728 list_lookup : Nat -> List a -> Maybe a
729 list_lookup _ Nil = Nothing
730 list_lookup Z (x :: xs) = Just x
731 list_lookup (S k) (x :: xs) = list_lookup k xs
733The ``maybe`` function is used to process values of type ``Maybe``,
734either by applying a function to the value, if there is one, or by
735providing a default value:
739 maybe : Lazy b -> (a -> b) -> Maybe a -> b
741Note that the type of the first argument is ``Lazy b`` rather than
742simply ``b``. Since the default value might not be used, we mark it as
743``Lazy`` in case it is a large expression where evaluating it then
744discarding it would be wasteful.
746Tuples and Dependent Pairs
747~~~~~~~~~~~~~~~~~~~~~~~~~~
749Values can be paired with the following built-in data type:
753 data Pair a b = MkPair a b
755As syntactic sugar, we can write ``(a, b)`` which, according to
756context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
757contain an arbitrary number of values, represented as nested pairs:
764 jim : (String, Int, String)
765 jim = ("Jim", 25, "Cambridge")
770Dependent pairs allow the type of the second element of a pair to depend
771on the value of the first element. Traditionally, these are referred to
776 data Sigma : (A : Type) -> (P : A -> Type) -> Type where
777 MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
779Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
780of a pair of A and P, where the name ``a`` can occur inside ``P``.
781``( a ** p )`` constructs a value of this type. For example, we can
782pair a number with a ``Vect`` of a particular length.
786 vec : (n : Nat ** Vect n Int)
789If you like, you can write it out the long way, the two are precisely
794 vec : Sigma Nat (\n => Vect n Int)
795 vec = MkSigma 2 [3, 4]
797The type checker could of course infer the value of the first element
798from the length of the vector. We can write an underscore ``_`` in
799place of values which we expect the type checker to fill in, so the
800above definition could also be written as:
804 vec : (n : Nat ** Vect n Int)
807We might also prefer to omit the type of the first element of the
808pair, since, again, it can be inferred:
812 vec : (n ** Vect n Int)
815One use for dependent pairs is to return values of dependent types
816where the index is not necessarily known in advance. For example, if
817we filter elements out of a ``Vect`` according to some predicate, we
818will not know in advance what the length of the resulting vector will
823 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
825If the ``Vect`` is empty, the result is easy:
829 filter p Nil = (_ ** [])
831In the ``::`` case, we need to inspect the result of a recursive call
832to ``filter`` to extract the length and the vector from the result. To
833do this, we use ``with`` notation, which allows pattern matching on
838 filter p (x :: xs) with (filter p xs)
839 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
841We will see more on ``with`` notation later.
851Intermediate values can be calculated using ``let`` bindings:
855 data Person = MkPerson String Int
857 showPerson : Person -> String
858 showPerson p = let MkPerson name age = p in
859 name ++ " is " ++ show age ++ " years old"
861 splitAt : Char -> String -> (String, String)
862 splitAt c x = case break (== c) x of
863 (x, y) => (x, strTail y)
865We can do simple pattern matching in ``let`` bindings too. For
866example, we can extract fields from a record as follows, as well as by
867pattern matching at the top level:
871 data Person = MkPerson String Int
873 showPerson : Person -> String
874 showPerson p = let MkPerson name age = p in
875 name ++ " is " ++ show age ++ " years old"
880Idris provides *comprehension* notation as a convenient shorthand
881for building lists. The general form is:
885 [ expression | qualifiers ]
887This generates the list of values produced by evaluating the
888``expression``, according to the conditions given by the comma
889separated ``qualifiers``. For example, we can build a list of
890Pythagorean triples as follows:
894 pythag : Int -> List (Int, Int, Int)
895 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
898The ``[a..b]`` notation is another shorthand which builds a list of
899numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
900list of numbers between ``a`` and ``c`` with the increment specified
901by the difference between ``a`` and ``b``. This works for any numeric
902type, using the ``count`` function from the prelude.
907Another way of inspecting intermediate values of *simple* types is to
908use a ``case`` expression. The following function, for example, splits
909a string into two at a given character:
913 splitAt : Char -> String -> (String, String)
914 splitAt c x = case break (== c) x of
915 (x, y) => (x, strTail y)
917``break`` is a library function which breaks a string into a pair of
918strings at the point where the given function returns true. We then
919deconstruct the pair it returns, and remove the first character of the
922A ``case`` expression can match several cases, for example, to inspect
923an intermediate value of type ``Maybe a``. Recall ``list_lookup``
924which looks up an index in a list, returning ``Nothing`` if the index
925is out of bounds. We can use this to write ``lookup_default``, which
926looks up an index and returns a default value if the index is out of
931 lookup_default : Nat -> List a -> a -> a
932 lookup_default i xs def = case list_lookup i xs of
936If the index is in bounds, we get the value at that index, otherwise
937we get a default value:
941 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
943 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
946**Restrictions:** The ``case`` construct is intended for simple
947analysis of intermediate expressions to avoid the need to write
948auxiliary functions, and is also used internally to implement pattern
949matching ``let`` and lambda bindings. It will *only* work if:
951- Each branch *matches* a value of the same type, and *returns* a value
954- The type of the result is “known”. i.e. the type of the expression
955 can be determined *without* type checking the ``case``-expression
961*Records* are data types which collect several values (the record's
962*fields*) together. Idris provides syntax for defining records and
963*automatically generating field access and update functions. For
964*example, we can represent a person's name and age in a record:
968 record Person : Type where
969 MkPerson : (name : String) ->
970 (age : Int) -> Person
973 fred = MkPerson "Fred" 30
975Record declarations are like ``data`` declarations, except that they
976are introduced by the ``record`` keyword, and can only have one
977constructor. The names of the binders in the constructor type
978(``name`` and ``age``) here are the field names, which we can use to
979access the field values:
988 name : Person -> String
990We can also use the field names to update a record (or, more
991precisely, produce a new record with the given fields updated).
995 *record> record { name = "Jim" } fred
996 MkPerson "Jim" 30 : Person
997 *record> record { name = "Jim", age = 20 } fred
998 MkPerson "Jim" 20 : Person
1000The syntax ``record { field = val, ... }`` generates a function which
1001updates the given fields in a record.
1003Records, and fields within records, can have dependent types. Updates
1004are allowed to change the type of a field, provided that the result is
1005well-typed, and the result does not affect the type of the record as a
1008.. code-block:: idris
1010 record Class : Type where
1011 ClassInfo : (students : Vect n Person) ->
1012 (className : String) ->
1015It is safe to update the ``students`` field to a vector of a different
1016length because it will not affect the type of the record:
1018.. code-block:: idris
1020 addStudent : Person -> Class -> Class
1021 addStudent p c = record { students = p :: students c } c
1025 *record> addStudent fred (ClassInfo [] "CS")
1026 ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1032Idris also provides a convenient syntax for accessing and updating
1033nested records. For example, if a field is accessible with the
1034expression ``c (b (a x))``, it can be updated using the following
1037.. code-block:: idris
1039 record { a->b->c = val } x
1041This returns a new record, with the field accessed by the path
1042``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
1043a->b->c = val }`` itself has a function type. Symmetrically, the field
1044can also be accessed with the following syntax:
1046.. code-block:: idris
1048 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