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)
252In Idris, types are a first class language construct, meaning that they
253can be computed and manipulated (and passed to functions) just like any
254other language construct. For example, we could write a function which
259 isSingleton : Bool -> Type
260 isSingleton True = Nat
261 isSingleton False = List Nat
263This function calculates the appropriate type from a ``Bool`` which flags
264whether the type should be a singleton or not. We can use this function
265to calculate a type anywhere that a type can be used. For example, it
266can be used to calculate a return type:
270 mkSingle : (x : Bool) -> isSingleton x
274Or it can be used to have varying input types. The following function
275calculates either the sum of a list of ``Nat``, or returns the given
276``Nat``, depending on whether the singleton flag is true:
280 sum : (single : Bool) -> isSingleton single -> Nat
283 sum True (x :: xs) = x + sum True xs
288A standard example of a dependent data type is the type of “lists with
289length”, conventionally called vectors in the dependent type
290literature. They are available as part of the Idris library, by
291importing ``Data.Vect``, or we can declare them as follows:
295 data Vect : Nat -> Type -> Type where
297 (::) : a -> Vect k a -> Vect (S k) a
299Note that we have used the same constructor names as for ``List``.
300Ad-hoc name overloading such as this is accepted by Idris,
301provided that the names are declared in different namespaces (in
302practice, normally in different modules). Ambiguous constructor names
303can normally be resolved from context.
305This declares a family of types, and so the form of the declaration is
306rather different from the simple type declarations above. We
307explicitly state the type of the type constructor ``Vect`` — it takes
308a ``Nat`` and a type as an argument, where ``Type`` stands for the
309type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
310*parameterised* by ``Type``. Each constructor targets a different part
311of the family of types. ``Nil`` can only be used to construct vectors
312with zero length, and ``::`` to construct vectors with non-zero
313length. In the type of ``::``, we state explicitly that an element of
314type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
315``k``) combine to make a vector of length ``S k``.
317We can define functions on dependent types such as ``Vect`` in the same
318way as on simple types such as ``List`` and ``Nat`` above, by pattern
319matching. The type of a function over ``Vect`` will describe what
320happens to the lengths of the vectors involved. For example, ``++``,
321defined as follows, appends two ``Vect``:
325 (++) : Vect n a -> Vect m a -> Vect (n + m) a
327 (++) (x :: xs) ys = x :: xs ++ ys
329The type of ``(++)`` states that the resulting vector’s length will be
330the sum of the input lengths. If we get the definition wrong in such a
331way that this does not hold, Idris will not accept the definition.
336 (++) : Vect n a -> Vect m a -> Vect (n + m) a
338 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
340When run through the Idris type checker, this results in the
345 $ idris vbroken.idr --check
346 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
347 When elaborating an application of constructor Vect.:::
348 Type mismatch between
349 Vect (k + k) a (Type of xs ++ xs)
351 Vect (plus k m) a (Expected type)
354 Type mismatch between
360This error message suggests that there is a length mismatch between
361two vectors — we needed a vector of length ``k + m``, but provided a
362vector of length ``k + k``.
367Finite sets, as the name suggests, are sets with a finite number of
368elements. They are available as part of the Idris library, by
369importing ``Data.Fin``, or can be declared as follows:
373 data Fin : Nat -> Type where
375 FS : Fin k -> Fin (S k)
377From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
378So this is not a set in the sense of a collection that is a container of objects,
379rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
380Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
381``n`` is the argument used to instantiate the ``Fin`` type.
382For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
384Let us look at the constructors in greater detail.
386``FZ`` is the zeroth element of a finite set with ``S k`` elements;
387``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
388elements. ``Fin`` is indexed by a ``Nat``, which represents the number
389of elements in the set. Since we can’t construct an element of an
390empty set, neither constructor targets ``Fin Z``.
392As mentioned above, a useful application of the ``Fin`` family is to represent bounded
393natural numbers. Since the first ``n`` natural numbers form a finite
394set of ``n`` elements, we can treat ``Fin n`` as the set of integers
395greater than or equal to zero and less than ``n``.
397For example, the following function which looks up an element in a
398``Vect``, by a bounded index given as a ``Fin n``, is defined in the
403 index : Fin n -> Vect n a -> a
404 index FZ (x :: xs) = x
405 index (FS k) (x :: xs) = index k xs
407This function looks up a value at a given location in a vector. The
408location is bounded by the length of the vector (``n`` in each case),
409so there is no need for a run-time bounds check. The type checker
410guarantees that the location is no larger than the length of the
411vector, and of course no less than zero.
413Note also that there is no case for ``Nil`` here. This is because it
414is impossible. Since there is no element of ``Fin Z``, and the
415location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
416attempting to look up an element in an empty vector would give a
417compile time type error, since it would force ``n`` to be ``Z``.
422Let us take a closer look at the type of ``index``:
426 index : Fin n -> Vect n a -> a
428It takes two arguments, an element of the finite set of ``n`` elements,
429and a vector with ``n`` elements of type ``a``. But there are also two
430names, ``n`` and ``a``, which are not declared explicitly. These are
431*implicit* arguments to ``index``. We could also write the type of
436 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
438Implicit arguments, given in braces ``{}`` in the type declaration,
439are not given in applications of ``index``; their values can be
440inferred from the types of the ``Fin n`` and ``Vect n a``
441arguments. Any name beginning with a lower case letter which appears
442as a parameter or index in a
443type declaration, but which is otherwise unbound, will be automatically
444bound as an implicit argument. Implicit arguments can still be given
445explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
450 index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
452In fact, any argument, implicit or explicit, may be given a name. We
453could have declared the type of ``index`` as:
457 index : (i:Fin n) -> (xs:Vect n a) -> a
459It is a matter of taste whether you want to do this — sometimes it can
460help document a function by making the purpose of an argument more
466Sometimes it is useful to provide types of implicit arguments,
467particularly where there is a dependency ordering, or where the
468implicit arguments themselves have dependencies. For example, we may
469wish to state the types of the implicit arguments in the following
470definition, which defines a predicate on vectors:
474 data Elem : a -> Vect n a -> Type where
475 Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
476 There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
478An instance of ``Elem x xs`` states that ``x`` is an element of
479``xs``. We can construct such a predicate if the required element is
480``Here``, at the head of the vector, or ``There``, in the tail of the
486 testVec = 3 :: 4 :: 5 :: 6 :: Nil
488 inVect : Elem 5 testVec
489 inVect = There (There Here)
491If the same implicit arguments are being used a lot, it can make a
492definition difficult to read. To avoid this problem, a ``using`` block
493gives the types and ordering of any implicit arguments which can
494appear within the block:
498 using (x:a, y:a, xs:Vect n a)
499 data Elem : a -> Vect n a -> Type where
500 Here : Elem x (x :: xs)
501 There : Elem x xs -> Elem x (y :: xs)
503Note: Declaration Order and ``mutual`` blocks
504---------------------------------------------
506In general, functions and data types must be defined before use, since
507dependent types allow functions to appear as part of types, and their
508reduction behaviour to affect type checking. However, this restriction
509can be relaxed by using a ``mutual`` block, which allows data types
510and functions to be defined simultaneously:
523In a ``mutual`` block, first all of the type declarations are added,
524then the function bodies. As a result, none of the function types can
525depend on the reduction behaviour of any of the functions in the
531Computer programs are of little use if they do not interact with the
532user or the system in some way. The difficulty in a pure language such
533as Idris — that is, a language where expressions do not have
534side-effects — is that I/O is inherently side-effecting. Therefore in
535Idris, such interactions are encapsulated in the type ``IO``:
539 data IO a -- IO operation returning a value of type a
541We’ll leave the definition of ``IO`` abstract, but effectively it
542describes what the I/O operations to be executed are, rather than how
543to execute them. The resulting operations are executed externally, by
544the run-time system. We’ve already seen one IO program:
549 main = putStrLn "Hello world"
551The type of ``putStrLn`` explains that it takes a string, and returns
552an element of the unit type ``()`` via an I/O action. There is a
553variant ``putStr`` which outputs a string without a newline:
557 putStrLn : String -> IO ()
558 putStr : String -> IO ()
560We can also read strings from user input:
566A number of other I/O operations are defined in the prelude, for
567example for reading and writing files, including:
571 data File -- abstract
572 data Mode = Read | Write | ReadWrite
574 openFile : String -> Mode -> IO File
575 closeFile : File -> IO ()
577 fread : File -> IO String
578 fwrite : File -> String -> IO ()
579 feof : File -> IO Bool
581 readFile : String -> IO String
588I/O programs will typically need to sequence actions, feeding the
589output of one computation into the input of the next. ``IO`` is an
590abstract type, however, so we can’t access the result of a computation
591directly. Instead, we sequence operations with ``do`` notation:
596 greet = do putStr "What is your name? "
598 putStrLn ("Hello " ++ name)
600The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
601type ``IO a``, and puts the result, of type ``a`` into the variable
602``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
603has type ``String``. Indentation is significant — each statement in
604the do block must begin in the same column. The ``return`` operation
605allows us to inject a value directly into an IO operation:
611As we will see later, ``do`` notation is more general than this, and
619Normally, arguments to functions are evaluated before the function
620itself (that is, Idris uses *eager* evaluation). However, this is
621not always the best approach. Consider the following function:
625 ifThenElse : Bool -> a -> a -> a;
626 ifThenElse True t e = t;
627 ifThenElse False t e = e;
629This function uses one of the ``t`` or ``e`` arguments, but not both
630(in fact, this is used to implement the ``if...then...else`` construct
631as we will see later. We would prefer if *only* the argument which was
632used was evaluated. To achieve this, Idris provides a ``Lazy``
633data type, which allows evaluation to be suspended:
637 data Lazy : Type -> Type where
638 Delay : (val : a) -> Lazy a
642A value of type ``Lazy a`` is unevaluated until it is forced by
643``Force``. The Idris type checker knows about the ``Lazy`` type,
644and inserts conversions where necessary between ``Lazy a`` and ``a``,
645and vice versa. We can therefore write ``ifThenElse`` as follows,
646without any explicit use of ``Force`` or ``Delay``:
650 ifThenElse : Bool -> Lazy a -> Lazy a -> a;
651 ifThenElse True t e = t;
652 ifThenElse False t e = e;
657Idris includes a number of useful data types and library functions
658(see the ``libs/`` directory in the distribution). This chapter
659describes a few of these. The functions described here are imported
660automatically by every Idris program, as part of ``Prelude.idr``.
665We have already seen the ``List`` and ``Vect`` data types:
669 data List a = Nil | (::) a (List a)
671 data Vect : Nat -> Type -> Type where
673 (::) : a -> Vect k a -> Vect (S k) a
675Note that the constructor names are the same for each — constructor
676names (in fact, names in general) can be overloaded, provided that
677they are declared in different namespaces (see Section
678:ref:`sect-namespaces`), and will typically be resolved according to
679their type. As syntactic sugar, any type with the constructor names
680``Nil`` and ``::`` can be written in list form. For example:
682- ``[]`` means ``Nil``
684- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
686The library also defines a number of functions for manipulating these
687types. ``map`` is overloaded both for ``List`` and ``Vect`` and
688applies a function to every element of the list or vector.
692 map : (a -> b) -> List a -> List b
694 map f (x :: xs) = f x :: map f xs
696 map : (a -> b) -> Vect n a -> Vect n b
698 map f (x :: xs) = f x :: map f xs
700For example, given the following vector of integers, and a function to
706 intVec = [1, 2, 3, 4, 5]
711the function ``map`` can be used as follows to double every element in
716 *usefultypes> show (map double intVec)
717 "[2, 4, 6, 8, 10]" : String
719You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
720directory. For more details of the functions available on ``List`` and
721``Vect``, look in the library files:
723- ``libs/prelude/Prelude/List.idr``
725- ``libs/base/Data/List.idr``
727- ``libs/base/Data/Vect.idr``
729- ``libs/base/Data/VectType.idr``
731Functions include filtering, appending, reversing, and so on. Also
732remember that Idris is still in development, so if you don’t see
733the function you need, please feel free to add it and submit a patch!
735Aside: Anonymous functions and operator sections
736------------------------------------------------
738There are actually neater ways to write the above expression. One way
739would be to use an anonymous function:
743 *usefultypes> show (map (\x => x * 2) intVec)
744 "[2, 4, 6, 8, 10]" : String
746The notation ``\x => val`` constructs an anonymous function which takes
747one argument, ``x`` and returns the expression ``val``. Anonymous
748functions may take several arguments, separated by commas,
749e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
750e.g. ``\x : Int => x * 2``, and can pattern match,
751e.g. ``\(x, y) => x + y``. We could also use an operator section:
755 *usefultypes> show (map (* 2) intVec)
756 "[2, 4, 6, 8, 10]" : String
758``(*2)`` is shorthand for a function which multiplies a number
759by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
765``Maybe`` describes an optional value. Either there is a value of the
766given type, or there isn’t:
770 data Maybe a = Just a | Nothing
772``Maybe`` is one way of giving a type to an operation that may
773fail. For example, looking something up in a ``List`` (rather than a
774vector) may result in an out of bounds error:
778 list_lookup : Nat -> List a -> Maybe a
779 list_lookup _ Nil = Nothing
780 list_lookup Z (x :: xs) = Just x
781 list_lookup (S k) (x :: xs) = list_lookup k xs
783The ``maybe`` function is used to process values of type ``Maybe``,
784either by applying a function to the value, if there is one, or by
785providing a default value:
789 maybe : Lazy b -> (a -> b) -> Maybe a -> b
791Note that the type of the first argument is ``Lazy b`` rather than
792simply ``b``. Since the default value might not be used, we mark it as
793``Lazy`` in case it is a large expression where evaluating it then
794discarding it would be wasteful.
796Tuples and Dependent Pairs
797--------------------------
799Values can be paired with the following built-in data type:
803 data Pair a b = MkPair a b
805As syntactic sugar, we can write ``(a, b)`` which, according to
806context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
807contain an arbitrary number of values, represented as nested pairs:
814 jim : (String, Int, String)
815 jim = ("Jim", 25, "Cambridge")
820Dependent pairs allow the type of the second element of a pair to depend
821on the value of the first element. Traditionally, these are referred to
826 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
827 MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P
829Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
830of a pair of A and P, where the name ``a`` can occur inside ``P``.
831``( a ** p )`` constructs a value of this type. For example, we can
832pair a number with a ``Vect`` of a particular length.
836 vec : (n : Nat ** Vect n Int)
839If you like, you can write it out the long way, the two are precisely
844 vec : Sigma Nat (\n => Vect n Int)
845 vec = MkSigma 2 [3, 4]
847The type checker could of course infer the value of the first element
848from the length of the vector. We can write an underscore ``_`` in
849place of values which we expect the type checker to fill in, so the
850above definition could also be written as:
854 vec : (n : Nat ** Vect n Int)
857We might also prefer to omit the type of the first element of the
858pair, since, again, it can be inferred:
862 vec : (n ** Vect n Int)
865One use for dependent pairs is to return values of dependent types
866where the index is not necessarily known in advance. For example, if
867we filter elements out of a ``Vect`` according to some predicate, we
868will not know in advance what the length of the resulting vector will
873 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
875If the ``Vect`` is empty, the result is easy:
879 filter p Nil = (_ ** [])
881In the ``::`` case, we need to inspect the result of a recursive call
882to ``filter`` to extract the length and the vector from the result. To
883do this, we use ``with`` notation, which allows pattern matching on
888 filter p (x :: xs) with (filter p xs)
889 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
891We will see more on ``with`` notation later.
901Intermediate values can be calculated using ``let`` bindings:
905 data Person = MkPerson String Int
907 showPerson : Person -> String
908 showPerson p = let MkPerson name age = p in
909 name ++ " is " ++ show age ++ " years old"
911 splitAt : Char -> String -> (String, String)
912 splitAt c x = case break (== c) x of
913 (x, y) => (x, strTail y)
915We can do simple pattern matching in ``let`` bindings too. For
916example, we can extract fields from a record as follows, as well as by
917pattern matching at the top level:
921 data Person = MkPerson String Int
923 showPerson : Person -> String
924 showPerson p = let MkPerson name age = p in
925 name ++ " is " ++ show age ++ " years old"
930Idris provides *comprehension* notation as a convenient shorthand
931for building lists. The general form is:
935 [ expression | qualifiers ]
937This generates the list of values produced by evaluating the
938``expression``, according to the conditions given by the comma
939separated ``qualifiers``. For example, we can build a list of
940Pythagorean triples as follows:
944 pythag : Int -> List (Int, Int, Int)
945 pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
948The ``[a..b]`` notation is another shorthand which builds a list of
949numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
950list of numbers between ``a`` and ``c`` with the increment specified
951by the difference between ``a`` and ``b``. This works for any numeric
952type, using the ``count`` function from the prelude.
957Another way of inspecting intermediate values of *simple* types is to
958use a ``case`` expression. The following function, for example, splits
959a string into two at a given character:
963 splitAt : Char -> String -> (String, String)
964 splitAt c x = case break (== c) x of
965 (x, y) => (x, strTail y)
967``break`` is a library function which breaks a string into a pair of
968strings at the point where the given function returns true. We then
969deconstruct the pair it returns, and remove the first character of the
972A ``case`` expression can match several cases, for example, to inspect
973an intermediate value of type ``Maybe a``. Recall ``list_lookup``
974which looks up an index in a list, returning ``Nothing`` if the index
975is out of bounds. We can use this to write ``lookup_default``, which
976looks up an index and returns a default value if the index is out of
981 lookup_default : Nat -> List a -> a -> a
982 lookup_default i xs def = case list_lookup i xs of
986If the index is in bounds, we get the value at that index, otherwise
987we get a default value:
991 *usefultypes> lookup_default 2 [3,4,5,6] (-1)
993 *usefultypes> lookup_default 4 [3,4,5,6] (-1)
996**Restrictions:** The ``case`` construct is intended for simple
997analysis of intermediate expressions to avoid the need to write
998auxiliary functions, and is also used internally to implement pattern
999matching ``let`` and lambda bindings. It will *only* work if:
1001- Each branch *matches* a value of the same type, and *returns* a
1002 value of the same type.
1004- The type of the result is "known". i.e. the type of the expression
1005 can be determined *without* type checking the ``case``-expression
1011*Records* are data types which collect several values (the record's
1012*fields*) together. Idris provides syntax for defining records and
1013*automatically generating field access and update functions*. For
1014example, we can represent a person's name and age in a record:
1016.. code-block:: idris
1019 constructor MkPerson
1024 fred = MkPerson "Fred" 30
1026Records can have *parameters*, which are listed between the record
1027name and the ``where`` keyword, and *fields*, which are in an indented
1028block following the `where` keyword (here, ``name`` and ``age``). The
1029constructor name is provided after the ``constructor`` keyword. The
1030field names can be used to access the field values:
1039 name : Person -> String
1041We can also use the field names to update a record (or, more
1042precisely, produce a copy of the record with the given fields
1047 *record> record { name = "Jim" } fred
1048 MkPerson "Jim" 30 : Person
1049 *record> record { name = "Jim", age = 20 } fred
1050 MkPerson "Jim" 20 : Person
1052The syntax ``record { field = val, ... }`` generates a function which
1053updates the given fields in a record.
1055Records, and fields within records, can have dependent types. Updates
1056are allowed to change the type of a field, provided that the result is
1059.. code-block:: idris
1062 constructor ClassInfo
1063 students : Vect n Person
1066It is safe to update the ``students`` field to a vector of a different
1067length because it will not affect the type of the record:
1069.. code-block:: idris
1071 addStudent : Person -> Class -> Class
1072 addStudent p c = record { students = p :: students c } c
1076 *record> addStudent fred (ClassInfo [] "CS")
1077 ClassInfo [MkPerson "Fred" 30] "CS" : Class
1082Idris also provides a convenient syntax for accessing and updating
1083nested records. For example, if a field is accessible with the
1084expression ``c (b (a x))``, it can be updated using the following
1087.. code-block:: idris
1089 record { a->b->c = val } x
1091This returns a new record, with the field accessed by the path
1092``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
1093a->b->c = val }`` itself has a function type. Symmetrically, the field
1094can also be accessed with the following syntax:
1096.. code-block:: idris
1098 record { a->b->c } x
1100Parameters and Fields
1101---------------------
1103Records can have *parameters*, which are not subject to field
1104updates. The parameters appear as arguments to the resulting type, and
1105are written following the record type name. For example, a pair type
1106could be defined as follows:
1108.. code-block:: idris
1110 record Prod a b where
1115The parameters to a record type need not be types. For example, we can
1116restrict the size of classes using a ``Nat`` parameter to the
1119.. code-block:: idris
1121 record SizedClass (size : Nat) where
1122 constructor SizedClassInfo
1123 students : Vect size Person
1126Note that it is no longer possible to write ``addStudent`` for this
1127type, as that would change the size of the class.
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