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}:
14\begin{SaveVerbatim}{constprims}
22foo = "Sausage machine"
34An \Idris{} file consists of an optional module declaration (here
35\texttt{module prims}) followed by an optional list of imports (none here,
36however \Idris{} programs can consist of several modules, and the definitions
37in each module each have their own namespace, as we will discuss in Section
38\ref{sect:namespaces}) and a
39collection of declarations and definitions. Each definition must have a type
40declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
41Indentation is significant --- a new declaration begins at the same level
42of indentation as the preceding declaration. Alternatively, declarations
43may be terminated with a semicolon.
45A library module \texttt{prelude} is automatically imported by every \Idris{} program,
46including facilities for IO, arithmetic, data structures and various common
47functions. The prelude defines several arithmetic and comparison operators,
48which we can use at the prompt. Evaluating things at the prompt gives an
49answer, and the type of the answer. For example:
51\begin{SaveVerbatim}{promptprim}
62All of the usual arithmetic and comparison operators are defined for the primitive
63types. They are overloaded using type classes, as we will discuss in Section
64\ref{sec:classes} and can be extended to work on user defined types.
65Boolean expressions can be tested with the \texttt{if...then...else} construct:
67\begin{SaveVerbatim}{ifthenelse}
69*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
75\subsection{Data Types}
77Data types are declared in a similar way to Haskell data types, with a similar
78syntax. Natural numbers and lists, for example, can be declared as follows:
80\begin{SaveVerbatim}{natlist}
82data Nat = O | S Nat -- Natural numbers
83 -- (zero and successor)
84data List a = Nil | (::) a (List a) -- Polymorphic lists
90The above declarations are taken from the standard library. Unary natural
91numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
92the successor of another natural number (\texttt{S k}).
93Lists can either be empty (\texttt{Nil})
94or a value added to the front of another list (\texttt{x :: xs}).
95In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
96such as this can be added using a fixity declaration, as follows:
98\begin{SaveVerbatim}{infixcons}
106Functions, data constructors and type constuctors may all be given infix
107operators as names. They may be used in prefix form if enclosed in brackets,
108e.g. \tDC{(::)}. Infix operators can use any of the symbols:
110\begin{SaveVerbatim}{infixsyms}
117\begin{SaveVerbatim}{argh}
121\subsection{Functions}
123Functions are implemented by pattern matching, again using a similar syntax to
124Haskell. The main difference is that \Idris{} requires type declarations for all
125functions, using a single colon \texttt{:} (rather than
126Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
127defined as follows, again taken from the standard library:
129\begin{SaveVerbatim}{natfns}
132plus : Nat -> Nat -> Nat
134plus (S k) y = S (plus k y)
136-- Unary multiplication
137mult : Nat -> Nat -> Nat
139mult (S k) y = plus y (mult k y)
145The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
146for use by \texttt{Nat}, and are implemented
147using the above functions. Unlike Haskell, there is no restriction on whether
148types and function names must begin with a capital letter or not. Function
149names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
150\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
151all part of the same namespace.
153We can test these functions at the \Idris{} prompt:
155\begin{SaveVerbatim}{fntest}
157Idris> plus (S (S O)) (S (S O))
159Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
160S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
166Like arithmetic operations, integer literals are also overloaded using type classes,
167meaning that we can also test the functions as follows:
169\begin{SaveVerbatim}{fntest}
173Idris> mult 3 (plus 2 2)
174S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
180You may wonder, by the way, why we have unary natural numbers when our
181computers have perfectly good integer arithmetic built in. The reason is
182primarily that unary numbers have a very convenient structure which is easy to
183reason about, and easy to relate to other data structures as we will see later.
184Nevertheless, we do not want this convenience to be at the expense of
185efficiency. Fortunately, \Idris{} knows about the relationship between
186\tTC{Nat} (and similarly structured types) and numbers, so optimises the
187representation and functions such as \tFN{plus} and \tFN{mult}.
189\subsubsection*{\texttt{where} clauses}
191Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,
192to define a function which reverses a list, we can use an auxiliary function which
193accumulates the new, reversed list, and which does not need to be visible globally:
195\begin{SaveVerbatim}{revwhere}
197reverse : List a -> List a
198reverse xs = revAcc [] xs where
199 revAcc : List a -> List a -> List a
201 revAcc acc (x :: xs) = revAcc (x :: acc) xs
207Indentation is significant --- functions in the \texttt{where} block must be indented
208further than the outer function.
211Any names which are visible in the outer scope are also visible in the \texttt{where}
212clause (unless they have been redefined, such as \texttt{xs} here).
213\emph{However}, names which appear in the type are \emph{not} in scope. In particular,
214in the above example, the \texttt{a} in the top level type and the \texttt{a} in the
215auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required
216behaviour, the \texttt{a} can be brought into scope as follows:
218\begin{SaveVerbatim}{revwhereb}
220reverse : List a -> List a
221reverse {a} xs = revAcc [] xs where
222 revAcc : List a -> List a -> List a
229As well as functions, \texttt{where} blocks can include local data
230declarations, such as the following where \texttt{MyLT} is not accessible outside
231the definition of \texttt{foo}:
233\begin{SaveVerbatim}{wheredata}
243 isLT = if x < 20 then Yes else No
248\subsection{Dependent Types}
250\subsubsection{Vectors}
252A standard example of a dependent type is the type of ``lists with length'',
253conventionally called vectors in the dependent type literature. In \Idris{},
254we declare vectors as follows:
256\begin{SaveVerbatim}{vect}
258data Vect : Set -> Nat -> Set where
260 (::) : a -> Vect a k -> Vect a (S k)
266Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
267name overloading such as this is accepted by \Idris{}, provided that the names
268are declared in different namespaces (in practice, normally in different modules).
269Ambiguous constructor names can normally be resolved from context.
271This declares a family of types, and so the form of the declaration is rather
272different from the simple type declarations above. We explicitly state the type
273of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an
274argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}
275is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
276constructor targets a different part of the family of types. \tDC{Nil} can only
277be used to construct vectors with zero length, and \tDC{::} to construct
278vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element
279of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})
280combine to make a vector of length \texttt{S k}.
282We can define functions on dependent types such as \tTC{Vect} in the same way
283as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
284The type of a function over \tTC{Vect} will describe what happens to the
285lengths of the vectors involved. For example, \tFN{++}, defined in the
286library, appends two \tTC{Vect}s:
288\begin{SaveVerbatim}{vapp}
290(++) : Vect A n -> Vect A m -> Vect A (n + m)
292(++) (x :: xs) ys = x :: xs ++ ys
298The type of \tFN{(++)} states that the resulting vector's length will be the sum of
299the input lengths. If we get the definition wrong in such a way that this does
300not hold, \Idris{} will not accept the definition. For example:
302\begin{SaveVerbatim}{vapperr}
304(++) : Vect a n -> Vect a m -> Vect a (n + m)
306(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
311\begin{SaveVerbatim}{vapperrmsg}
313$ idris vbroken.idr --check
314vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
320\begin{SaveVerbatim}{bleh}
326This error message suggests that there is a length mismatch between two vectors
327--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
328of length \texttt{(S (k + k))}.
329Note that the terms in the error message have been \emph{normalised}, so in
330particular \texttt{n + m} has been reduced to \texttt{plus n m}.
332\subsubsection{The Finite Sets}
334Finite sets, as the name suggests, are sets with a finite number of elements.
335They are declared as follows (again, in the prelude):
337\begin{SaveVerbatim}{findecl}
339data Fin : Nat -> Set where
341 fS : Fin k -> Fin (S k)
347\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
349\texttt{n+1}th element of a finite set with \texttt{S k} elements.
350\tTC{Fin} is indexed by a \tTC{Nat}, which
351represents the number of elements in the set. Obviously we can't construct an
352element of an empty set, so neither constructor targets \texttt{Fin O}.
354A useful application of the \tTC{Fin} family is to represent bounded
355natural numbers. Since the first \tTC{n} natural numbers form a finite
356set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural
357numbers bounded by \tTC{n}.
359For example, the following function which looks up an element in a \tTC{Vect},
360by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
362\begin{SaveVerbatim}{vindex}
364index : Fin n -> Vect a n -> a
365index fO (x :: xs) = x
366index (fS k) (x :: xs) = index k xs
372This function looks up a value at a given location in a vector. The location is
373bounded by the length of the vector (\texttt{n} in each case), so there is no
374need for a run-time bounds check. The type checker guarantees that the location
375is no larger than the length of the vector.
377Note also that there is no case for \texttt{Nil} here. This is because it is
378impossible. Since there is no element of \texttt{Fin O}, and the location is a
379\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
380look up an element in an empty vector would give a compile time type error,
381since it would force \texttt{n} to be \tDC{O}.
383\subsubsection{Implicit Arguments}
385Let us take a closer look at the type of \texttt{index}:
387\begin{SaveVerbatim}{vindexty}
389index : Fin n -> Vect a n -> a
395It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
396with \texttt{n} elements of type \texttt{a}. But there are also two names,
397\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
398arguments to \texttt{index}. We could also write the type of \texttt{index} as:
400\begin{SaveVerbatim}{vindeximpty}
402index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
408Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
409not given in applications of \texttt{index}; their values can be inferred from
410the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name
411with a \remph{lower case initial letter} which
412appears as a parameter or index in a type declaration, but which is otherwise
413free, will be automatically bound as an implicit argument. Implicit arguments
414can still be given explicitly in applications, using \texttt{\{a=value\}} and
415\texttt{\{n=value\}}, for example:
417\begin{SaveVerbatim}{vindexexp}
419index {a=Int} {n=2} fO (2 :: 3 :: Nil)
425In fact, any argument, implicit or explicit, may be given a name. We could have
426declared the type of \texttt{index} as:
428\begin{SaveVerbatim}{vindexn}
430index : (i:Fin n) -> (xs:Vect a n) -> a
436It is a matter of taste whether you want to do this --- sometimes it can help
437document a function by making the purpose of an argument more clear.
439\subsubsection{``\texttt{using}'' notation}
441Sometimes it is necessary to provide types of implicit arguments where
442the type checker can not work them out itself. This can happen if there is a
443dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
444before being used --- or if an implicit argument has a complex type. For example,
445we will need to state the types of the implicit arguments in the following
446definition, which defines a predicate on vectors:
448\begin{SaveVerbatim}{elem}
450data Elem : a -> Vect a n -> Set where
451 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)
452 there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)
458An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
459\texttt{xs}. We can construct
460such a predicate if the required element is \texttt{here}, at the head of the vector,
461or \texttt{there}, in the tail of the vector. For example:
463\begin{SaveVerbatim}{testelem}
466testVec = 3 :: 4 :: 5 :: 6 :: Nil
468inVect : Elem 5 testVec
469inVect = there (there here)
475If the same implicit arguments are being used a lot, it can make a definition
476difficult to read. To avoid this problem, a \texttt{using} block gives the types and
477ordering of any implicit arguments which can appear within the block:
479\begin{SaveVerbatim}{elemusing}
481using (x:a, y:a, xs:Vect a n)
482 data Elem : a -> Vect a n -> Set where
483 here : Elem x (x :: xs)
484 there : Elem x xs -> Elem x (y :: xs)
491Computer programs are of little use if they do not interact with the user or
492the system in some way. The difficulty in a pure language such as \Idris{} ---
493that is, a language where expressions do not have side-effects --- is that I/O
494is inherently side-effecting. Therefore in \Idris{}, such interactions are
495encapsulated in the type \texttt{IO}:
497\begin{SaveVerbatim}{ioty}
499data IO a -- IO operation returning a value of type a
505We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
506the I/O operations to be executed are, rather than how to execute them. The
507resulting operations are executed externally,
508by the run-time system. We've already seen one IO
511\begin{SaveVerbatim}{main}
514main = putStrLn "Hello world"
520The type of \texttt{putStrLn} explains that it takes a string, and returns an
521element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
522outputs a string without a newline:
524\begin{SaveVerbatim}{putstr}
526putStrLn : String -> IO ()
527putStr : String -> IO ()
531We can also read strings from user input:
533\begin{SaveVerbatim}{getline}
541A number of other I/O operations are defined in the prelude, for example for reading and
542writing files, including:
544\begin{SaveVerbatim}{fileops}
547data Mode = Read | Write | ReadWrite
549openFile : String -> Mode -> IO File
550closeFile : File -> IO ()
552fread : File -> IO String
553fwrite : File -> String -> IO ()
554feof : File -> IO Bool
556readFile : String -> IO String
561\subsection{``\texttt{do}'' notation}
565I/O programs will typically need to sequence actions, feeding the output of one
566computation into the input of the next. \texttt{IO} is an abstract type, however, so we
567can't access the result of a computation directly. Instead, we sequence
568operations with \texttt{do} notation:
570\begin{SaveVerbatim}{greet}
573greet = do putStr "What is your name? "
575 putStrLn ("Hello " ++ name)
581The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
583puts the result, of type \texttt{a} into the variable \texttt{x}.
584In this case, \texttt{getLine} returns an \texttt{IO String},
585so \texttt{name} has type \texttt{String}. Indentation is significant --- each
586statement in the do block must begin in the same column.
587The \texttt{return} operation allows us to inject a value directly into an IO
590\begin{SaveVerbatim}{return}
598As we will see later, \texttt{do} notation is more general than this, and can be
601\subsection{Useful Data Types}
603\Idris{} includes a number of useful data types and library functions (see the
604\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
605functions described here are imported automatically by every \Idris{} program, as
606part of \texttt{prelude.idr}.
608\subsubsection{\texttt{List} and \texttt{Vect}}
610We have already seen the \texttt{List} and \texttt{Vect} data types:
612\begin{SaveVerbatim}{listvec}
614data List a = Nil | (::) a (List a)
616data Vect : Set -> Nat -> Set where
618 (::) : a -> Vect a k -> Vect a (S k)
624Note that the constructor names are the same for each --- constructor names (in
625fact, names in general) can be overloaded, provided that they are declared in
626different namespaces (see Section \ref{sect:namespaces}), and will typically be
627resolved according to their type. As syntactic sugar, any type with the constructor
628names \texttt{Nil} and \texttt{::} can be written in list form. For example:
631\item \texttt{[]} means \texttt{Nil}
632\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
636The library also defines a number of functions for manipulating these types.
637\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
638and applies a function to every element of the list or vector.
640\begin{SaveVerbatim}{map}
642map : (a -> b) -> List a -> List b
644map f (x :: xs) = f x :: map f xs
646map : (a -> b) -> Vect a n -> Vect b n
648map f (x :: xs) = f x :: map f xs
654For example, to double every element in a vector of integers:
656\begin{SaveVerbatim}{dvect}
659intVec = [1, 2, 3, 4, 5]
668You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
670\begin{SaveVerbatim}{rundvect}
672*usefultypes> show (map double intVec)
673"[2, 4, 6, 8, 10]" : String
679For more details of the functions available on \texttt{List} and \texttt{Vect},
680look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
681Functions include filtering, appending, reversing, and so on. Also remember
682that \Idris{} is still in development, so if you don't see the function you
683need, please feel free to add it and submit a patch!
685\subsubsection*{Aside: Anonymous functions and operator sections}
687There are actually neater ways to write the above expression. One way would be
688to use an anonymous function:
690\begin{SaveVerbatim}{lam1}
692*usefultypes> show (map (\x => x * 2) intVec)
693"[2, 4, 6, 8, 10]" : String
699The notation \texttt{$\backslash$x => val} constructs an anonymous function
700which takes one argument, \texttt{x} and returns the expression \texttt{val}.
701Anonymous functions may take several arguments, separated by commas, e.g.
702\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
703types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
704e.g. \texttt{$\backslash$ (x, y) => x + y}.
705We could also use an operator section:
707\begin{SaveVerbatim}{sec1}
709*usefultypes> show (map (* 2) intVec)
710"[2, 4, 6, 8, 10]" : String
716\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
717\texttt{$\backslash$x => x * 2}.
718Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
722\texttt{Maybe} describes an optional value. Either there is a value of the given type,
725\begin{SaveVerbatim}{maybe}
727data Maybe a = Just a | Nothing
733\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
734looking something up in a \texttt{List} (rather than a vector) may result in an out of
737\begin{SaveVerbatim}{lookuplist}
739list_lookup : Nat -> List a -> Maybe a
740list_lookup _ Nil = Nothing
741list_lookup O (x :: xs) = Just x
742list_lookup (S k) (x :: xs) = list_lookup k xs
748The \texttt{maybe} function is used to process values of type \texttt{Maybe},
749either by applying a function to the value, if there is one, or by providing a default value:
751\begin{SaveVerbatim}{maybefn}
753maybe : Maybe a -> |(default:b) -> (a -> b) -> b
759The vertical bar $\mid$ before the default value is a laziness annotation. Normally
760expressions are evaluated before being passed to a function. This is typically
761the most efficient behaviour. However, in this case, the default value might
762not be used and if it is a large expression, evaluating it will be wasteful.
763The $\mid$ annotation tells the compiler not to evaluate the argument until it is
766\subsubsection{Tuples and Dependent Pairs}
768Values can be paired with the following built-in data type:
770\begin{SaveVerbatim}{mkpair}
772data Pair a b = MkPair a b
778As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
779means either \texttt{Pair a b} or \texttt{MkPair a b}.
780Tuples can contain an arbitrary number of values, represented as nested pairs:
782\begin{SaveVerbatim}{tuple}
787jim : (String, Int, String)
788jim = ("Jim", 25, "Cambridge")
793\subsubsection*{Dependent Pairs}
795Dependent pairs allow the type of the second element of a pair to depend on
796the value of the first element:
798\begin{SaveVerbatim}{sigma}
800data Exists : (A : Set) -> (P : A -> Set) -> Set where
801 Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P
807Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
808A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}
809constructs a value of this type. For example, we can pair a number with a
810\texttt{Vect} of a particular length.
812\begin{SaveVerbatim}{dvec}
814vec : (n : Nat ** Vect Int n)
821The type checker could of course infer the value of the first element from the
822length of the vector. We can write an underscore \texttt{\_} in place of values which we
823expect the type checker to fill in, so the above definition could also be
826\begin{SaveVerbatim}{dvec1}
828vec : (n : Nat ** Vect Int n)
835We might also prefer to omit the type of the first element of the pair, since,
836again, it can be inferred:
838\begin{SaveVerbatim}{dvec2}
840vec : (n ** Vect Int n)
847One use for dependent pairs is to return values of dependent types where the
848index is not necessarily known in advance. For example, if we filter elements
849out of a \texttt{Vect} according to some predicate, we will not know in advance what the
850length of the resulting vector will be:
852\begin{SaveVerbatim}{vfilter}
854filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
860If the \texttt{Vect} is empty, the result is easy:
862\begin{SaveVerbatim}{vfilternil}
864filter p Nil = (_ , [])
870In the \texttt{::} case, we need to inspect the result of a recursive call to
872extract the length and the vector from the result. To do this, we use \texttt{with}
873notation, which allows pattern matching on intermediate values:
875\begin{SaveVerbatim}{vfiltercons}
877filter p (x :: xs) with (filter p xs)
878 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
884We will see more on \texttt{with} notation later.
886\subsection{\texttt{so}}
888The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
891\begin{SaveVerbatim}{sotype}
893data so : Bool -> Set where
900This is most useful for providing a static guarantee that a dynamic check has been made.
901For example, we might provide a safe interface to a function which draws a pixel
902on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
903the point \texttt{(x,y)} is within the bounds of a 640x480 window:
905\begin{SaveVerbatim}{soexample}
907inBounds : Int -> Int -> Bool
908inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
910drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
911drawPoint x y oh = unsafeDrawPoint x y
916\subsection{More Expressions}
918\subsubsection*{\texttt{let} bindings}
920Intermediate values can be calculated using \texttt{let} bindings:
922\begin{SaveVerbatim}{letb}
924mirror : List a -> List a
925mirror xs = let xs' = rev xs in
932We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
933fields from a record as follows, as well as by pattern matching at the top level:
935\begin{SaveVerbatim}{letp}
937data Person = MkPerson String Int
939showPerson : Person -> String
940showPerson p = let MkPerson name age = p in
941 name ++ " is " ++ show age ++ " years old"
946\subsubsection*{List comprehensions}
950\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
951building lists. The general form is:
953\begin{SaveVerbatim}{listcomp}
955[ expression | qualifiers ]
961This generates the list of values produced by evaluating the
962\texttt{expression}, according to the conditions given by the comma separated
963\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
966\begin{SaveVerbatim}{triples}
968pythag : Int -> List (Int, Int, Int)
969pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
976The \texttt{[a..b]} notation is another shorthand which builds a list of
977numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]}
978builds a list of numbers between \texttt{a} and \texttt{c} with the increment
979specified by the difference between \texttt{a} and \texttt{c}. This works for
980any numeric type, using the \texttt{count} function from the prelude.
982\subsubsection*{\texttt{case} expressions}
984Another way of inspecting intermediate values of \emph{simple} types
985is to use a \texttt{case} expression.
986The following function, for example, splits a string into two at a given character:
988\begin{SaveVerbatim}{split}
990splitAt : Char -> String -> (String, String)
991splitAt c x = case break (== c) x of
992 (x, y) => (x, strTail y)
998\texttt{break} is a library function which breaks a string into a pair of strings
999at the point where the given function returns true. We then deconstruct the
1000pair it returns, and remove the first character of the second string.
1002A \texttt{case} expression can match several cases, for example, to inspect an
1003intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
1004looks up an index in a list, returning \texttt{Nothing} if the index is out
1005of bounds. We can use this to write \texttt{lookup\_default}, which
1006looks up an index and returns a default value if the index is out of bounds:
1008\begin{SaveVerbatim}{listlookup}
1010lookup_default : Nat -> List a -> a -> a
1011lookup_default i xs def = case list_lookup i xs of
1019If the index is in bounds, we get the value at that index, otherwise we get
1022\begin{SaveVerbatim}{deftest}
1024*usefultypes> lookup_default 2 [3,4,5,6] (-1)
1026*usefultypes> lookup_default 4 [3,4,5,6] (-1)
1033\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
1034of intermediate expressions to avoid the need to write auxiliary functions, and is
1035also used internally to implement pattern matching \texttt{let} and lambda bindings.
1036It will \emph{only} work if:
1039\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
1040value of the same type.
1041\item The type of the result is ``known''. i.e. the type of the expression can be
1042determined \emph{without} type checking the \texttt{case}-expression itself.
1045\subsection{Dependent Records}
1047\remph{Records} are data types which collect several values (the record's
1048\remph{fields}) together. \Idris{} provides syntax for defining records and
1049automatically generating field access and update functions. For example, we
1050can represent a person's name and age in a record:
1052\begin{SaveVerbatim}{recsimpl}
1054record Person : Set where
1055 MkPerson : (name : String) ->
1056 (age : Int) -> Person
1059fred = MkPerson "Fred" 30
1065Record declarations are like \texttt{data} declarations, except that they are
1066introduced by the \texttt{record} keyword, and can only have one constructor.
1067The names of the binders in the constructor type (\texttt{name} and \texttt{age})
1068here are the field names, which we can use to access the field values:
1070\begin{SaveVerbatim}{recaccess}
1077name : Person -> String
1083We can also use the field names to update a record (or, more precisely, produce a
1084new record with the given fields updates).
1086\begin{SaveVerbatim}{recupdate}
1088*record> record { name = "Jim" } fred
1089MkPerson "Jim" 30 : Person
1090*record> record { name = "Jim", age = 20 } fred
1091MkPerson "Jim" 20 : Person
1097The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
1098the given fields in a record.
1100Records, and fields within records, can have dependent types.
1101Updates are allowed to change the type of a field,
1102provided that the result is well-typed, and the result does not affect the type of
1103the record as a whole. For example:
1105\begin{SaveVerbatim}{deprec}
1107record Class : Set where
1108 ClassInfo : (students : Vect Person n) ->
1109 (className : String) ->
1116It is safe to update the \texttt{students} field to a vector of a different length
1117because it will not affect the type of the record:
1119\begin{SaveVerbatim}{addstu}
1121addStudent : Person -> Class -> Class
1122addStudent p c = record { students = p :: students c } c
1124*record> addStudent fred (ClassInfo [] "CS")
1125ClassInfo (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