# edwinb/Idris-dev forked from idris-lang/Idris-dev

Fetching contributors…
Cannot retrieve contributors at this time
1110 lines (788 sloc) 33 KB
 \section{Types and Functions} \subsection{Primitive Types} \Idris{} defines several primitive types: \tTC{Int}, \tTC{Integer} and \tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for text manipulation, and \tTC{Ptr} which represents foreign pointers. There are also several data types declared in the library, including \tTC{Bool}, with values \tDC{True} and \tDC{False}. We can declare some constants with these types. Enter the following into a file \texttt{prims.idr} and load it into the \Idris{} interactive environment by typing \texttt{idris prims.idr}: \begin{SaveVerbatim}{constprims} module prims x : Int x = 42 foo : String foo = "Sausage machine" bar : Char bar = 'Z' quux : Bool quux = False \end{SaveVerbatim} \useverb{constprims} \noindent An \Idris{} file consists of an optional module declaration (here \texttt{module prims}) followed by an optional list of imports (none here, however \Idris{} programs can consist of several modules, and the definitions in each module each have their own namespace, as we will discuss in Section \ref{sect:namespaces}) and a collection of declarations and definitions. Each definition must have a type declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc). Indentation is significant --- a new declaration begins at the same level of indentation as the preceding declaration. Alternatively, declarations may be terminated with a semicolon. A library module \texttt{prelude} is automatically imported by every \Idris{} program, including facilities for IO, arithmetic, data structures and various common functions. The prelude defines several arithmetic and comparison operators, which we can use at the prompt. Evaluating things at the prompt gives an answer, and the type of the answer. For example: \begin{SaveVerbatim}{promptprim} *prims> 6*6+6 42 : Int *prims> x == 6*6+6 True : Bool \end{SaveVerbatim} \useverb{promptprim} \noindent All of the usual arithmetic and comparison operators are defined for the primitive types. They are overloaded using type classes, as we will discuss in Section \ref{sec:classes} and can be extended to work on user defined types. Boolean expressions can be tested with the \texttt{if...then...else} construct: \begin{SaveVerbatim}{ifthenelse} *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer" "The answer!" : String \end{SaveVerbatim} \useverb{ifthenelse} \subsection{Data Types} Data types are declared in a similar way to Haskell data types, with a similar syntax. Natural numbers and lists, for example, can be declared as follows: \begin{SaveVerbatim}{natlist} data Nat = O | S Nat -- Natural numbers -- (zero and successor) data List a = Nil | (::) a (List a) -- Polymorphic lists \end{SaveVerbatim} \useverb{natlist} \noindent The above declarations are taken from the standard library. Unary natural numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or the successor of another natural number (\texttt{S k}). Lists can either be empty (\texttt{Nil}) or a value added to the front of another list (\texttt{x :: xs}). In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators such as this can be added using a fixity declaration, as follows: \begin{SaveVerbatim}{infixcons} infixr 10 :: \end{SaveVerbatim} \useverb{infixcons} \noindent Functions, data constructors and type constuctors may all be given infix operators as names. They may be used in prefix form if enclosed in brackets, e.g. \tDC{(::)}. Infix operators can use any of the symbols: \begin{SaveVerbatim}{infixsyms} :+-*/=_.?|&> Nat -> Nat plus O y = y plus (S k) y = S (plus k y) -- Unary multiplication mult : Nat -> Nat -> Nat mult O y = O mult (S k) y = plus y (mult k y) \end{SaveVerbatim} \useverb{natfns} \noindent The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded for use by \texttt{Nat}, and are implemented using the above functions. Unlike Haskell, there is no restriction on whether types and function names must begin with a capital letter or not. Function names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S}, \tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are all part of the same namespace. We can test these functions at the \Idris{} prompt: \begin{SaveVerbatim}{fntest} Idris> plus (S (S O)) (S (S O)) S (S (S (S O))) : Nat Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O))) S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat \end{SaveVerbatim} \useverb{fntest} \noindent Like arithmetic operations, integer literals are also overloaded using type classes, meaning that we can also test the functions as follows: \begin{SaveVerbatim}{fntest} Idris> plus 2 2 S (S (S (S O))) : Nat Idris> mult 3 (plus 2 2) S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat \end{SaveVerbatim} \useverb{fntest} \noindent You may wonder, by the way, why we have unary natural numbers when our computers have perfectly good integer arithmetic built in. The reason is primarily that unary numbers have a very convenient structure which is easy to reason about, and easy to relate to other data structures as we will see later. Nevertheless, we do not want this convenience to be at the expense of efficiency. Fortunately, \Idris{} knows about the relationship between \tTC{Nat} (and similarly structured types) and numbers, so optimises the representation and functions such as \tFN{plus} and \tFN{mult}. \subsubsection*{\texttt{where} clauses} Functions can also be defined \emph{locally} using \texttt{where} clauses. For example, to define a function which reverses a list, we can use an auxiliary function which accumulates the new, reversed list, and which does not need to be visible globally: \begin{SaveVerbatim}{revwhere} reverse : List a -> List a reverse xs = revAcc [] xs where revAcc : List a -> List a -> List a revAcc acc [] = acc revAcc acc (x :: xs) = revAcc (x :: acc) xs \end{SaveVerbatim} \useverb{revwhere} \noindent Indentation is significant --- functions in the \texttt{where} block must be indented further than the outer function. \textbf{Scope:} Any names which are visible in the outer scope are also visible in the \texttt{where} clause (unless they have been redefined, such as \texttt{xs} here). \emph{However}, names which appear in the type are \emph{not} in scope. In particular, in the above example, the \texttt{a} in the top level type and the \texttt{a} in the auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required behaviour, the \texttt{a} can be brought into scope as follows: \begin{SaveVerbatim}{revwhereb} reverse : List a -> List a reverse {a} xs = revAcc [] xs where revAcc : List a -> List a -> List a ... \end{SaveVerbatim} \useverb{revwhereb} \subsection{Dependent Types} \subsubsection{Vectors} A standard example of a dependent type is the type of lists with length'', conventionally called vectors in the dependent type literature. In \Idris{}, we declare vectors as follows: \begin{SaveVerbatim}{vect} data Vect : Set -> Nat -> Set where Nil : Vect a O (::) : a -> Vect a k -> Vect a (S k) \end{SaveVerbatim} \useverb{vect} \noindent Note that we have used the same constructor names as for \tTC{List}. Ad-hoc name overloading such as this is accepted by \Idris{}, provided that the names are declared in different namespaces (in practice, normally in different modules). Ambiguous constructor names can normally be resolved from context. This declares a family of types, and so the form of the declaration is rather different from the simple type declarations above. We explicitly state the type of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect} is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each constructor targets a different part of the family of types. \tDC{Nil} can only be used to construct vectors with zero length, and \tDC{::} to construct vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k}) combine to make a vector of length \texttt{S k}. We can define functions on dependent types such as \tTC{Vect} in the same way as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching. The type of a function over \tTC{Vect} will describe what happens to the lengths of the vectors involved. For example, \tFN{++}, defined in the library, appends two \tTC{Vect}s: \begin{SaveVerbatim}{vapp} (++) : Vect A n -> Vect A m -> Vect A (n + m) (++) Nil ys = ys (++) (x :: xs) ys = x :: xs ++ ys \end{SaveVerbatim} \useverb{vapp} \noindent The type of \tFN{(++)} states that the resulting vector's length will be the sum of the input lengths. If we get the definition wrong in such a way that this does not hold, \Idris{} will not accept the definition. For example: \begin{SaveVerbatim}{vapperr} (++) : Vect a n -> Vect a m -> Vect a (n + m) (++) Nil ys = ys (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN \end{SaveVerbatim} \useverb{vapperr} \begin{SaveVerbatim}{vapperrmsg} $idris vbroken.idr --check vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m)) Specifically: Can't unify k with m \end{SaveVerbatim} \begin{SaveVerbatim}{bleh}$ \end{SaveVerbatim} \useverb{vapperrmsg} \noindent This error message suggests that there is a length mismatch between two vectors --- we needed a vector of length \texttt{(S (k + m))}, but provided a vector of length \texttt{(S (k + k))}. Note that the terms in the error message have been \emph{normalised}, so in particular \texttt{n + m} has been reduced to \texttt{plus n m}. \subsubsection{The Finite Sets} Finite sets, as the name suggests, are sets with a finite number of elements. They are declared as follows (again, in the prelude): \begin{SaveVerbatim}{findecl} data Fin : Nat -> Set where fO : Fin (S k) fS : Fin k -> Fin (S k) \end{SaveVerbatim} \useverb{findecl} \noindent \tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements; \texttt{fS n} is the \texttt{n+1}th element of a finite set with \texttt{S k} elements. \tTC{Fin} is indexed by a \tTC{Nat}, which represents the number of elements in the set. Obviously we can't construct an element of an empty set, so neither constructor targets \texttt{Fin O}. A useful application of the \tTC{Fin} family is to represent bounded natural numbers. Since the first \tTC{n} natural numbers form a finite set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural numbers bounded by \tTC{n}. For example, the following function which looks up an element in a \tTC{Vect}, by a bounded index given as a \tTC{Fin n}, is defined in the prelude: \begin{SaveVerbatim}{vindex} index : Fin n -> Vect a n -> a index fO (x :: xs) = x index (fS k) (x :: xs) = index k xs \end{SaveVerbatim} \useverb{vindex} \noindent This function looks up a value at a given location in a vector. The location is bounded by the length of the vector (\texttt{n} in each case), so there is no need for a run-time bounds check. The type checker guarantees that the location is no larger than the length of the vector. Note also that there is no case for \texttt{Nil} here. This is because it is impossible. Since there is no element of \texttt{Fin O}, and the location is a \texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to look up an element in an empty vector would give a compile time type error, since it would force \texttt{n} to be \tDC{O}. \subsubsection{Implicit Arguments} Let us take a closer look at the type of \texttt{index}: \begin{SaveVerbatim}{vindexty} index : Fin n -> Vect a n -> a \end{SaveVerbatim} \useverb{vindexty} \noindent It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector with \texttt{n} elements of type \texttt{a}. But there are also two names, \texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit} arguments to \texttt{index}. We could also write the type of \texttt{index} as: \begin{SaveVerbatim}{vindeximpty} index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a \end{SaveVerbatim} \useverb{vindeximpty} \noindent Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in applications of \texttt{index}; their values can be inferred from the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter or index in a type declaration, but which is otherwise free, will be automatically bound as an implicit argument. Implicit arguments can still be given explicitly in applications, using \texttt{\{a=value\}} and \texttt{\{n=value\}}, for example: \begin{SaveVerbatim}{vindexexp} index {a=Int} {n=2} fO (2 :: 3 :: Nil) \end{SaveVerbatim} \useverb{vindexexp} \noindent In fact, any argument, implicit or explicit, may be given a name. We could have declared the type of \texttt{index} as: \begin{SaveVerbatim}{vindexn} index : (i:Fin n) -> (xs:Vect a n) -> a \end{SaveVerbatim} \useverb{vindexn} \noindent It is a matter of taste whether you want to do this --- sometimes it can help document a function by making the purpose of an argument more clear. \subsubsection{\texttt{using}'' notation} Sometimes it is necessary to provide types of implicit arguments where the type checker can not work them out itself. This can happen if there is a dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above before being used --- or if an implicit argument has a complex type. For example, we will need to state the types of the implicit arguments in the following definition, which defines a predicate on vectors: \begin{SaveVerbatim}{elem} data Elem : a -> Vect a n -> Set where here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs) there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs) \end{SaveVerbatim} \useverb{elem} \noindent An instance of \texttt{Elem x xs} states that \texttt{x} is an element of \texttt{xs}. We can construct such a predicate if the required element is \texttt{here}, at the head of the vector, or \texttt{there}, in the tail of the vector. For example: \begin{SaveVerbatim}{testelem} testVec : Vect Int 4 testVec = 3 :: 4 :: 5 :: 6 :: Nil inVect : Elem 5 testVec inVect = there (there here) \end{SaveVerbatim} \useverb{testelem} \noindent If the same implicit arguments are being used a lot, it can make a definition difficult to read. To avoid this problem, a \texttt{using} block gives the types and ordering of any implicit arguments which can appear within the block: \begin{SaveVerbatim}{elemusing} using (x:a, y:a, xs:Vect a n) data Elem : a -> Vect a n -> Set where here : Elem x (x :: xs) there : Elem x xs -> Elem x (y :: xs) \end{SaveVerbatim} \useverb{elemusing} \subsection{I/O} Computer programs are of little use if they do not interact with the user or the system in some way. The difficulty in a pure language such as \Idris{} --- that is, a language where expressions do not have side-effects --- is that I/O is inherently side-effecting. Therefore in \Idris{}, such interactions are encapsulated in the type \texttt{IO}: \begin{SaveVerbatim}{ioty} data IO a -- IO operation returning a value of type a \end{SaveVerbatim} \useverb{ioty} \noindent We'll leave the definition of \texttt{IO} abstract, but effectively it describes what the I/O operations to be executed are, rather than how to execute them. The resulting operations are executed externally, by the run-time system. We've already seen one IO program: \begin{SaveVerbatim}{main} main : IO () main = putStrLn "Hello world" \end{SaveVerbatim} \useverb{main} \noindent The type of \texttt{putStrLn} explains that it takes a string, and returns an element of the unit type () via an I/O action. There is a variant \texttt{putStr} which outputs a string without a newline: \begin{SaveVerbatim}{putstr} putStrLn : String -> IO () putStr : String -> IO () \end{SaveVerbatim} We can also read strings from user input: \begin{SaveVerbatim}{getline} getLine : IO String \end{SaveVerbatim} \useverb{getline} \noindent A number of other I/O operations are defined in the prelude, for example for reading and writing files, including: \begin{SaveVerbatim}{fileops} data File -- abstract data Mode = Read | Write | ReadWrite openFile : String -> Mode -> IO File closeFile : File -> IO () fread : File -> IO String fwrite : File -> String -> IO () feof : File -> IO Bool readFile : String -> IO String \end{SaveVerbatim} \useverb{fileops} \subsection{\texttt{do}'' notation} \label{sect:do} I/O programs will typically need to sequence actions, feeding the output of one computation into the input of the next. \texttt{IO} is an abstract type, however, so we can't access the result of a computation directly. Instead, we sequence operations with \texttt{do} notation: \begin{SaveVerbatim}{greet} greet : IO () greet = do putStr "What is your name? " name <- getLine putStrLn ("Hello " ++ name) \end{SaveVerbatim} \useverb{greet} \noindent The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type \texttt{IO a}, and puts the result, of type \texttt{a} into the variable \texttt{x}. In this case, \texttt{getLine} returns an \texttt{IO String}, so \texttt{name} has type \texttt{String}. Indentation is significant --- each statement in the do block must begin in the same column. The \texttt{return} operation allows us to inject a value directly into an IO operation: \begin{SaveVerbatim}{return} return : a -> IO a \end{SaveVerbatim} \useverb{return} \noindent As we will see later, \texttt{do} notation is more general than this, and can be overloaded. \subsection{Useful Data Types} \Idris{} includes a number of useful data types and library functions (see the \texttt{lib/} directory in the distribution). This chapter describes a few of these. The functions described here are imported automatically by every \Idris{} program, as part of \texttt{prelude.idr}. \subsubsection{\texttt{List} and \texttt{Vect}} We have already seen the \texttt{List} and \texttt{Vect} data types: \begin{SaveVerbatim}{listvec} data List a = Nil | (::) a (List a) data Vect : Set -> Nat -> Set where Nil : Vect a O (::) : a -> Vect a k -> Vect a (S k) \end{SaveVerbatim} \useverb{listvec} \noindent Note that the constructor names are the same for each --- constructor names (in fact, names in general) can be overloaded, provided that they are declared in different namespaces (see Section \ref{sect:namespaces}), and will typically be resolved according to their type. As syntactic sugar, any type with the constructor names \texttt{Nil} and \texttt{::} can be written in list form. For example: \begin{itemize} \item \texttt{[]} means \texttt{Nil} \item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil} \end{itemize} \noindent The library also defines a number of functions for manipulating these types. \texttt{map} is overloaded both for \texttt{List} and \texttt{Vect} and applies a function to every element of the list or vector. \begin{SaveVerbatim}{map} map : (a -> b) -> List a -> List b map f [] = [] map f (x :: xs) = f x :: map f xs map : (a -> b) -> Vect a n -> Vect b n map f [] = [] map f (x :: xs) = f x :: map f xs \end{SaveVerbatim} \useverb{map} \noindent For example, to double every element in a vector of integers: \begin{SaveVerbatim}{dvect} intVec : Vect Int 5 intVec = [1, 2, 3, 4, 5] double : Int -> Int double x = x * 2 \end{SaveVerbatim} \useverb{dvect} \noindent You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory: \begin{SaveVerbatim}{rundvect} *usefultypes> show (map double intVec) "[2, 4, 6, 8, 10]" : String \end{SaveVerbatim} \useverb{rundvect} \noindent For more details of the functions available on \texttt{List} and \texttt{Vect}, look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively. Functions include filtering, appending, reversing, and so on. Also remember that \Idris{} is still in development, so if you don't see the function you need, please feel free to add it and submit a patch! \subsubsection*{Aside: Anonymous functions and operator sections} There are actually neater ways to write the above expression. One way would be to use an anonymous function: \begin{SaveVerbatim}{lam1} *usefultypes> show (map (\x => x * 2) intVec) "[2, 4, 6, 8, 10]" : String \end{SaveVerbatim} \useverb{lam1} \noindent The notation \texttt{$\backslash$x => val} constructs an anonymous function which takes one argument, \texttt{x} and returns the expression \texttt{val}. Anonymous functions may take several arguments, separated by commas, e.g. \texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match, e.g. \texttt{$\backslash$ (x, y) => x + y}. We could also use an operator section: \begin{SaveVerbatim}{sec1} *usefultypes> show (map (* 2) intVec) "[2, 4, 6, 8, 10]" : String \end{SaveVerbatim} \useverb{sec1} \noindent \texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to \texttt{$\backslash$x => x * 2}. Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}. \subsubsection{Maybe} \texttt{Maybe} describes an optional value. Either there is a value of the given type, or there isn't: \begin{SaveVerbatim}{maybe} data Maybe a = Just a | Nothing \end{SaveVerbatim} \useverb{maybe} \noindent \texttt{Maybe} is one way of giving a type to an operation that may fail. For example, looking something up in a \texttt{List} (rather than a vector) may result in an out of bounds error: \begin{SaveVerbatim}{lookuplist} list_lookup : Nat -> List a -> Maybe a list_lookup _ Nil = Nothing list_lookup O (x :: xs) = Just x list_lookup (S k) (x :: xs) = list_lookup k xs \end{SaveVerbatim} \useverb{lookuplist} \noindent The \texttt{maybe} function is used to process values of type \texttt{Maybe}, either by applying a function to the value, if there is one, or by providing a default value: \begin{SaveVerbatim}{maybefn} maybe : Maybe a -> |(default:b) -> (a -> b) -> b \end{SaveVerbatim} \useverb{maybefn} \noindent The vertical bar $\mid$ before the default value is a laziness annotation. Normally expressions are evaluated before being passed to a function. This is typically the most efficient behaviour. However, in this case, the default value might not be used and if it is a large expression, evaluating it will be wasteful. The $\mid$ annotation tells the compiler not to evaluate the argument until it is needed. \subsubsection{Tuples and Dependent Pairs} Values can be paired with the following built-in data type: \begin{SaveVerbatim}{mkpair} data Pair a b = MkPair a b \end{SaveVerbatim} \useverb{mkpair} \noindent As syntactic sugar, we can write \texttt{(a, b)} which, according to context, means either \texttt{Pair a b} or \texttt{MkPair a b}. Tuples can contain an arbitrary number of values, represented as nested pairs: \begin{SaveVerbatim}{tuple} fred : (String, Int) fred = ("Fred", 42) jim : (String, Int, String) jim = ("Jim", 25, "Cambridge") \end{SaveVerbatim} \useverb{tuple} \subsubsection*{Dependent Pairs} Dependent pairs allow the type of the second element of a pair to depend on the value of the first element: \begin{SaveVerbatim}{sigma} data Exists : (A : Set) -> (P : A -> Set) -> Set where Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P \end{SaveVerbatim} \useverb{sigma} \noindent Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )} constructs a value of this type. For example, we can pair a number with a \texttt{Vect} of a particular length. \begin{SaveVerbatim}{dvec} vec : (n : Nat ** Vect Int n) vec = (2 ** [3, 4]) \end{SaveVerbatim} \useverb{dvec} \noindent The type checker could of course infer the value of the first element from the length of the vector. We can write an underscore \texttt{\_} in place of values which we expect the type checker to fill in, so the above definition could also be written as: \begin{SaveVerbatim}{dvec1} vec : (n : Nat ** Vect Int n) vec = (_ ** [3, 4]) \end{SaveVerbatim} \useverb{dvec1} \noindent We might also prefer to omit the type of the first element of the pair, since, again, it can be inferred: \begin{SaveVerbatim}{dvec2} vec : (n ** Vect Int n) vec = (_ ** [3, 4]) \end{SaveVerbatim} \useverb{dvec2} \noindent One use for dependent pairs is to return values of dependent types where the index is not necessarily known in advance. For example, if we filter elements out of a \texttt{Vect} according to some predicate, we will not know in advance what the length of the resulting vector will be: \begin{SaveVerbatim}{vfilter} filter : (a -> Bool) -> Vect a n -> (p ** Vect a p) \end{SaveVerbatim} \useverb{vfilter} \noindent If the \texttt{Vect} is empty, the result is easy: \begin{SaveVerbatim}{vfilternil} filter p Nil = (_ , []) \end{SaveVerbatim} \useverb{vfilternil} \noindent In the \texttt{::} case, we need to inspect the result of a recursive call to \texttt{filter} to extract the length and the vector from the result. To do this, we use \texttt{with} notation, which allows pattern matching on intermediate values: \begin{SaveVerbatim}{vfiltercons} filter p (x :: xs) with (filter p xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' ) \end{SaveVerbatim} \useverb{vfiltercons} \noindent We will see more on \texttt{with} notation later. \subsection{\texttt{so}} The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the value is true: \begin{SaveVerbatim}{sotype} data so : Bool -> Set where oh : so True \end{SaveVerbatim} \useverb{sotype} \noindent This is most useful for providing a static guarantee that a dynamic check has been made. For example, we might provide a safe interface to a function which draws a pixel on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that the point \texttt{(x,y)} is within the bounds of a 640x480 window: \begin{SaveVerbatim}{soexample} inBounds : Int -> Int -> Bool inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480 drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO () drawPoint x y oh = unsafeDrawPoint x y \end{SaveVerbatim} \useverb{soexample} \subsection{More Expressions} \subsubsection*{\texttt{let} bindings} Intermediate values can be calculated using \texttt{let} bindings: \begin{SaveVerbatim}{letb} mirror : List a -> List a mirror xs = let xs' = rev xs in app xs xs' \end{SaveVerbatim} \useverb{letb} \noindent We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract fields from a record as follows, as well as by pattern matching at the top level: \begin{SaveVerbatim}{letp} data Person = MkPerson String Int showPerson : Person -> String showPerson p = let MkPerson name age = p in name ++ " is " ++ show age ++ " years old" \end{SaveVerbatim} \useverb{letp} \subsubsection*{List comprehensions} \label{sec:listcomp} \Idris{} provides \emph{comprehension} notation as a convenient shorthand for building lists. The general form is: \begin{SaveVerbatim}{listcomp} [ expression | qualifiers ] \end{SaveVerbatim} \useverb{listcomp} \noindent This generates the list of values produced by evaluating the \texttt{expression}, according to the conditions given by the comma separated \texttt{qualifiers}. For example, we can build a list of Pythagorean triples as follows: \begin{SaveVerbatim}{triples} pythag : Int -> List (Int, Int, Int) pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y], x*x + y*y == z*z ] \end{SaveVerbatim} \useverb{triples} \noindent The \texttt{[a..b]} notation is another shorthand which builds a list of numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]} builds a list of numbers between \texttt{a} and \texttt{c} with the increment specified by the difference between \texttt{a} and \texttt{c}. This works for any numeric type, using the \texttt{count} function from the prelude. \subsubsection*{\texttt{case} expressions} Another way of inspecting intermediate values of \emph{simple} types is to use a \texttt{case} expression. The following function, for example, splits a string into two at a given character: \begin{SaveVerbatim}{split} splitAt : Char -> String -> (String, String) splitAt c x = case break (== c) x of (x, y) => (x, strTail y) \end{SaveVerbatim} \useverb{split} \noindent \texttt{break} is a library function which breaks a string into a pair of strings at the point where the given function returns true. We then deconstruct the pair it returns, and remove the first character of the second string. A \texttt{case} expression can match several cases, for example, to inspect an intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which looks up an index in a list, returning \texttt{Nothing} if the index is out of bounds. We can use this to write \texttt{lookup\_default}, which looks up an index and returns a default value if the index is out of bounds: \begin{SaveVerbatim}{listlookup} lookup_default : Nat -> List a -> a -> a lookup_default i xs def = case list_lookup i xs of Nothing => def Just x => x \end{SaveVerbatim} \useverb{listlookup} \noindent If the index is in bounds, we get the value at that index, otherwise we get a default value: \begin{SaveVerbatim}{deftest} *usefultypes> lookup_default 2 [3,4,5,6] (-1) 5 : Int *usefultypes> lookup_default 4 [3,4,5,6] (-1) -1 : Int \end{SaveVerbatim} \useverb{deftest} \noindent \textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis of intermediate expressions to avoid the need to write auxiliary functions, and is also used internally to implement pattern matching \texttt{let} and lambda bindings. It will \emph{only} work if: \begin{itemize} \item Each branch \emph{matches} a value of the same type, and \emph{returns} a value of the same type. \item The type of the result is known''. i.e. the type of the expression can be determined \emph{without} type checking the \texttt{case}-expression itself. \end{itemize} \subsection{Dependent Records} \remph{Records} are data types which collect several values (the record's \remph{fields}) together. \Idris{} provides syntax for defining records and automatically generating field access and update functions. For example, we can represent a person's name and age in a record: \begin{SaveVerbatim}{recsimpl} record Person : Set where MkPerson : (name : String) -> (age : Int) -> Person fred : Person fred = MkPerson "Fred" 30 \end{SaveVerbatim} \useverb{recsimpl} \noindent Record declarations are like \texttt{data} declarations, except that they are introduced by the \texttt{record} keyword, and can only have one constructor. The names of the binders in the constructor type (\texttt{name} and \texttt{age}) here are the field names, which we can use to access the field values: \begin{SaveVerbatim}{recaccess} *record> name fred "Fred" : String *record> age fred 30 : Int *record> :t name name : Person -> String \end{SaveVerbatim} \useverb{recaccess} \noindent We can also use the field names to update a record (or, more precisely, produce a new record with the given fields updates). \begin{SaveVerbatim}{recupdate} *record> record { name = "Jim" } fred MkPerson "Jim" 30 : Person *record> record { name = "Jim", age = 20 } fred MkPerson "Jim" 20 : Person \end{SaveVerbatim} \useverb{recupdate} \noindent The syntax \texttt{record \{ field = val, ... \}} generates a function which updates the given fields in a record. Records, and fields within records, can have dependent types. Updates are allowed to change the type of a field, provided that the result is well-typed, and the result does not affect the type of the record as a whole. For example: \begin{SaveVerbatim}{deprec} record Class : Set where ClassInfo : (students : Vect Person n) -> (className : String) -> Class \end{SaveVerbatim} \useverb{deprec} \noindent It is safe to update the \texttt{students} field to a vector of a different length because it will not affect the type of the record: \begin{SaveVerbatim}{addstu} addStudent : Person -> Class -> Class addStudent p c = record { students = p :: students c } c *record> addStudent fred (ClassInfo [] "CS") ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS" : Class \end{SaveVerbatim} \useverb{addstu}