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. The order of definitions is
40significant --- functions and data types must be defined before use.
41Each definition must have a type
42declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
43Indentation is significant --- a new declaration begins at the same level
44of indentation as the preceding declaration. Alternatively, declarations
45may be terminated with a semicolon.
47A library module \texttt{prelude} is automatically imported by every \Idris{} program,
48including facilities for IO, arithmetic, data structures and various common
49functions. The prelude defines several arithmetic and comparison operators,
50which we can use at the prompt. Evaluating things at the prompt gives an
51answer, and the type of the answer. For example:
53\begin{SaveVerbatim}{promptprim}
64All of the usual arithmetic and comparison operators are defined for the primitive
65types. They are overloaded using type classes, as we will discuss in Section
66\ref{sec:classes} and can be extended to work on user defined types.
67Boolean expressions can be tested with the \texttt{if...then...else} construct:
69\begin{SaveVerbatim}{ifthenelse}
71*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
77\subsection{Data Types}
79Data types are declared in a similar way to Haskell data types, with a similar
80syntax. Natural numbers and lists, for example, can be declared as follows:
82\begin{SaveVerbatim}{natlist}
84data Nat = O | S Nat -- Natural numbers
85 -- (zero and successor)
86data List a = Nil | (::) a (List a) -- Polymorphic lists
92The above declarations are taken from the standard library. Unary natural
93numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
94the successor of another natural number (\texttt{S k}).
95Lists can either be empty (\texttt{Nil})
96or a value added to the front of another list (\texttt{x :: xs}).
97In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
98such as this can be added using a fixity declaration, as follows:
100\begin{SaveVerbatim}{infixcons}
108Functions, data constructors and type constuctors may all be given infix
109operators as names. They may be used in prefix form if enclosed in brackets,
110e.g. \tDC{(::)}. Infix operators can use any of the symbols:
112\begin{SaveVerbatim}{infixsyms}
119\begin{SaveVerbatim}{argh}
123\subsection{Functions}
125Functions are implemented by pattern matching, again using a similar syntax to
126Haskell. The main difference is that \Idris{} requires type declarations for all
127functions, using a single colon \texttt{:} (rather than
128Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
129defined as follows, again taken from the standard library:
131\begin{SaveVerbatim}{natfns}
134plus : Nat -> Nat -> Nat
136plus (S k) y = S (plus k y)
138-- Unary multiplication
139mult : Nat -> Nat -> Nat
141mult (S k) y = plus y (mult k y)
147The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
148for use by \texttt{Nat}, and are implemented
149using the above functions. Unlike Haskell, there is no restriction on whether
150types and function names must begin with a capital letter or not. Function
151names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
152\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
153all part of the same namespace.
155We can test these functions at the \Idris{} prompt:
157\begin{SaveVerbatim}{fntest}
159Idris> plus (S (S O)) (S (S O))
161Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
162S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
168Like arithmetic operations, integer literals are also overloaded using type classes,
169meaning that we can also test the functions as follows:
171\begin{SaveVerbatim}{fntest}
175Idris> mult 3 (plus 2 2)
176S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
182You may wonder, by the way, why we have unary natural numbers when our
183computers have perfectly good integer arithmetic built in. The reason is
184primarily that unary numbers have a very convenient structure which is easy to
185reason about, and easy to relate to other data structures as we will see later.
186Nevertheless, we do not want this convenience to be at the expense of
187efficiency. Fortunately, \Idris{} knows about the relationship between
188\tTC{Nat} (and similarly structured types) and numbers, so optimises the
189representation and functions such as \tFN{plus} and \tFN{mult}.
191\subsubsection*{\texttt{where} clauses}
193Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,
194to define a function which reverses a list, we can use an auxiliary function which
195accumulates the new, reversed list, and which does not need to be visible globally:
197\begin{SaveVerbatim}{revwhere}
199reverse : List a -> List a
200reverse xs = revAcc [] xs where
201 revAcc : List a -> List a -> List a
203 revAcc acc (x :: xs) = revAcc (x :: acc) xs
209Indentation is significant --- functions in the \texttt{where} block must be indented
210further than the outer function.
213Any names which are visible in the outer scope are also visible in the
214\texttt{where} clause (unless they have been redefined, such as \texttt{xs}
215here). A name which appears only in the type will be in scope in the
216\texttt{where} clause if it is a \remph{parameter} to one of the types,
217i.e. it is fixed across the entire structure.
219As well as functions, \texttt{where} blocks can include local data
220declarations, such as the following where \texttt{MyLT} is not accessible outside
221the definition of \texttt{foo}:
223\begin{SaveVerbatim}{wheredata}
233 isLT = if x < 20 then Yes else No
239In general, functions defined in a \texttt{where} clause need a type declaration
240just like any top level function. However, the type declaration for
241a function \texttt{f} \remph{can} be omitted if:
244\item \texttt{f} appears in the right hand side of the top level definition
245\item The type of \texttt{f} can be completely determined from its first
250So, for example, the following definitions are legal:
252\begin{SaveVerbatim}{whereinfer}
256even (S k) = odd k where
260test : Num a => List a
261test = [c 1, c 2, d 3]
263 d y = c (y + 1 + z y)
270\subsection{Dependent Types}
272\subsubsection{Vectors}
274A standard example of a dependent type is the type of ``lists with length'',
275conventionally called vectors in the dependent type literature. In \Idris{},
276we declare vectors as follows:
278\begin{SaveVerbatim}{vect}
280data Vect : Type -> Nat -> Type where
282 (::) : a -> Vect a k -> Vect a (S k)
288Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
289name overloading such as this is accepted by \Idris{}, provided that the names
290are declared in different namespaces (in practice, normally in different modules).
291Ambiguous constructor names can normally be resolved from context.
293This declares a family of types, and so the form of the declaration is rather
294different from the simple type declarations above. We explicitly state the type
295of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an
296argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}
297is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
298constructor targets a different part of the family of types. \tDC{Nil} can only
299be used to construct vectors with zero length, and \tDC{::} to construct
300vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element
301of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})
302combine to make a vector of length \texttt{S k}.
304We can define functions on dependent types such as \tTC{Vect} in the same way
305as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
306The type of a function over \tTC{Vect} will describe what happens to the
307lengths of the vectors involved. For example, \tFN{++}, defined in the
308library, appends two \tTC{Vect}s:
310\begin{SaveVerbatim}{vapp}
312(++) : Vect A n -> Vect A m -> Vect A (n + m)
314(++) (x :: xs) ys = x :: xs ++ ys
320The type of \tFN{(++)} states that the resulting vector's length will be the sum of
321the input lengths. If we get the definition wrong in such a way that this does
322not hold, \Idris{} will not accept the definition. For example:
324\begin{SaveVerbatim}{vapperr}
326(++) : Vect a n -> Vect a m -> Vect a (n + m)
328(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
333\begin{SaveVerbatim}{vapperrmsg}
335$ idris vbroken.idr --check
336vbroken.idr:3:Can't unify Vect a n with Vect a m
342\begin{SaveVerbatim}{bleh}
348This error message suggests that there is a length mismatch between two vectors
349--- we needed a vector of length \texttt{m}, but provided a vector
351%Note that the terms in the error message have been \emph{normalised}, so in
352%particular \texttt{n + m} has been reduced to \texttt{plus n m}.
354\subsubsection{The Finite Sets}
356Finite sets, as the name suggests, are sets with a finite number of elements.
357They are declared as follows (again, in the prelude):
359\begin{SaveVerbatim}{findecl}
361data Fin : Nat -> Type where
363 fS : Fin k -> Fin (S k)
369\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
371\texttt{n+1}th element of a finite set with \texttt{S k} elements.
372\tTC{Fin} is indexed by a \tTC{Nat}, which
373represents the number of elements in the set. Obviously we can't construct an
374element of an empty set, so neither constructor targets \texttt{Fin O}.
376A useful application of the \tTC{Fin} family is to represent bounded
377natural numbers. Since the first \tTC{n} natural numbers form a finite
378set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural
379numbers bounded by \tTC{n}.
381For example, the following function which looks up an element in a \tTC{Vect},
382by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
384\begin{SaveVerbatim}{vindex}
386index : Fin n -> Vect a n -> a
387index fO (x :: xs) = x
388index (fS k) (x :: xs) = index k xs
394This function looks up a value at a given location in a vector. The location is
395bounded by the length of the vector (\texttt{n} in each case), so there is no
396need for a run-time bounds check. The type checker guarantees that the location
397is no larger than the length of the vector.
399Note also that there is no case for \texttt{Nil} here. This is because it is
400impossible. Since there is no element of \texttt{Fin O}, and the location is a
401\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
402look up an element in an empty vector would give a compile time type error,
403since it would force \texttt{n} to be \tDC{O}.
405\subsubsection{Implicit Arguments}
407Let us take a closer look at the type of \texttt{index}:
409\begin{SaveVerbatim}{vindexty}
411index : Fin n -> Vect a n -> a
417It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
418with \texttt{n} elements of type \texttt{a}. But there are also two names,
419\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
420arguments to \texttt{index}. We could also write the type of \texttt{index} as:
422\begin{SaveVerbatim}{vindeximpty}
424index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a
430Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
431not given in applications of \texttt{index}; their values can be inferred from
432the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name
433with a \remph{lower case initial letter} which
434appears as a parameter or index in a type declaration, but which is otherwise
435free, will be automatically bound as an implicit argument. Implicit arguments
436can still be given explicitly in applications, using \texttt{\{a=value\}} and
437\texttt{\{n=value\}}, for example:
439\begin{SaveVerbatim}{vindexexp}
441index {a=Int} {n=2} fO (2 :: 3 :: Nil)
447In fact, any argument, implicit or explicit, may be given a name. We could have
448declared the type of \texttt{index} as:
450\begin{SaveVerbatim}{vindexn}
452index : (i:Fin n) -> (xs:Vect a n) -> a
458It is a matter of taste whether you want to do this --- sometimes it can help
459document a function by making the purpose of an argument more clear.
461\subsubsection{``\texttt{using}'' notation}
463Sometimes it is necessary to provide types of implicit arguments where
464the type checker can not work them out itself. This can happen if there is a
465dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
466before being used --- or if an implicit argument has a complex type. For example,
467we will need to state the types of the implicit arguments in the following
468definition, which defines a predicate on vectors:
470\begin{SaveVerbatim}{elem}
472data Elem : a -> Vect a n -> Type where
473 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)
474 there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)
480An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
481\texttt{xs}. We can construct
482such a predicate if the required element is \texttt{here}, at the head of the vector,
483or \texttt{there}, in the tail of the vector. For example:
485\begin{SaveVerbatim}{testelem}
488testVec = 3 :: 4 :: 5 :: 6 :: Nil
490inVect : Elem 5 testVec
491inVect = there (there here)
497If the same implicit arguments are being used a lot, it can make a definition
498difficult to read. To avoid this problem, a \texttt{using} block gives the types and
499ordering of any implicit arguments which can appear within the block:
501\begin{SaveVerbatim}{elemusing}
503using (x:a, y:a, xs:Vect a n)
504 data Elem : a -> Vect a n -> Type where
505 here : Elem x (x :: xs)
506 there : Elem x xs -> Elem x (y :: xs)
511\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
513In general, functions and data types must be defined before use, since
514dependent types allow functions to appear as part of types, and their
515reduction behaviour to affect type checking. However, this
516restriction can be relaxed by using a \texttt{mutual} block, which allows
517data types and functions to be defined simultaneously:
519\begin{SaveVerbatim}{mutual}
534In a \texttt{mutual} block, first all of the type declarations are added,
535then the function bodies. As a result, none of the function types can depend
536on the reduction behaviour of any of the functions in the block.
540Computer programs are of little use if they do not interact with the user or
541the system in some way. The difficulty in a pure language such as \Idris{} ---
542that is, a language where expressions do not have side-effects --- is that I/O
543is inherently side-effecting. Therefore in \Idris{}, such interactions are
544encapsulated in the type \texttt{IO}:
546\begin{SaveVerbatim}{ioty}
548data IO a -- IO operation returning a value of type a
554We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
555the I/O operations to be executed are, rather than how to execute them. The
556resulting operations are executed externally,
557by the run-time system. We've already seen one IO
560\begin{SaveVerbatim}{main}
563main = putStrLn "Hello world"
569The type of \texttt{putStrLn} explains that it takes a string, and returns an
570element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
571outputs a string without a newline:
573\begin{SaveVerbatim}{putstr}
575putStrLn : String -> IO ()
576putStr : String -> IO ()
580We can also read strings from user input:
582\begin{SaveVerbatim}{getline}
590A number of other I/O operations are defined in the prelude, for example for reading and
591writing files, including:
593\begin{SaveVerbatim}{fileops}
596data Mode = Read | Write | ReadWrite
598openFile : String -> Mode -> IO File
599closeFile : File -> IO ()
601fread : File -> IO String
602fwrite : File -> String -> IO ()
603feof : File -> IO Bool
605readFile : String -> IO String
610\subsection{``\texttt{do}'' notation}
614I/O programs will typically need to sequence actions, feeding the output of one
615computation into the input of the next. \texttt{IO} is an abstract type, however, so we
616can't access the result of a computation directly. Instead, we sequence
617operations with \texttt{do} notation:
619\begin{SaveVerbatim}{greet}
622greet = do putStr "What is your name? "
624 putStrLn ("Hello " ++ name)
630The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
632puts the result, of type \texttt{a} into the variable \texttt{x}.
633In this case, \texttt{getLine} returns an \texttt{IO String},
634so \texttt{name} has type \texttt{String}. Indentation is significant --- each
635statement in the do block must begin in the same column.
636The \texttt{return} operation allows us to inject a value directly into an IO
639\begin{SaveVerbatim}{return}
647As we will see later, \texttt{do} notation is more general than this, and can be
650\subsection{Useful Data Types}
652\Idris{} includes a number of useful data types and library functions (see the
653\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
654functions described here are imported automatically by every \Idris{} program, as
655part of \texttt{prelude.idr}.
657\subsubsection{\texttt{List} and \texttt{Vect}}
659We have already seen the \texttt{List} and \texttt{Vect} data types:
661\begin{SaveVerbatim}{listvec}
663data List a = Nil | (::) a (List a)
665data Vect : Type -> Nat -> Type where
667 (::) : a -> Vect a k -> Vect a (S k)
673Note that the constructor names are the same for each --- constructor names (in
674fact, names in general) can be overloaded, provided that they are declared in
675different namespaces (see Section \ref{sect:namespaces}), and will typically be
676resolved according to their type. As syntactic sugar, any type with the constructor
677names \texttt{Nil} and \texttt{::} can be written in list form. For example:
680\item \texttt{[]} means \texttt{Nil}
681\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
685The library also defines a number of functions for manipulating these types.
686\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
687and applies a function to every element of the list or vector.
689\begin{SaveVerbatim}{map}
691map : (a -> b) -> List a -> List b
693map f (x :: xs) = f x :: map f xs
695map : (a -> b) -> Vect a n -> Vect b n
697map f (x :: xs) = f x :: map f xs
703For example, to double every element in a vector of integers:
705\begin{SaveVerbatim}{dvect}
708intVec = [1, 2, 3, 4, 5]
717You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
719\begin{SaveVerbatim}{rundvect}
721*usefultypes> show (map double intVec)
722"[2, 4, 6, 8, 10]" : String
728For more details of the functions available on \texttt{List} and \texttt{Vect},
729look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
730Functions include filtering, appending, reversing, and so on. Also remember
731that \Idris{} is still in development, so if you don't see the function you
732need, please feel free to add it and submit a patch!
734\subsubsection*{Aside: Anonymous functions and operator sections}
736There are actually neater ways to write the above expression. One way would be
737to use an anonymous function:
739\begin{SaveVerbatim}{lam1}
741*usefultypes> show (map (\x => x * 2) intVec)
742"[2, 4, 6, 8, 10]" : String
748The notation \texttt{$\backslash$x => val} constructs an anonymous function
749which takes one argument, \texttt{x} and returns the expression \texttt{val}.
750Anonymous functions may take several arguments, separated by commas, e.g.
751\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
752types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
753e.g. \texttt{$\backslash$ (x, y) => x + y}.
754We could also use an operator section:
756\begin{SaveVerbatim}{sec1}
758*usefultypes> show (map (* 2) intVec)
759"[2, 4, 6, 8, 10]" : String
765\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
766\texttt{$\backslash$x => x * 2}.
767Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
771\texttt{Maybe} describes an optional value. Either there is a value of the given type,
774\begin{SaveVerbatim}{maybe}
776data Maybe a = Just a | Nothing
782\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
783looking something up in a \texttt{List} (rather than a vector) may result in an out of
786\begin{SaveVerbatim}{lookuplist}
788list_lookup : Nat -> List a -> Maybe a
789list_lookup _ Nil = Nothing
790list_lookup O (x :: xs) = Just x
791list_lookup (S k) (x :: xs) = list_lookup k xs
797The \texttt{maybe} function is used to process values of type \texttt{Maybe},
798either by applying a function to the value, if there is one, or by providing a default value:
800\begin{SaveVerbatim}{maybefn}
802maybe : Maybe a -> |(default:b) -> (a -> b) -> b
808The vertical bar $\mid$ before the default value is a laziness annotation. Normally
809expressions are evaluated before being passed to a function. This is typically
810the most efficient behaviour. However, in this case, the default value might
811not be used and if it is a large expression, evaluating it will be wasteful.
812The $\mid$ annotation tells the compiler not to evaluate the argument until it is
815\subsubsection{Tuples and Dependent Pairs}
817Values can be paired with the following built-in data type:
819\begin{SaveVerbatim}{mkpair}
821data Pair a b = MkPair a b
827As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
828means either \texttt{Pair a b} or \texttt{MkPair a b}.
829Tuples can contain an arbitrary number of values, represented as nested pairs:
831\begin{SaveVerbatim}{tuple}
836jim : (String, Int, String)
837jim = ("Jim", 25, "Cambridge")
842\subsubsection*{Dependent Pairs}
844Dependent pairs allow the type of the second element of a pair to depend on
845the value of the first element:
847\begin{SaveVerbatim}{sigma}
849data Exists : (A : Type) -> (P : A -> Type) -> Type where
850 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
856Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
857A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}
858constructs a value of this type. For example, we can pair a number with a
859\texttt{Vect} of a particular length.
861\begin{SaveVerbatim}{dvec}
863vec : (n : Nat ** Vect Int n)
870The type checker could of course infer the value of the first element from the
871length of the vector. We can write an underscore \texttt{\_} in place of values which we
872expect the type checker to fill in, so the above definition could also be
875\begin{SaveVerbatim}{dvec1}
877vec : (n : Nat ** Vect Int n)
884We might also prefer to omit the type of the first element of the pair, since,
885again, it can be inferred:
887\begin{SaveVerbatim}{dvec2}
889vec : (n ** Vect Int n)
896One use for dependent pairs is to return values of dependent types where the
897index is not necessarily known in advance. For example, if we filter elements
898out of a \texttt{Vect} according to some predicate, we will not know in advance what the
899length of the resulting vector will be:
901\begin{SaveVerbatim}{vfilter}
903filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
909If the \texttt{Vect} is empty, the result is easy:
911\begin{SaveVerbatim}{vfilternil}
913filter p Nil = (_ ** [])
919In the \texttt{::} case, we need to inspect the result of a recursive call to
921extract the length and the vector from the result. To do this, we use \texttt{with}
922notation, which allows pattern matching on intermediate values:
924\begin{SaveVerbatim}{vfiltercons}
926filter p (x :: xs) with (filter p xs)
927 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
933We will see more on \texttt{with} notation later.
935\subsection{\texttt{so}}
937The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
940\begin{SaveVerbatim}{sotype}
942data so : Bool -> Type where
949This is most useful for providing a static guarantee that a dynamic check has been made.
950For example, we might provide a safe interface to a function which draws a pixel
951on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
952the point \texttt{(x,y)} is within the bounds of a 640x480 window:
954\begin{SaveVerbatim}{soexample}
956inBounds : Int -> Int -> Bool
957inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
959drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
960drawPoint x y p = unsafeDrawPoint x y
965\subsection{More Expressions}
967\subsubsection*{\texttt{let} bindings}
969Intermediate values can be calculated using \texttt{let} bindings:
971\begin{SaveVerbatim}{letb}
973mirror : List a -> List a
974mirror xs = let xs' = rev xs in
981We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
982fields from a record as follows, as well as by pattern matching at the top level:
984\begin{SaveVerbatim}{letp}
986data Person = MkPerson String Int
988showPerson : Person -> String
989showPerson p = let MkPerson name age = p in
990 name ++ " is " ++ show age ++ " years old"
995\subsubsection*{List comprehensions}
999\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
1000building lists. The general form is:
1002\begin{SaveVerbatim}{listcomp}
1004[ expression | qualifiers ]
1010This generates the list of values produced by evaluating the
1011\texttt{expression}, according to the conditions given by the comma separated
1012\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
1015\begin{SaveVerbatim}{triples}
1017pythag : Int -> List (Int, Int, Int)
1018pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1025The \texttt{[a..b]} notation is another shorthand which builds a list of
1026numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]}
1027builds a list of numbers between \texttt{a} and \texttt{c} with the increment
1028specified by the difference between \texttt{a} and \texttt{c}. This works for
1029any numeric type, using the \texttt{count} function from the prelude.
1031\subsubsection*{\texttt{case} expressions}
1033Another way of inspecting intermediate values of \emph{simple} types
1034is to use a \texttt{case} expression.
1035The following function, for example, splits a string into two at a given character:
1037\begin{SaveVerbatim}{split}
1039splitAt : Char -> String -> (String, String)
1040splitAt c x = case break (== c) x of
1041 (x, y) => (x, strTail y)
1047\texttt{break} is a library function which breaks a string into a pair of strings
1048at the point where the given function returns true. We then deconstruct the
1049pair it returns, and remove the first character of the second string.
1051A \texttt{case} expression can match several cases, for example, to inspect an
1052intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
1053looks up an index in a list, returning \texttt{Nothing} if the index is out
1054of bounds. We can use this to write \texttt{lookup\_default}, which
1055looks up an index and returns a default value if the index is out of bounds:
1057\begin{SaveVerbatim}{listlookup}
1059lookup_default : Nat -> List a -> a -> a
1060lookup_default i xs def = case list_lookup i xs of
1068If the index is in bounds, we get the value at that index, otherwise we get
1071\begin{SaveVerbatim}{deftest}
1073*usefultypes> lookup_default 2 [3,4,5,6] (-1)
1075*usefultypes> lookup_default 4 [3,4,5,6] (-1)
1082\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
1083of intermediate expressions to avoid the need to write auxiliary functions, and is
1084also used internally to implement pattern matching \texttt{let} and lambda bindings.
1085It will \emph{only} work if:
1088\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
1089value of the same type.
1090\item The type of the result is ``known''. i.e. the type of the expression can be
1091determined \emph{without} type checking the \texttt{case}-expression itself.
1094\subsection{Dependent Records}
1096\remph{Records} are data types which collect several values (the record's
1097\remph{fields}) together. \Idris{} provides syntax for defining records and
1098automatically generating field access and update functions. For example, we
1099can represent a person's name and age in a record:
1101\begin{SaveVerbatim}{recsimpl}
1103record Person : Type where
1104 MkPerson : (name : String) ->
1105 (age : Int) -> Person
1108fred = MkPerson "Fred" 30
1114Record declarations are like \texttt{data} declarations, except that they are
1115introduced by the \texttt{record} keyword, and can only have one constructor.
1116The names of the binders in the constructor type (\texttt{name} and \texttt{age})
1117here are the field names, which we can use to access the field values:
1119\begin{SaveVerbatim}{recaccess}
1126name : Person -> String
1132We can also use the field names to update a record (or, more precisely, produce a
1133new record with the given fields updates).
1135\begin{SaveVerbatim}{recupdate}
1137*record> record { name = "Jim" } fred
1138MkPerson "Jim" 30 : Person
1139*record> record { name = "Jim", age = 20 } fred
1140MkPerson "Jim" 20 : Person
1146The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
1147the given fields in a record.
1149Records, and fields within records, can have dependent types.
1150Updates are allowed to change the type of a field,
1151provided that the result is well-typed, and the result does not affect the type of
1152the record as a whole. For example:
1154\begin{SaveVerbatim}{deprec}
1156record Class : Type where
1157 ClassInfo : (students : Vect Person n) ->
1158 (className : String) ->
1165It is safe to update the \texttt{students} field to a vector of a different length
1166because it will not affect the type of the record:
1168\begin{SaveVerbatim}{addstu}
1170addStudent : Person -> Class -> Class
1171addStudent p c = record { students = p :: students c } c
1173*record> addStudent fred (ClassInfo [] "CS")
1174ClassInfo (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