1\section{Types and Functions}
3\subsection{Primitive Types}
5\Idris{} defines several primitive types: \tTC{Int}, \tTC{Integer} and
6\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for
7text manipulation, and \tTC{Ptr} which represents foreign pointers.
8There are also several data types declared in the library, including
9\tTC{Bool}, with values \tDC{True} and \tDC{False}.
10We can declare some constants with these types. Enter the following
11into a file \texttt{prims.idr} and load it into the \Idris{} interactive
12environment by typing \texttt{idris prims.idr}:
21foo = "Sausage machine"
31An \Idris{} file consists of an optional module declaration (here
32\texttt{module prims}) followed by an optional list of imports (none here,
33however \Idris{} programs can consist of several modules, and the definitions
34in each module each have their own namespace, as we will discuss in Section
35\ref{sect:namespaces}) and a
36collection of declarations and definitions. The order of definitions is
37significant --- functions and data types must be defined before use.
38Each definition must have a type
39declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
40Indentation is significant --- a new declaration begins at the same level
41of indentation as the preceding declaration. Alternatively, declarations
42may be terminated with a semicolon.
44A library module \texttt{prelude} is automatically imported by every \Idris{} program,
45including facilities for IO, arithmetic, data structures and various common
46functions. The prelude defines several arithmetic and comparison operators,
47which we can use at the prompt. Evaluating things at the prompt gives an
48answer, and the type of the answer. For example:
58All of the usual arithmetic and comparison operators are defined for the primitive
59types. They are overloaded using type classes, as we will discuss in Section
60\ref{sec:classes} and can be extended to work on user defined types.
61Boolean expressions can be tested with the \texttt{if...then...else} construct:
64*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
68\subsection{Data Types}
70Data types are declared in a similar way to Haskell data types, with a similar
71syntax. Natural numbers and lists, for example, can be declared as follows:
74data Nat = Z | S Nat -- Natural numbers
75 -- (zero and successor)
76data List a = Nil | (::) a (List a) -- Polymorphic lists
80The above declarations are taken from the standard library. Unary natural
81numbers can be either zero (\texttt{Z}), or
82the successor of another natural number (\texttt{S k}).
83Lists can either be empty (\texttt{Nil})
84or a value added to the front of another list (\texttt{x :: xs}).
85In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
86such as this can be added using a fixity declaration, as follows:
93Functions, data constructors and type constuctors may all be given infix
94operators as names. They may be used in prefix form if enclosed in brackets,
95e.g. \tDC{(::)}. Infix operators can use any of the symbols:
101\subsection{Functions}
103Functions are implemented by pattern matching, again using a similar syntax to
104Haskell. The main difference is that \Idris{} requires type declarations for all
105functions, using a single colon \texttt{:} (rather than
106Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
107defined as follows, again taken from the standard library:
111plus : Nat -> Nat -> Nat
113plus (S k) y = S (plus k y)
115-- Unary multiplication
116mult : Nat -> Nat -> Nat
118mult (S k) y = plus y (mult k y)
122The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
123for use by \texttt{Nat}, and are implemented
124using the above functions. Unlike Haskell, there is no restriction on whether
125types and function names must begin with a capital letter or not. Function
126names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{Z}, \tDC{S},
127\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
128all part of the same namespace.
130We can test these functions at the \Idris{} prompt:
133Idris> plus (S (S Z)) (S (S Z))
135Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
136S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
140Like arithmetic operations, integer literals are also overloaded using type classes,
141meaning that we can also test the functions as follows:
146Idris> mult 3 (plus 2 2)
147S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
151You may wonder, by the way, why we have unary natural numbers when our
152computers have perfectly good integer arithmetic built in. The reason is
153primarily that unary numbers have a very convenient structure which is easy to
154reason about, and easy to relate to other data structures as we will see later.
155Nevertheless, we do not want this convenience to be at the expense of
156efficiency. Fortunately, \Idris{} knows about the relationship between
157\tTC{Nat} (and similarly structured types) and numbers, so optimises the
158representation and functions such as \tFN{plus} and \tFN{mult}.
160\subsubsection*{\texttt{where} clauses}
162Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,
163to define a function which reverses a list, we can use an auxiliary function which
164accumulates the new, reversed list, and which does not need to be visible globally:
167reverse : List a -> List a
168reverse xs = revAcc [] xs where
169 revAcc : List a -> List a -> List a
171 revAcc acc (x :: xs) = revAcc (x :: acc) xs
175Indentation is significant --- functions in the \texttt{where} block must be indented
176further than the outer function.
179Any names which are visible in the outer scope are also visible in the
180\texttt{where} clause (unless they have been redefined, such as \texttt{xs}
181here). A name which appears only in the type will be in scope in the
182\texttt{where} clause if it is a \remph{parameter} to one of the types,
183i.e. it is fixed across the entire structure.
185As well as functions, \texttt{where} blocks can include local data
186declarations, such as the following where \texttt{MyLT} is not accessible outside
187the definition of \texttt{foo}:
198 isLT = if x < 20 then Yes else No
202In general, functions defined in a \texttt{where} clause need a type declaration
203just like any top level function. However, the type declaration for
204a function \texttt{f} \remph{can} be omitted if:
207\item \texttt{f} appears in the right hand side of the top level definition
208\item The type of \texttt{f} can be completely determined from its first
213So, for example, the following definitions are legal:
218even (S k) = odd k where
223test = [c (S 1), c Z, d (S Z)]
225 d y = c (y + 1 + z y)
229\subsection{Dependent Types}
231\subsubsection{Vectors}
233A standard example of a dependent type is the type of ``lists with length'',
234conventionally called vectors in the dependent type literature. In \Idris{},
235we declare vectors as follows\footnote{Note that prior to \Idris{} 0.9.9,
236the order of the arguments to \texttt{Vect} was reversed.}:
239data Vect : Nat -> Type -> Type where
241 (::) : a -> Vect k a -> Vect (S k) a
245Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
246name overloading such as this is accepted by \Idris{}, provided that the names
247are declared in different namespaces (in practice, normally in different modules).
248Ambiguous constructor names can normally be resolved from context.
250This declares a family of types, and so the form of the declaration is rather
251different from the simple type declarations above. We explicitly state the type
252of the type constructor \tTC{Vect} --- it takes a \tTC{Nat} and a type as an
253argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}
254is \emph{indexed} over \tTC{Nat} and \emph{parameterised} by \tTC{Type}. Each
255constructor targets a different part of the family of types. \tDC{Nil} can only
256be used to construct vectors with zero length, and \tDC{::} to construct
257vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element
258of type \texttt{a} and a tail of type \texttt{Vect k a} (i.e., a vector of length \texttt{k})
259combine to make a vector of length \texttt{S k}.
261We can define functions on dependent types such as \tTC{Vect} in the same way
262as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
263The type of a function over \tTC{Vect} will describe what happens to the
264lengths of the vectors involved. For example, \tFN{++}, defined in the
265library, appends two \tTC{Vect}s:
268(++) : Vect n a -> Vect m a -> Vect (n + m) a
270(++) (x :: xs) ys = x :: xs ++ ys
274The type of \tFN{(++)} states that the resulting vector's length will be the sum of
275the input lengths. If we get the definition wrong in such a way that this does
276not hold, \Idris{} will not accept the definition. For example:
279(++) : Vect n a -> Vect m a -> Vect (n + m) a
281(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
285$ idris vbroken.idr --check
286vbroken.idr:3:Can't unify Vect n a with Vect m a
294This error message suggests that there is a length mismatch between two vectors
295--- we needed a vector of length \texttt{m}, but provided a vector
297%Note that the terms in the error message have been \emph{normalised}, so in
298%particular \texttt{n + m} has been reduced to \texttt{plus n m}.
300\subsubsection{The Finite Sets}
302Finite sets, as the name suggests, are sets with a finite number of elements.
303They are declared as follows (again, in the prelude):
306data Fin : Nat -> Type where
308 fS : Fin k -> Fin (S k)
312\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements;
314\texttt{n+1}th element of a finite set with \texttt{S k} elements.
315\tTC{Fin} is indexed by a \tTC{Nat}, which
316represents the number of elements in the set. Obviously we can't construct an
317element of an empty set, so neither constructor targets \texttt{Fin Z}.
319A useful application of the \tTC{Fin} family is to represent bounded
320natural numbers. Since the first \tTC{n} natural numbers form a finite
321set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural
322numbers bounded by \tTC{n}.
324For example, the following function which looks up an element in a \tTC{Vect},
325by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
328index : Fin n -> Vect n a -> a
329index fZ (x :: xs) = x
330index (fS k) (x :: xs) = index k xs
334This function looks up a value at a given location in a vector. The location is
335bounded by the length of the vector (\texttt{n} in each case), so there is no
336need for a run-time bounds check. The type checker guarantees that the location
337is no larger than the length of the vector.
339Note also that there is no case for \texttt{Nil} here. This is because it is
340impossible. Since there is no element of \texttt{Fin Z}, and the location is a
341\texttt{Fin n}, then \texttt{n} can not be \tDC{Z}. As a result, attempting to
342look up an element in an empty vector would give a compile time type error,
343since it would force \texttt{n} to be \tDC{Z}.
345\subsubsection{Implicit Arguments}
347Let us take a closer look at the type of \texttt{index}:
350index : Fin n -> Vect n a -> a
354It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
355with \texttt{n} elements of type \texttt{a}. But there are also two names,
356\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
357arguments to \texttt{index}. We could also write the type of \texttt{index} as:
360index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
364Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
365not given in applications of \texttt{index}; their values can be inferred from
366the types of the \texttt{Fin n} and \texttt{Vect n a} arguments. Any name
367with a \remph{lower case initial letter} which
368appears as a parameter or index in a type declaration, but which is otherwise
369free, will be automatically bound as an implicit argument. Implicit arguments
370can still be given explicitly in applications, using \texttt{\{a=value\}} and
371\texttt{\{n=value\}}, for example:
374index {a=Int} {n=2} fZ (2 :: 3 :: Nil)
378In fact, any argument, implicit or explicit, may be given a name. We could have
379declared the type of \texttt{index} as:
382index : (i:Fin n) -> (xs:Vect n a) -> a
386It is a matter of taste whether you want to do this --- sometimes it can help
387document a function by making the purpose of an argument more clear.
389\subsubsection{``\texttt{using}'' notation}
391Sometimes it is necessary to provide types of implicit arguments where
392the type checker can not work them out itself. This can happen if there is a
393dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
394before being used --- or if an implicit argument has a complex type. For example,
395we will need to state the types of the implicit arguments in the following
396definition, which defines a predicate on vectors:
399data Elem : a -> Vect n a -> Type where
400 here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
401 there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
405An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
406\texttt{xs}. We can construct
407such a predicate if the required element is \texttt{here}, at the head of the vector,
408or \texttt{there}, in the tail of the vector. For example:
412testVec = 3 :: 4 :: 5 :: 6 :: Nil
414inVect : Elem 5 testVec
415inVect = there (there here)
419If the same implicit arguments are being used a lot, it can make a definition
420difficult to read. To avoid this problem, a \texttt{using} block gives the types and
421ordering of any implicit arguments which can appear within the block:
424using (x:a, y:a, xs:Vect n a)
425 data Elem : a -> Vect n a -> Type where
426 here : Elem x (x :: xs)
427 there : Elem x xs -> Elem x (y :: xs)
431\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
433In general, functions and data types must be defined before use, since
434dependent types allow functions to appear as part of types, and their
435reduction behaviour to affect type checking. However, this
436restriction can be relaxed by using a \texttt{mutual} block, which allows
437data types and functions to be defined simultaneously:
452In a \texttt{mutual} block, first all of the type declarations are added,
453then the function bodies. As a result, none of the function types can depend
454on the reduction behaviour of any of the functions in the block.
458Computer programs are of little use if they do not interact with the user or
459the system in some way. The difficulty in a pure language such as \Idris{} ---
460that is, a language where expressions do not have side-effects --- is that I/O
461is inherently side-effecting. Therefore in \Idris{}, such interactions are
462encapsulated in the type \texttt{IO}:
465data IO a -- IO operation returning a value of type a
470We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
471the I/O operations to be executed are, rather than how to execute them. The
472resulting operations are executed externally,
473by the run-time system. We've already seen one IO
478main = putStrLn "Hello world"
483The type of \texttt{putStrLn} explains that it takes a string, and returns an
484element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
485outputs a string without a newline:
488putStrLn : String -> IO ()
489putStr : String -> IO ()
492We can also read strings from user input:
500A number of other I/O operations are defined in the prelude, for example for reading and
501writing files, including:
505data Mode = Read | Write | ReadWrite
507openFile : String -> Mode -> IO File
508closeFile : File -> IO ()
510fread : File -> IO String
511fwrite : File -> String -> IO ()
512feof : File -> IO Bool
514readFile : String -> IO String
518\subsection{``\texttt{do}'' notation}
522I/O programs will typically need to sequence actions, feeding the output of one
523computation into the input of the next. \texttt{IO} is an abstract type, however, so we
524can't access the result of a computation directly. Instead, we sequence
525operations with \texttt{do} notation:
529greet = do putStr "What is your name? "
531 putStrLn ("Hello " ++ name)
536The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
538puts the result, of type \texttt{a} into the variable \texttt{x}.
539In this case, \texttt{getLine} returns an \texttt{IO String},
540so \texttt{name} has type \texttt{String}. Indentation is significant --- each
541statement in the do block must begin in the same column.
542The \texttt{return} operation allows us to inject a value directly into an IO
551As we will see later, \texttt{do} notation is more general than this, and can be
554\subsection{Useful Data Types}
556\Idris{} includes a number of useful data types and library functions (see the
557\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
558functions described here are imported automatically by every \Idris{} program, as
559part of \texttt{prelude.idr}.
561\subsubsection{\texttt{List} and \texttt{Vect}}
563We have already seen the \texttt{List} and \texttt{Vect} data types:
566data List a = Nil | (::) a (List a)
568data Vect : Nat -> Type -> Type where
570 (::) : a -> Vect k a -> Vect (S k) a
575Note that the constructor names are the same for each --- constructor names (in
576fact, names in general) can be overloaded, provided that they are declared in
577different namespaces (see Section \ref{sect:namespaces}), and will typically be
578resolved according to their type. As syntactic sugar, any type with the constructor
579names \texttt{Nil} and \texttt{::} can be written in list form. For example:
582\item \texttt{[]} means \texttt{Nil}
583\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
587The library also defines a number of functions for manipulating these types.
588\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
589and applies a function to every element of the list or vector.
592map : (a -> b) -> List a -> List b
594map f (x :: xs) = f x :: map f xs
596map : (a -> b) -> Vect n a -> Vect n b
598map f (x :: xs) = f x :: map f xs
603For example, to double every element in a vector of integers:
607intVec = [1, 2, 3, 4, 5]
615You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
618*usefultypes> show (map double intVec)
619"[2, 4, 6, 8, 10]" : String
624For more details of the functions available on \texttt{List} and \texttt{Vect},
625look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
626Functions include filtering, appending, reversing, and so on. Also remember
627that \Idris{} is still in development, so if you don't see the function you
628need, please feel free to add it and submit a patch!
630\subsubsection*{Aside: Anonymous functions and operator sections}
632There are actually neater ways to write the above expression. One way would be
633to use an anonymous function:
636*usefultypes> show (map (\x => x * 2) intVec)
637"[2, 4, 6, 8, 10]" : String
642The notation \texttt{$\backslash$x => val} constructs an anonymous function
643which takes one argument, \texttt{x} and returns the expression \texttt{val}.
644Anonymous functions may take several arguments, separated by commas, e.g.
645\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
646types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
647e.g. \texttt{$\backslash$ (x, y) => x + y}.
648We could also use an operator section:
651*usefultypes> show (map (* 2) intVec)
652"[2, 4, 6, 8, 10]" : String
657\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
658\texttt{$\backslash$x => x * 2}.
659Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
663\texttt{Maybe} describes an optional value. Either there is a value of the given type,
667data Maybe a = Just a | Nothing
672\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
673looking something up in a \texttt{List} (rather than a vector) may result in an out of
677list_lookup : Nat -> List a -> Maybe a
678list_lookup _ Nil = Nothing
679list_lookup Z (x :: xs) = Just x
680list_lookup (S k) (x :: xs) = list_lookup k xs
685The \texttt{maybe} function is used to process values of type \texttt{Maybe},
686either by applying a function to the value, if there is one, or by providing a default value:
689maybe : Maybe a -> |(default:b) -> (a -> b) -> b
694The vertical bar $\mid$ before the default value is a laziness annotation. Normally
695expressions are evaluated before being passed to a function. This is typically
696the most efficient behaviour. However, in this case, the default value might
697not be used and if it is a large expression, evaluating it will be wasteful.
698The $\mid$ annotation tells the compiler not to evaluate the argument until it is
701\subsubsection{Tuples and Dependent Pairs}
703Values can be paired with the following built-in data type:
706data Pair a b = MkPair a b
711As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
712means either \texttt{Pair a b} or \texttt{MkPair a b}.
713Tuples can contain an arbitrary number of values, represented as nested pairs:
719jim : (String, Int, String)
720jim = ("Jim", 25, "Cambridge")
724\subsubsection*{Dependent Pairs}
726Dependent pairs allow the type of the second element of a pair to depend on
727the value of the first element:
730data Exists : (A : Type) -> (P : A -> Type) -> Type where
731 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
736Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
737A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}
738constructs a value of this type. For example, we can pair a number with a
739\texttt{Vect} of a particular length.
742vec : (n : Nat ** Vect n Int)
748The type checker could of course infer the value of the first element from the
749length of the vector. We can write an underscore \texttt{\_} in place of values which we
750expect the type checker to fill in, so the above definition could also be
754vec : (n : Nat ** Vect n Int)
760We might also prefer to omit the type of the first element of the pair, since,
761again, it can be inferred:
764vec : (n ** Vect n Int)
770One use for dependent pairs is to return values of dependent types where the
771index is not necessarily known in advance. For example, if we filter elements
772out of a \texttt{Vect} according to some predicate, we will not know in advance what the
773length of the resulting vector will be:
776filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
781If the \texttt{Vect} is empty, the result is easy:
784filter p Nil = (_ ** [])
789In the \texttt{::} case, we need to inspect the result of a recursive call to
791extract the length and the vector from the result. To do this, we use \texttt{with}
792notation, which allows pattern matching on intermediate values:
795filter p (x :: xs) with (filter p xs)
796 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
800We will see more on \texttt{with} notation later.
802\subsection{\texttt{so}}
804The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
808data so : Bool -> Type where
814This is most useful for providing a static guarantee that a dynamic check has been made.
815For example, we might provide a safe interface to a function which draws a pixel
816on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
817the point \texttt{(x,y)} is within the bounds of a 640x480 window:
820inBounds : Int -> Int -> Bool
821inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
823drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
824drawPoint x y p = unsafeDrawPoint x y
828\subsection{More Expressions}
830\subsubsection*{\texttt{let} bindings}
832Intermediate values can be calculated using \texttt{let} bindings:
835mirror : List a -> List a
836mirror xs = let xs' = rev xs in
842We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
843fields from a record as follows, as well as by pattern matching at the top level:
846data Person = MkPerson String Int
848showPerson : Person -> String
849showPerson p = let MkPerson name age = p in
850 name ++ " is " ++ show age ++ " years old"
854\subsubsection*{List comprehensions}
858\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
859building lists. The general form is:
862[ expression | qualifiers ]
867This generates the list of values produced by evaluating the
868\texttt{expression}, according to the conditions given by the comma separated
869\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
873pythag : Int -> List (Int, Int, Int)
874pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
880The \texttt{[a..b]} notation is another shorthand which builds a list of
881numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]}
882builds a list of numbers between \texttt{a} and \texttt{c} with the increment
883specified by the difference between \texttt{a} and \texttt{b}. This works for
884any numeric type, using the \texttt{count} function from the prelude.
886\subsubsection*{\texttt{case} expressions}
888Another way of inspecting intermediate values of \emph{simple} types
889is to use a \texttt{case} expression.
890The following function, for example, splits a string into two at a given character:
893splitAt : Char -> String -> (String, String)
894splitAt c x = case break (== c) x of
895 (x, y) => (x, strTail y)
900\texttt{break} is a library function which breaks a string into a pair of strings
901at the point where the given function returns true. We then deconstruct the
902pair it returns, and remove the first character of the second string.
904A \texttt{case} expression can match several cases, for example, to inspect an
905intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
906looks up an index in a list, returning \texttt{Nothing} if the index is out
907of bounds. We can use this to write \texttt{lookup\_default}, which
908looks up an index and returns a default value if the index is out of bounds:
911lookup_default : Nat -> List a -> a -> a
912lookup_default i xs def = case list_lookup i xs of
919If the index is in bounds, we get the value at that index, otherwise we get
923*usefultypes> lookup_default 2 [3,4,5,6] (-1)
925*usefultypes> lookup_default 4 [3,4,5,6] (-1)
931\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
932of intermediate expressions to avoid the need to write auxiliary functions, and is
933also used internally to implement pattern matching \texttt{let} and lambda bindings.
934It will \emph{only} work if:
937\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
938value of the same type.
939\item The type of the result is ``known''. i.e. the type of the expression can be
940determined \emph{without} type checking the \texttt{case}-expression itself.
943\subsection{Dependent Records}
945\remph{Records} are data types which collect several values (the record's
946\remph{fields}) together. \Idris{} provides syntax for defining records and
947automatically generating field access and update functions. For example, we
948can represent a person's name and age in a record:
951record Person : Type where
952 MkPerson : (name : String) ->
953 (age : Int) -> Person
956fred = MkPerson "Fred" 30
961Record declarations are like \texttt{data} declarations, except that they are
962introduced by the \texttt{record} keyword, and can only have one constructor.
963The names of the binders in the constructor type (\texttt{name} and \texttt{age})
964here are the field names, which we can use to access the field values:
972name : Person -> String
976We can also use the field names to update a record (or, more precisely, produce a
977new record with the given fields updates).
980*record> record { name = "Jim" } fred
981MkPerson "Jim" 30 : Person
982*record> record { name = "Jim", age = 20 } fred
983MkPerson "Jim" 20 : Person
987The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
988the given fields in a record.
990Records, and fields within records, can have dependent types.
991Updates are allowed to change the type of a field,
992provided that the result is well-typed, and the result does not affect the type of
993the record as a whole. For example:
996record Class : Type where
997 ClassInfo : (students : Vect n Person) ->
998 (className : String) ->
1003It is safe to update the \texttt{students} field to a vector of a different length
1004because it will not affect the type of the record:
1007addStudent : Person -> Class -> Class
1008addStudent p c = record { students = p :: students c } c
1012*record> addStudent fred (ClassInfo [] "CS")
1013ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
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