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 = Z | 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{Z}), 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{Z}, \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 Z)) (S (S Z))
161Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
162S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : 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 Z))))))))))) : 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
261test = [c (S 1), c Z, d (S Z)]
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\footnote{Note that prior to \Idris{} 0.9.9,
277the order of the arguments to \texttt{Vect} was reversed.}:
279\begin{SaveVerbatim}{vect}
281data Vect : Nat -> Type -> Type where
283 (::) : a -> Vect k a -> Vect (S k) a
289Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
290name overloading such as this is accepted by \Idris{}, provided that the names
291are declared in different namespaces (in practice, normally in different modules).
292Ambiguous constructor names can normally be resolved from context.
294This declares a family of types, and so the form of the declaration is rather
295different from the simple type declarations above. We explicitly state the type
296of the type constructor \tTC{Vect} --- it takes a \tTC{Nat} and a type as an
297argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}
298is \emph{indexed} over \tTC{Nat} and \emph{parameterised} by \tTC{Type}. Each
299constructor targets a different part of the family of types. \tDC{Nil} can only
300be used to construct vectors with zero length, and \tDC{::} to construct
301vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element
302of type \texttt{a} and a tail of type \texttt{Vect k a} (i.e., a vector of length \texttt{k})
303combine to make a vector of length \texttt{S k}.
305We can define functions on dependent types such as \tTC{Vect} in the same way
306as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
307The type of a function over \tTC{Vect} will describe what happens to the
308lengths of the vectors involved. For example, \tFN{++}, defined in the
309library, appends two \tTC{Vect}s:
311\begin{SaveVerbatim}{vapp}
313(++) : Vect n a -> Vect m a -> Vect (n + m) a
315(++) (x :: xs) ys = x :: xs ++ ys
321The type of \tFN{(++)} states that the resulting vector's length will be the sum of
322the input lengths. If we get the definition wrong in such a way that this does
323not hold, \Idris{} will not accept the definition. For example:
325\begin{SaveVerbatim}{vapperr}
327(++) : Vect n a -> Vect m a -> Vect (n + m) a
329(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
334\begin{SaveVerbatim}{vapperrmsg}
336$ idris vbroken.idr --check
337vbroken.idr:3:Can't unify Vect n a with Vect m a
343\begin{SaveVerbatim}{bleh}
349This error message suggests that there is a length mismatch between two vectors
350--- we needed a vector of length \texttt{m}, but provided a vector
352%Note that the terms in the error message have been \emph{normalised}, so in
353%particular \texttt{n + m} has been reduced to \texttt{plus n m}.
355\subsubsection{The Finite Sets}
357Finite sets, as the name suggests, are sets with a finite number of elements.
358They are declared as follows (again, in the prelude):
360\begin{SaveVerbatim}{findecl}
362data Fin : Nat -> Type where
364 fS : Fin k -> Fin (S k)
370\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
372\texttt{n+1}th element of a finite set with \texttt{S k} elements.
373\tTC{Fin} is indexed by a \tTC{Nat}, which
374represents the number of elements in the set. Obviously we can't construct an
375element of an empty set, so neither constructor targets \texttt{Fin Z}.
377A useful application of the \tTC{Fin} family is to represent bounded
378natural numbers. Since the first \tTC{n} natural numbers form a finite
379set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural
380numbers bounded by \tTC{n}.
382For example, the following function which looks up an element in a \tTC{Vect},
383by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
385\begin{SaveVerbatim}{vindex}
387index : Fin n -> Vect n a -> a
388index fZ (x :: xs) = x
389index (fS k) (x :: xs) = index k xs
395This function looks up a value at a given location in a vector. The location is
396bounded by the length of the vector (\texttt{n} in each case), so there is no
397need for a run-time bounds check. The type checker guarantees that the location
398is no larger than the length of the vector.
400Note also that there is no case for \texttt{Nil} here. This is because it is
401impossible. Since there is no element of \texttt{Fin Z}, and the location is a
402\texttt{Fin n}, then \texttt{n} can not be \tDC{Z}. As a result, attempting to
403look up an element in an empty vector would give a compile time type error,
404since it would force \texttt{n} to be \tDC{Z}.
406\subsubsection{Implicit Arguments}
408Let us take a closer look at the type of \texttt{index}:
410\begin{SaveVerbatim}{vindexty}
412index : Fin n -> Vect n a -> a
418It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
419with \texttt{n} elements of type \texttt{a}. But there are also two names,
420\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
421arguments to \texttt{index}. We could also write the type of \texttt{index} as:
423\begin{SaveVerbatim}{vindeximpty}
425index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
431Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
432not given in applications of \texttt{index}; their values can be inferred from
433the types of the \texttt{Fin n} and \texttt{Vect n a} arguments. Any name
434with a \remph{lower case initial letter} which
435appears as a parameter or index in a type declaration, but which is otherwise
436free, will be automatically bound as an implicit argument. Implicit arguments
437can still be given explicitly in applications, using \texttt{\{a=value\}} and
438\texttt{\{n=value\}}, for example:
440\begin{SaveVerbatim}{vindexexp}
442index {a=Int} {n=2} fZ (2 :: 3 :: Nil)
448In fact, any argument, implicit or explicit, may be given a name. We could have
449declared the type of \texttt{index} as:
451\begin{SaveVerbatim}{vindexn}
453index : (i:Fin n) -> (xs:Vect n a) -> a
459It is a matter of taste whether you want to do this --- sometimes it can help
460document a function by making the purpose of an argument more clear.
462\subsubsection{``\texttt{using}'' notation}
464Sometimes it is necessary to provide types of implicit arguments where
465the type checker can not work them out itself. This can happen if there is a
466dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
467before being used --- or if an implicit argument has a complex type. For example,
468we will need to state the types of the implicit arguments in the following
469definition, which defines a predicate on vectors:
471\begin{SaveVerbatim}{elem}
473data Elem : a -> Vect n a -> Type where
474 here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
475 there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
481An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
482\texttt{xs}. We can construct
483such a predicate if the required element is \texttt{here}, at the head of the vector,
484or \texttt{there}, in the tail of the vector. For example:
486\begin{SaveVerbatim}{testelem}
489testVec = 3 :: 4 :: 5 :: 6 :: Nil
491inVect : Elem 5 testVec
492inVect = there (there here)
498If the same implicit arguments are being used a lot, it can make a definition
499difficult to read. To avoid this problem, a \texttt{using} block gives the types and
500ordering of any implicit arguments which can appear within the block:
502\begin{SaveVerbatim}{elemusing}
504using (x:a, y:a, xs:Vect n a)
505 data Elem : a -> Vect n a -> Type where
506 here : Elem x (x :: xs)
507 there : Elem x xs -> Elem x (y :: xs)
512\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
514In general, functions and data types must be defined before use, since
515dependent types allow functions to appear as part of types, and their
516reduction behaviour to affect type checking. However, this
517restriction can be relaxed by using a \texttt{mutual} block, which allows
518data types and functions to be defined simultaneously:
520\begin{SaveVerbatim}{mutual}
535In a \texttt{mutual} block, first all of the type declarations are added,
536then the function bodies. As a result, none of the function types can depend
537on the reduction behaviour of any of the functions in the block.
541Computer programs are of little use if they do not interact with the user or
542the system in some way. The difficulty in a pure language such as \Idris{} ---
543that is, a language where expressions do not have side-effects --- is that I/O
544is inherently side-effecting. Therefore in \Idris{}, such interactions are
545encapsulated in the type \texttt{IO}:
547\begin{SaveVerbatim}{ioty}
549data IO a -- IO operation returning a value of type a
555We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
556the I/O operations to be executed are, rather than how to execute them. The
557resulting operations are executed externally,
558by the run-time system. We've already seen one IO
561\begin{SaveVerbatim}{main}
564main = putStrLn "Hello world"
570The type of \texttt{putStrLn} explains that it takes a string, and returns an
571element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
572outputs a string without a newline:
574\begin{SaveVerbatim}{putstr}
576putStrLn : String -> IO ()
577putStr : String -> IO ()
581We can also read strings from user input:
583\begin{SaveVerbatim}{getline}
591A number of other I/O operations are defined in the prelude, for example for reading and
592writing files, including:
594\begin{SaveVerbatim}{fileops}
597data Mode = Read | Write | ReadWrite
599openFile : String -> Mode -> IO File
600closeFile : File -> IO ()
602fread : File -> IO String
603fwrite : File -> String -> IO ()
604feof : File -> IO Bool
606readFile : String -> IO String
611\subsection{``\texttt{do}'' notation}
615I/O programs will typically need to sequence actions, feeding the output of one
616computation into the input of the next. \texttt{IO} is an abstract type, however, so we
617can't access the result of a computation directly. Instead, we sequence
618operations with \texttt{do} notation:
620\begin{SaveVerbatim}{greet}
623greet = do putStr "What is your name? "
625 putStrLn ("Hello " ++ name)
631The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
633puts the result, of type \texttt{a} into the variable \texttt{x}.
634In this case, \texttt{getLine} returns an \texttt{IO String},
635so \texttt{name} has type \texttt{String}. Indentation is significant --- each
636statement in the do block must begin in the same column.
637The \texttt{return} operation allows us to inject a value directly into an IO
640\begin{SaveVerbatim}{return}
648As we will see later, \texttt{do} notation is more general than this, and can be
651\subsection{Useful Data Types}
653\Idris{} includes a number of useful data types and library functions (see the
654\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
655functions described here are imported automatically by every \Idris{} program, as
656part of \texttt{prelude.idr}.
658\subsubsection{\texttt{List} and \texttt{Vect}}
660We have already seen the \texttt{List} and \texttt{Vect} data types:
662\begin{SaveVerbatim}{listvec}
664data List a = Nil | (::) a (List a)
666data Vect : Nat -> Type -> Type where
668 (::) : a -> Vect k a -> Vect (S k) a
674Note that the constructor names are the same for each --- constructor names (in
675fact, names in general) can be overloaded, provided that they are declared in
676different namespaces (see Section \ref{sect:namespaces}), and will typically be
677resolved according to their type. As syntactic sugar, any type with the constructor
678names \texttt{Nil} and \texttt{::} can be written in list form. For example:
681\item \texttt{[]} means \texttt{Nil}
682\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
686The library also defines a number of functions for manipulating these types.
687\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
688and applies a function to every element of the list or vector.
690\begin{SaveVerbatim}{map}
692map : (a -> b) -> List a -> List b
694map f (x :: xs) = f x :: map f xs
696map : (a -> b) -> Vect n a -> Vect n b
698map f (x :: xs) = f x :: map f xs
704For example, to double every element in a vector of integers:
706\begin{SaveVerbatim}{dvect}
709intVec = [1, 2, 3, 4, 5]
718You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
720\begin{SaveVerbatim}{rundvect}
722*usefultypes> show (map double intVec)
723"[2, 4, 6, 8, 10]" : String
729For more details of the functions available on \texttt{List} and \texttt{Vect},
730look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
731Functions include filtering, appending, reversing, and so on. Also remember
732that \Idris{} is still in development, so if you don't see the function you
733need, please feel free to add it and submit a patch!
735\subsubsection*{Aside: Anonymous functions and operator sections}
737There are actually neater ways to write the above expression. One way would be
738to use an anonymous function:
740\begin{SaveVerbatim}{lam1}
742*usefultypes> show (map (\x => x * 2) intVec)
743"[2, 4, 6, 8, 10]" : String
749The notation \texttt{$\backslash$x => val} constructs an anonymous function
750which takes one argument, \texttt{x} and returns the expression \texttt{val}.
751Anonymous functions may take several arguments, separated by commas, e.g.
752\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
753types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
754e.g. \texttt{$\backslash$ (x, y) => x + y}.
755We could also use an operator section:
757\begin{SaveVerbatim}{sec1}
759*usefultypes> show (map (* 2) intVec)
760"[2, 4, 6, 8, 10]" : String
766\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
767\texttt{$\backslash$x => x * 2}.
768Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
772\texttt{Maybe} describes an optional value. Either there is a value of the given type,
775\begin{SaveVerbatim}{maybe}
777data Maybe a = Just a | Nothing
783\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
784looking something up in a \texttt{List} (rather than a vector) may result in an out of
787\begin{SaveVerbatim}{lookuplist}
789list_lookup : Nat -> List a -> Maybe a
790list_lookup _ Nil = Nothing
791list_lookup Z (x :: xs) = Just x
792list_lookup (S k) (x :: xs) = list_lookup k xs
798The \texttt{maybe} function is used to process values of type \texttt{Maybe},
799either by applying a function to the value, if there is one, or by providing a default value:
801\begin{SaveVerbatim}{maybefn}
803maybe : Maybe a -> |(default:b) -> (a -> b) -> b
809The vertical bar $\mid$ before the default value is a laziness annotation. Normally
810expressions are evaluated before being passed to a function. This is typically
811the most efficient behaviour. However, in this case, the default value might
812not be used and if it is a large expression, evaluating it will be wasteful.
813The $\mid$ annotation tells the compiler not to evaluate the argument until it is
816\subsubsection{Tuples and Dependent Pairs}
818Values can be paired with the following built-in data type:
820\begin{SaveVerbatim}{mkpair}
822data Pair a b = MkPair a b
828As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
829means either \texttt{Pair a b} or \texttt{MkPair a b}.
830Tuples can contain an arbitrary number of values, represented as nested pairs:
832\begin{SaveVerbatim}{tuple}
837jim : (String, Int, String)
838jim = ("Jim", 25, "Cambridge")
843\subsubsection*{Dependent Pairs}
845Dependent pairs allow the type of the second element of a pair to depend on
846the value of the first element:
848\begin{SaveVerbatim}{sigma}
850data Exists : (A : Type) -> (P : A -> Type) -> Type where
851 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
857Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
858A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}
859constructs a value of this type. For example, we can pair a number with a
860\texttt{Vect} of a particular length.
862\begin{SaveVerbatim}{dvec}
864vec : (n : Nat ** Vect n Int)
871The type checker could of course infer the value of the first element from the
872length of the vector. We can write an underscore \texttt{\_} in place of values which we
873expect the type checker to fill in, so the above definition could also be
876\begin{SaveVerbatim}{dvec1}
878vec : (n : Nat ** Vect n Int)
885We might also prefer to omit the type of the first element of the pair, since,
886again, it can be inferred:
888\begin{SaveVerbatim}{dvec2}
890vec : (n ** Vect n Int)
897One use for dependent pairs is to return values of dependent types where the
898index is not necessarily known in advance. For example, if we filter elements
899out of a \texttt{Vect} according to some predicate, we will not know in advance what the
900length of the resulting vector will be:
902\begin{SaveVerbatim}{vfilter}
904filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
910If the \texttt{Vect} is empty, the result is easy:
912\begin{SaveVerbatim}{vfilternil}
914filter p Nil = (_ ** [])
920In the \texttt{::} case, we need to inspect the result of a recursive call to
922extract the length and the vector from the result. To do this, we use \texttt{with}
923notation, which allows pattern matching on intermediate values:
925\begin{SaveVerbatim}{vfiltercons}
927filter p (x :: xs) with (filter p xs)
928 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
934We will see more on \texttt{with} notation later.
936\subsection{\texttt{so}}
938The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
941\begin{SaveVerbatim}{sotype}
943data so : Bool -> Type where
950This is most useful for providing a static guarantee that a dynamic check has been made.
951For example, we might provide a safe interface to a function which draws a pixel
952on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
953the point \texttt{(x,y)} is within the bounds of a 640x480 window:
955\begin{SaveVerbatim}{soexample}
957inBounds : Int -> Int -> Bool
958inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
960drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
961drawPoint x y p = unsafeDrawPoint x y
966\subsection{More Expressions}
968\subsubsection*{\texttt{let} bindings}
970Intermediate values can be calculated using \texttt{let} bindings:
972\begin{SaveVerbatim}{letb}
974mirror : List a -> List a
975mirror xs = let xs' = rev xs in
982We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
983fields from a record as follows, as well as by pattern matching at the top level:
985\begin{SaveVerbatim}{letp}
987data Person = MkPerson String Int
989showPerson : Person -> String
990showPerson p = let MkPerson name age = p in
991 name ++ " is " ++ show age ++ " years old"
996\subsubsection*{List comprehensions}
1000\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
1001building lists. The general form is:
1003\begin{SaveVerbatim}{listcomp}
1005[ expression | qualifiers ]
1011This generates the list of values produced by evaluating the
1012\texttt{expression}, according to the conditions given by the comma separated
1013\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
1016\begin{SaveVerbatim}{triples}
1018pythag : Int -> List (Int, Int, Int)
1019pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1026The \texttt{[a..b]} notation is another shorthand which builds a list of
1027numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]}
1028builds a list of numbers between \texttt{a} and \texttt{c} with the increment
1029specified by the difference between \texttt{a} and \texttt{b}. This works for
1030any numeric type, using the \texttt{count} function from the prelude.
1032\subsubsection*{\texttt{case} expressions}
1034Another way of inspecting intermediate values of \emph{simple} types
1035is to use a \texttt{case} expression.
1036The following function, for example, splits a string into two at a given character:
1038\begin{SaveVerbatim}{split}
1040splitAt : Char -> String -> (String, String)
1041splitAt c x = case break (== c) x of
1042 (x, y) => (x, strTail y)
1048\texttt{break} is a library function which breaks a string into a pair of strings
1049at the point where the given function returns true. We then deconstruct the
1050pair it returns, and remove the first character of the second string.
1052A \texttt{case} expression can match several cases, for example, to inspect an
1053intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
1054looks up an index in a list, returning \texttt{Nothing} if the index is out
1055of bounds. We can use this to write \texttt{lookup\_default}, which
1056looks up an index and returns a default value if the index is out of bounds:
1058\begin{SaveVerbatim}{listlookup}
1060lookup_default : Nat -> List a -> a -> a
1061lookup_default i xs def = case list_lookup i xs of
1069If the index is in bounds, we get the value at that index, otherwise we get
1072\begin{SaveVerbatim}{deftest}
1074*usefultypes> lookup_default 2 [3,4,5,6] (-1)
1076*usefultypes> lookup_default 4 [3,4,5,6] (-1)
1083\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
1084of intermediate expressions to avoid the need to write auxiliary functions, and is
1085also used internally to implement pattern matching \texttt{let} and lambda bindings.
1086It will \emph{only} work if:
1089\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
1090value of the same type.
1091\item The type of the result is ``known''. i.e. the type of the expression can be
1092determined \emph{without} type checking the \texttt{case}-expression itself.
1095\subsection{Dependent Records}
1097\remph{Records} are data types which collect several values (the record's
1098\remph{fields}) together. \Idris{} provides syntax for defining records and
1099automatically generating field access and update functions. For example, we
1100can represent a person's name and age in a record:
1102\begin{SaveVerbatim}{recsimpl}
1104record Person : Type where
1105 MkPerson : (name : String) ->
1106 (age : Int) -> Person
1109fred = MkPerson "Fred" 30
1115Record declarations are like \texttt{data} declarations, except that they are
1116introduced by the \texttt{record} keyword, and can only have one constructor.
1117The names of the binders in the constructor type (\texttt{name} and \texttt{age})
1118here are the field names, which we can use to access the field values:
1120\begin{SaveVerbatim}{recaccess}
1127name : Person -> String
1133We can also use the field names to update a record (or, more precisely, produce a
1134new record with the given fields updates).
1136\begin{SaveVerbatim}{recupdate}
1138*record> record { name = "Jim" } fred
1139MkPerson "Jim" 30 : Person
1140*record> record { name = "Jim", age = 20 } fred
1141MkPerson "Jim" 20 : Person
1147The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
1148the given fields in a record.
1150Records, and fields within records, can have dependent types.
1151Updates are allowed to change the type of a field,
1152provided that the result is well-typed, and the result does not affect the type of
1153the record as a whole. For example:
1155\begin{SaveVerbatim}{deprec}
1157record Class : Type where
1158 ClassInfo : (students : Vect n Person) ->
1159 (className : String) ->
1166It is safe to update the \texttt{students} field to a vector of a different length
1167because it will not affect the type of the record:
1169\begin{SaveVerbatim}{addstu}
1171addStudent : Person -> Class -> Class
1172addStudent p c = record { students = p :: students c } c
1174*record> addStudent fred (ClassInfo [] "CS")
1175ClassInfo (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