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 \texttt{where}
214clause (unless they have been redefined, such as \texttt{xs} here).
215\emph{However}, names which appear in the type are \emph{not} in scope. In particular,
216in the above example, the \texttt{a} in the top level type and the \texttt{a} in the
217auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required
218behaviour, the \texttt{a} can be brought into scope as follows:
220\begin{SaveVerbatim}{revwhereb}
222reverse : List a -> List a
223reverse {a} xs = revAcc [] xs where
224 revAcc : List a -> List a -> List a
231As well as functions, \texttt{where} blocks can include local data
232declarations, such as the following where \texttt{MyLT} is not accessible outside
233the definition of \texttt{foo}:
235\begin{SaveVerbatim}{wheredata}
245 isLT = if x < 20 then Yes else No
251In general, functions defined in a \texttt{where} clause need a type declaration
252just like any top level function. However, the type declaration for
253a function \texttt{f} \remph{can} be omitted if:
256\item \texttt{f} appears in the right hand side of the top level definition
257\item The type of \texttt{f} can be completely determined from its first
262So, for example, the following definitions are legal:
264\begin{SaveVerbatim}{whereinfer}
268even (S k) = odd k where
272test : Num a => List a
273test = [c 1, c 2, d 3]
275 d y = c (y + 1 + z y)
282\subsection{Dependent Types}
284\subsubsection{Vectors}
286A standard example of a dependent type is the type of ``lists with length'',
287conventionally called vectors in the dependent type literature. In \Idris{},
288we declare vectors as follows:
290\begin{SaveVerbatim}{vect}
292data Vect : Type -> Nat -> Type where
294 (::) : a -> Vect a k -> Vect a (S k)
300Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
301name overloading such as this is accepted by \Idris{}, provided that the names
302are declared in different namespaces (in practice, normally in different modules).
303Ambiguous constructor names can normally be resolved from context.
305This declares a family of types, and so the form of the declaration is rather
306different from the simple type declarations above. We explicitly state the type
307of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an
308argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}
309is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
310constructor targets a different part of the family of types. \tDC{Nil} can only
311be used to construct vectors with zero length, and \tDC{::} to construct
312vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element
313of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})
314combine to make a vector of length \texttt{S k}.
316We can define functions on dependent types such as \tTC{Vect} in the same way
317as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
318The type of a function over \tTC{Vect} will describe what happens to the
319lengths of the vectors involved. For example, \tFN{++}, defined in the
320library, appends two \tTC{Vect}s:
322\begin{SaveVerbatim}{vapp}
324(++) : Vect A n -> Vect A m -> Vect A (n + m)
326(++) (x :: xs) ys = x :: xs ++ ys
332The type of \tFN{(++)} states that the resulting vector's length will be the sum of
333the input lengths. If we get the definition wrong in such a way that this does
334not hold, \Idris{} will not accept the definition. For example:
336\begin{SaveVerbatim}{vapperr}
338(++) : Vect a n -> Vect a m -> Vect a (n + m)
340(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
345\begin{SaveVerbatim}{vapperrmsg}
347$ idris vbroken.idr --check
348vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
354\begin{SaveVerbatim}{bleh}
360This error message suggests that there is a length mismatch between two vectors
361--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
362of length \texttt{(S (k + k))}.
363Note that the terms in the error message have been \emph{normalised}, so in
364particular \texttt{n + m} has been reduced to \texttt{plus n m}.
366\subsubsection{The Finite Sets}
368Finite sets, as the name suggests, are sets with a finite number of elements.
369They are declared as follows (again, in the prelude):
371\begin{SaveVerbatim}{findecl}
373data Fin : Nat -> Type where
375 fS : Fin k -> Fin (S k)
381\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
383\texttt{n+1}th element of a finite set with \texttt{S k} elements.
384\tTC{Fin} is indexed by a \tTC{Nat}, which
385represents the number of elements in the set. Obviously we can't construct an
386element of an empty set, so neither constructor targets \texttt{Fin O}.
388A useful application of the \tTC{Fin} family is to represent bounded
389natural numbers. Since the first \tTC{n} natural numbers form a finite
390set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural
391numbers bounded by \tTC{n}.
393For example, the following function which looks up an element in a \tTC{Vect},
394by a bounded index given as a \tTC{Fin n}, is defined in the prelude:
396\begin{SaveVerbatim}{vindex}
398index : Fin n -> Vect a n -> a
399index fO (x :: xs) = x
400index (fS k) (x :: xs) = index k xs
406This function looks up a value at a given location in a vector. The location is
407bounded by the length of the vector (\texttt{n} in each case), so there is no
408need for a run-time bounds check. The type checker guarantees that the location
409is no larger than the length of the vector.
411Note also that there is no case for \texttt{Nil} here. This is because it is
412impossible. Since there is no element of \texttt{Fin O}, and the location is a
413\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
414look up an element in an empty vector would give a compile time type error,
415since it would force \texttt{n} to be \tDC{O}.
417\subsubsection{Implicit Arguments}
419Let us take a closer look at the type of \texttt{index}:
421\begin{SaveVerbatim}{vindexty}
423index : Fin n -> Vect a n -> a
429It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
430with \texttt{n} elements of type \texttt{a}. But there are also two names,
431\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
432arguments to \texttt{index}. We could also write the type of \texttt{index} as:
434\begin{SaveVerbatim}{vindeximpty}
436index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a
442Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are
443not given in applications of \texttt{index}; their values can be inferred from
444the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name
445with a \remph{lower case initial letter} which
446appears as a parameter or index in a type declaration, but which is otherwise
447free, will be automatically bound as an implicit argument. Implicit arguments
448can still be given explicitly in applications, using \texttt{\{a=value\}} and
449\texttt{\{n=value\}}, for example:
451\begin{SaveVerbatim}{vindexexp}
453index {a=Int} {n=2} fO (2 :: 3 :: Nil)
459In fact, any argument, implicit or explicit, may be given a name. We could have
460declared the type of \texttt{index} as:
462\begin{SaveVerbatim}{vindexn}
464index : (i:Fin n) -> (xs:Vect a n) -> a
470It is a matter of taste whether you want to do this --- sometimes it can help
471document a function by making the purpose of an argument more clear.
473\subsubsection{``\texttt{using}'' notation}
475Sometimes it is necessary to provide types of implicit arguments where
476the type checker can not work them out itself. This can happen if there is a
477dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
478before being used --- or if an implicit argument has a complex type. For example,
479we will need to state the types of the implicit arguments in the following
480definition, which defines a predicate on vectors:
482\begin{SaveVerbatim}{elem}
484data Elem : a -> Vect a n -> Type where
485 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)
486 there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)
492An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
493\texttt{xs}. We can construct
494such a predicate if the required element is \texttt{here}, at the head of the vector,
495or \texttt{there}, in the tail of the vector. For example:
497\begin{SaveVerbatim}{testelem}
500testVec = 3 :: 4 :: 5 :: 6 :: Nil
502inVect : Elem 5 testVec
503inVect = there (there here)
509If the same implicit arguments are being used a lot, it can make a definition
510difficult to read. To avoid this problem, a \texttt{using} block gives the types and
511ordering of any implicit arguments which can appear within the block:
513\begin{SaveVerbatim}{elemusing}
515using (x:a, y:a, xs:Vect a n)
516 data Elem : a -> Vect a n -> Type where
517 here : Elem x (x :: xs)
518 there : Elem x xs -> Elem x (y :: xs)
523\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
525In general, functions and data types must be defined before use, since
526dependent types allow functions to appear as part of types, and their
527reduction behaviour to affect type checking. However, this
528restriction can be relaxed by using a \texttt{mutual} block, which allows
529data types and functions to be defined simultaneously:
531\begin{SaveVerbatim}{mutual}
546In a \texttt{mutual} block, first all of the type declarations are added,
547then the function bodies. As a result, none of the function types can depend
548on the reduction behaviour of any of the functions in the block.
552Computer programs are of little use if they do not interact with the user or
553the system in some way. The difficulty in a pure language such as \Idris{} ---
554that is, a language where expressions do not have side-effects --- is that I/O
555is inherently side-effecting. Therefore in \Idris{}, such interactions are
556encapsulated in the type \texttt{IO}:
558\begin{SaveVerbatim}{ioty}
560data IO a -- IO operation returning a value of type a
566We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
567the I/O operations to be executed are, rather than how to execute them. The
568resulting operations are executed externally,
569by the run-time system. We've already seen one IO
572\begin{SaveVerbatim}{main}
575main = putStrLn "Hello world"
581The type of \texttt{putStrLn} explains that it takes a string, and returns an
582element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
583outputs a string without a newline:
585\begin{SaveVerbatim}{putstr}
587putStrLn : String -> IO ()
588putStr : String -> IO ()
592We can also read strings from user input:
594\begin{SaveVerbatim}{getline}
602A number of other I/O operations are defined in the prelude, for example for reading and
603writing files, including:
605\begin{SaveVerbatim}{fileops}
608data Mode = Read | Write | ReadWrite
610openFile : String -> Mode -> IO File
611closeFile : File -> IO ()
613fread : File -> IO String
614fwrite : File -> String -> IO ()
615feof : File -> IO Bool
617readFile : String -> IO String
622\subsection{``\texttt{do}'' notation}
626I/O programs will typically need to sequence actions, feeding the output of one
627computation into the input of the next. \texttt{IO} is an abstract type, however, so we
628can't access the result of a computation directly. Instead, we sequence
629operations with \texttt{do} notation:
631\begin{SaveVerbatim}{greet}
634greet = do putStr "What is your name? "
636 putStrLn ("Hello " ++ name)
642The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
644puts the result, of type \texttt{a} into the variable \texttt{x}.
645In this case, \texttt{getLine} returns an \texttt{IO String},
646so \texttt{name} has type \texttt{String}. Indentation is significant --- each
647statement in the do block must begin in the same column.
648The \texttt{return} operation allows us to inject a value directly into an IO
651\begin{SaveVerbatim}{return}
659As we will see later, \texttt{do} notation is more general than this, and can be
662\subsection{Useful Data Types}
664\Idris{} includes a number of useful data types and library functions (see the
665\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
666functions described here are imported automatically by every \Idris{} program, as
667part of \texttt{prelude.idr}.
669\subsubsection{\texttt{List} and \texttt{Vect}}
671We have already seen the \texttt{List} and \texttt{Vect} data types:
673\begin{SaveVerbatim}{listvec}
675data List a = Nil | (::) a (List a)
677data Vect : Type -> Nat -> Type where
679 (::) : a -> Vect a k -> Vect a (S k)
685Note that the constructor names are the same for each --- constructor names (in
686fact, names in general) can be overloaded, provided that they are declared in
687different namespaces (see Section \ref{sect:namespaces}), and will typically be
688resolved according to their type. As syntactic sugar, any type with the constructor
689names \texttt{Nil} and \texttt{::} can be written in list form. For example:
692\item \texttt{[]} means \texttt{Nil}
693\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
697The library also defines a number of functions for manipulating these types.
698\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
699and applies a function to every element of the list or vector.
701\begin{SaveVerbatim}{map}
703map : (a -> b) -> List a -> List b
705map f (x :: xs) = f x :: map f xs
707map : (a -> b) -> Vect a n -> Vect b n
709map f (x :: xs) = f x :: map f xs
715For example, to double every element in a vector of integers:
717\begin{SaveVerbatim}{dvect}
720intVec = [1, 2, 3, 4, 5]
729You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
731\begin{SaveVerbatim}{rundvect}
733*usefultypes> show (map double intVec)
734"[2, 4, 6, 8, 10]" : String
740For more details of the functions available on \texttt{List} and \texttt{Vect},
741look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
742Functions include filtering, appending, reversing, and so on. Also remember
743that \Idris{} is still in development, so if you don't see the function you
744need, please feel free to add it and submit a patch!
746\subsubsection*{Aside: Anonymous functions and operator sections}
748There are actually neater ways to write the above expression. One way would be
749to use an anonymous function:
751\begin{SaveVerbatim}{lam1}
753*usefultypes> show (map (\x => x * 2) intVec)
754"[2, 4, 6, 8, 10]" : String
760The notation \texttt{$\backslash$x => val} constructs an anonymous function
761which takes one argument, \texttt{x} and returns the expression \texttt{val}.
762Anonymous functions may take several arguments, separated by commas, e.g.
763\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
764types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,
765e.g. \texttt{$\backslash$ (x, y) => x + y}.
766We could also use an operator section:
768\begin{SaveVerbatim}{sec1}
770*usefultypes> show (map (* 2) intVec)
771"[2, 4, 6, 8, 10]" : String
777\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
778\texttt{$\backslash$x => x * 2}.
779Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
783\texttt{Maybe} describes an optional value. Either there is a value of the given type,
786\begin{SaveVerbatim}{maybe}
788data Maybe a = Just a | Nothing
794\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
795looking something up in a \texttt{List} (rather than a vector) may result in an out of
798\begin{SaveVerbatim}{lookuplist}
800list_lookup : Nat -> List a -> Maybe a
801list_lookup _ Nil = Nothing
802list_lookup O (x :: xs) = Just x
803list_lookup (S k) (x :: xs) = list_lookup k xs
809The \texttt{maybe} function is used to process values of type \texttt{Maybe},
810either by applying a function to the value, if there is one, or by providing a default value:
812\begin{SaveVerbatim}{maybefn}
814maybe : Maybe a -> |(default:b) -> (a -> b) -> b
820The vertical bar $\mid$ before the default value is a laziness annotation. Normally
821expressions are evaluated before being passed to a function. This is typically
822the most efficient behaviour. However, in this case, the default value might
823not be used and if it is a large expression, evaluating it will be wasteful.
824The $\mid$ annotation tells the compiler not to evaluate the argument until it is
827\subsubsection{Tuples and Dependent Pairs}
829Values can be paired with the following built-in data type:
831\begin{SaveVerbatim}{mkpair}
833data Pair a b = MkPair a b
839As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
840means either \texttt{Pair a b} or \texttt{MkPair a b}.
841Tuples can contain an arbitrary number of values, represented as nested pairs:
843\begin{SaveVerbatim}{tuple}
848jim : (String, Int, String)
849jim = ("Jim", 25, "Cambridge")
854\subsubsection*{Dependent Pairs}
856Dependent pairs allow the type of the second element of a pair to depend on
857the value of the first element:
859\begin{SaveVerbatim}{sigma}
861data Exists : (A : Type) -> (P : A -> Type) -> Type where
862 Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
868Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
869A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}
870constructs a value of this type. For example, we can pair a number with a
871\texttt{Vect} of a particular length.
873\begin{SaveVerbatim}{dvec}
875vec : (n : Nat ** Vect Int n)
882The type checker could of course infer the value of the first element from the
883length of the vector. We can write an underscore \texttt{\_} in place of values which we
884expect the type checker to fill in, so the above definition could also be
887\begin{SaveVerbatim}{dvec1}
889vec : (n : Nat ** Vect Int n)
896We might also prefer to omit the type of the first element of the pair, since,
897again, it can be inferred:
899\begin{SaveVerbatim}{dvec2}
901vec : (n ** Vect Int n)
908One use for dependent pairs is to return values of dependent types where the
909index is not necessarily known in advance. For example, if we filter elements
910out of a \texttt{Vect} according to some predicate, we will not know in advance what the
911length of the resulting vector will be:
913\begin{SaveVerbatim}{vfilter}
915filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
921If the \texttt{Vect} is empty, the result is easy:
923\begin{SaveVerbatim}{vfilternil}
925filter p Nil = (_ , [])
931In the \texttt{::} case, we need to inspect the result of a recursive call to
933extract the length and the vector from the result. To do this, we use \texttt{with}
934notation, which allows pattern matching on intermediate values:
936\begin{SaveVerbatim}{vfiltercons}
938filter p (x :: xs) with (filter p xs)
939 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
945We will see more on \texttt{with} notation later.
947\subsection{\texttt{so}}
949The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the
952\begin{SaveVerbatim}{sotype}
954data so : Bool -> Type where
961This is most useful for providing a static guarantee that a dynamic check has been made.
962For example, we might provide a safe interface to a function which draws a pixel
963on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that
964the point \texttt{(x,y)} is within the bounds of a 640x480 window:
966\begin{SaveVerbatim}{soexample}
968inBounds : Int -> Int -> Bool
969inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
971drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
972drawPoint x y p = unsafeDrawPoint x y
977\subsection{More Expressions}
979\subsubsection*{\texttt{let} bindings}
981Intermediate values can be calculated using \texttt{let} bindings:
983\begin{SaveVerbatim}{letb}
985mirror : List a -> List a
986mirror xs = let xs' = rev xs in
993We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
994fields from a record as follows, as well as by pattern matching at the top level:
996\begin{SaveVerbatim}{letp}
998data Person = MkPerson String Int
1000showPerson : Person -> String
1001showPerson p = let MkPerson name age = p in
1002 name ++ " is " ++ show age ++ " years old"
1007\subsubsection*{List comprehensions}
1011\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
1012building lists. The general form is:
1014\begin{SaveVerbatim}{listcomp}
1016[ expression | qualifiers ]
1022This generates the list of values produced by evaluating the
1023\texttt{expression}, according to the conditions given by the comma separated
1024\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
1027\begin{SaveVerbatim}{triples}
1029pythag : Int -> List (Int, Int, Int)
1030pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
1037The \texttt{[a..b]} notation is another shorthand which builds a list of
1038numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]}
1039builds a list of numbers between \texttt{a} and \texttt{c} with the increment
1040specified by the difference between \texttt{a} and \texttt{c}. This works for
1041any numeric type, using the \texttt{count} function from the prelude.
1043\subsubsection*{\texttt{case} expressions}
1045Another way of inspecting intermediate values of \emph{simple} types
1046is to use a \texttt{case} expression.
1047The following function, for example, splits a string into two at a given character:
1049\begin{SaveVerbatim}{split}
1051splitAt : Char -> String -> (String, String)
1052splitAt c x = case break (== c) x of
1053 (x, y) => (x, strTail y)
1059\texttt{break} is a library function which breaks a string into a pair of strings
1060at the point where the given function returns true. We then deconstruct the
1061pair it returns, and remove the first character of the second string.
1063A \texttt{case} expression can match several cases, for example, to inspect an
1064intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
1065looks up an index in a list, returning \texttt{Nothing} if the index is out
1066of bounds. We can use this to write \texttt{lookup\_default}, which
1067looks up an index and returns a default value if the index is out of bounds:
1069\begin{SaveVerbatim}{listlookup}
1071lookup_default : Nat -> List a -> a -> a
1072lookup_default i xs def = case list_lookup i xs of
1080If the index is in bounds, we get the value at that index, otherwise we get
1083\begin{SaveVerbatim}{deftest}
1085*usefultypes> lookup_default 2 [3,4,5,6] (-1)
1087*usefultypes> lookup_default 4 [3,4,5,6] (-1)
1094\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
1095of intermediate expressions to avoid the need to write auxiliary functions, and is
1096also used internally to implement pattern matching \texttt{let} and lambda bindings.
1097It will \emph{only} work if:
1100\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
1101value of the same type.
1102\item The type of the result is ``known''. i.e. the type of the expression can be
1103determined \emph{without} type checking the \texttt{case}-expression itself.
1106\subsection{Dependent Records}
1108\remph{Records} are data types which collect several values (the record's
1109\remph{fields}) together. \Idris{} provides syntax for defining records and
1110automatically generating field access and update functions. For example, we
1111can represent a person's name and age in a record:
1113\begin{SaveVerbatim}{recsimpl}
1115record Person : Type where
1116 MkPerson : (name : String) ->
1117 (age : Int) -> Person
1120fred = MkPerson "Fred" 30
1126Record declarations are like \texttt{data} declarations, except that they are
1127introduced by the \texttt{record} keyword, and can only have one constructor.
1128The names of the binders in the constructor type (\texttt{name} and \texttt{age})
1129here are the field names, which we can use to access the field values:
1131\begin{SaveVerbatim}{recaccess}
1138name : Person -> String
1144We can also use the field names to update a record (or, more precisely, produce a
1145new record with the given fields updates).
1147\begin{SaveVerbatim}{recupdate}
1149*record> record { name = "Jim" } fred
1150MkPerson "Jim" 30 : Person
1151*record> record { name = "Jim", age = 20 } fred
1152MkPerson "Jim" 20 : Person
1158The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
1159the given fields in a record.
1161Records, and fields within records, can have dependent types.
1162Updates are allowed to change the type of a field,
1163provided that the result is well-typed, and the result does not affect the type of
1164the record as a whole. For example:
1166\begin{SaveVerbatim}{deprec}
1168record Class : Type where
1169 ClassInfo : (students : Vect Person n) ->
1170 (className : String) ->
1177It is safe to update the \texttt{students} field to a vector of a different length
1178because it will not affect the type of the record:
1180\begin{SaveVerbatim}{addstu}
1182addStudent : Person -> Class -> Class
1183addStudent p c = record { students = p :: students c } c
1185*record> addStudent fred (ClassInfo [] "CS")
1186ClassInfo (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