git.iko.soy/Idris-dev
on e2d0099 help sign in
Idris-dev/tutorial/typesfuns.tex
306 lines 10 kB history raw
1\section{Language Overview}
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}
16module prims;
18x : Int;
19x = 42;
21foo : String;
22foo = "Sausage machine";
24bar : Char;
25bar = 'Z';
27quux : Bool;
28quux = False;
30\end{SaveVerbatim}
31\useverb{constprims}
33An \Idris{} file consists of an optional module declaration (here
34\texttt{module prims}) followed by an optional list of imports (none here,
35however \Idris{} programs can consist of several modules, and the definitions
36in each module each have their own namespace, as we will discuss shortly) and a
37collection of declarations and definitions. Each definition must have a type
38declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc). Each
39component is separated by a semi-colon.
41A library module \texttt{prelude} is automatically imported by every \Idris{} program,
42including facilities for IO, arithmetic, data structures and various common
43functions. The prelude defines several arithmetic and comparison operators,
44which we can use at the prompt. Evaluating things at the prompt gives an
45answer, and the type of the answer. For example:
47\begin{SaveVerbatim}{promptprim}
49*prims> 6*6+6
5042 : Int
51*prims> x == 6*6+6
52True : Bool
54\end{SaveVerbatim}
55\useverb{promptprim}
57All of the usual arithmetic and comparison operators are defined for the primitive
58types. They are overloaded using type classes, as we will discuss in section
59\ref{sec:classes} and can be extended to work on user defined types.
60Boolean expressions can be tested with the \texttt{if...then...else} construct:
62\begin{SaveVerbatim}{ifthenelse}
64*prims> if (x==6*6+6) then "The answer!" else "Not the answer"
65"The answer!" : String
67\end{SaveVerbatim}
68\useverb{ifthenelse}
70\subsection{Data Types}
72Data types are declared in a similar way to Haskell data types, with a similar
73syntax. The main difference is that Idris syntax is not whitespace sensitive,
74and declarations must end with a semi-colon. Natural numbers and lists, for
75example, can be declared as follows:
77\begin{SaveVerbatim}{natlist}
79data Nat = O | S Nat; -- Natural numbers
80 -- (zero and successor)
81data List a = Nil | (::) a (List a); -- Polymorphic lists
83\end{SaveVerbatim}
84\useverb{natlist}
86The above declarations are taken from the standard library. Unary natural
87numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
88the successor of another natural number (\texttt{S k}).
89Lists can either be empty (\texttt{Nil})
90or a value added to the front of another list (\texttt{x :: xs}).
91In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
92such as this can be added using a fixity declaration, as follows:
94\begin{SaveVerbatim}{infixcons}
96infixr 7 :: ;
98\end{SaveVerbatim}
99\useverb{infixcons}
101Functions, data constructors and type constuctors may all be given infix
102operators as names. They may be used in prefix form if enclosed in brackets,
103e.g. (::). Infix operators can use any of the symbols:
105\begin{SaveVerbatim}{infixsyms}
107:+-*/=_.?|&><!@$%^~.
109\end{SaveVerbatim}
110\useverb{infixsyms}
112\subsection{Functions}
114Functions are implemented by pattern matching, again using a similar syntax to
115Haskell. The main difference is that \Idris{} requires type declarations for all
116functions, using a single colon \texttt{:} (rather than
117Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
118defined as follows, again taken from the standard library:
120\begin{SaveVerbatim}{natfns}
122-- Unary addition
123plus : Nat -> Nat -> Nat;
124plus O y = y;
125plus (S k) y = S (plus k y);
127-- Unary multiplication
128mult : Nat -> Nat -> Nat;
129mult O y = O;
130mult (S k) y = plus y (mult k y);
132\end{SaveVerbatim}
133\useverb{natfns}
135The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded for
136use by \texttt{Nat}, and are implemented using the above functions.
137Unlike Haskell, there is no restriction on whether types and function names
138must begin with a capital letter or not. Function names (\tFN{plus} and \tFN{mult} above),
139data constructors (\tDC{O}, \tDC{S}, \tDC{Nil} and \tDC{::}) and type
140constructors (\tTC{Nat} and \tTC{List}) are
141all part of the same namespace.
143We can test these functions at the Idris prompt:
145\begin{SaveVerbatim}{fntest}
147Idris> plus (S (S O)) (S (S O))
148S (S (S (S O))) : Nat
149Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
150S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
152\end{SaveVerbatim}
153\useverb{fntest}
155Like arithmetic operations, integer literals are also overloaded using type classes,
156meaning that we can also test the functions as follows:
158\begin{SaveVerbatim}{fntest}
160Idris> plus 2 2
161S (S (S (S O))) : Nat
162Idris> mult 3 (plus 2 2)
163S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
165\end{SaveVerbatim}
166\useverb{fntest}
168You may wonder, by the way, why we have unary natural numbers when our
169computers have perfectly good integer arithmetic built in. The reason is
170primarily that unary numbers have a very convenient structure which is easy to
171reason about, and easy to relate to other data structures as we will see later.
172Nevertheless, we do not want this convenience to be at the expense of
173efficiency. Fortunately, \Idris{} knows about the relationship between
174\tTC{Nat} (and similarly structured types) and numbers, so optimises the
175representation and functions such as \tFN{plus} and \tFN{mult}.
177\subsection{Dependent Types}
179\subsubsection{Vectors}
181A standard example of a dependent type is the type of ``lists with length'',
182conventionally called vectors in the dependent type literature. In \Idris{},
183we declare vectors as follows:
185\begin{SaveVerbatim}{vect}
187data Vect : Set -> Nat -> Set where
188 Nil : Vect a O
189 | (::) : a -> Vect a k -> Vect a (S k);
191\end{SaveVerbatim}
192\useverb{vect}
194Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
195name overloading such as this is accepted by \Idris{}, provided that the names
196are declared in different namespaces (in practice, normally in different modules).
197Ambiguous constructor names can normally be resolved from context.
199This declares a family of types, and so the form of the declaration is rather
200different from the simple type declarations above. We explicitly state the type
201of the type constructor \tTC{Vect} - it takes a type and a \tTC{Nat} as an
202argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}
203is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
204constructor targets a different part of the family of types. \tDC{Nil} can only
205be used to construct vectors with zero length, and \tDC{::} to constructor
206vectors with non-zero length.
208We can define functions on dependent types such as \tTC{Vect} in the same way
209as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
210The type of a function over \tTC{Vect} will describe what happens to the
211lengths of the vectors involved. For example, \tFN{app}, defined in the
212library, appends two \tTC{Vect}s:
214\begin{SaveVerbatim}{vapp}
216app : Vect A n -> Vect A m -> Vect A (n + m);
217app Nil ys = ys;
218app (x :: xs) ys = x :: app xs ys;
220\end{SaveVerbatim}
221\useverb{vapp}
223The type of \tFN{app} states that the resulting vector's length will be the sum of
224the input lengths. If we get the definition wrong in such a way that this does
225not hold, \Idris{} will not accept the definition. For example:
227\begin{SaveVerbatim}{vapperr}
229app : Vect a n -> Vect a m -> Vect a (n + m);
230app Nil ys = ys;
231app (x :: xs) ys = x :: app xs xs; -- BROKEN
233\end{SaveVerbatim}
234\useverb{vapperr}
236\begin{SaveVerbatim}{vapperrmsg}
238$ idris app.idr --check
239app.idr:3:Can't unify Vect a m with Vect a (plus n m)
241\end{SaveVerbatim}
242\useverb{vapperrmsg}
243%$
245This error message suggests that there is a length mismatch between two vectors.
246Note that the terms in the error message have been \emph{normalised}, so in
247particular \texttt{n + m} has been reduced to \texttt{plus n m}.
249\subsubsection{The Finite Sets}
251Finite sets, as the name suggests, are sets with a finite number of elements.
252They are declared as follows (again, in the prelude):
254\begin{SaveVerbatim}{findecl}
256data Fin : Nat -> Set where
257 fO : Fin (S k)
258 | fS : Fin k -> Fin (S k);
260\end{SaveVerbatim}
261\useverb{findecl}
263\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
264\texttt{fS n} is the
265\texttt{n+1}th element of a finite set with \texttt{S k} elements.
266\tTC{Fin} is indexed by a \tTC{Nat}, which
267represents the number of elements in the set. Obviously we can't construct an
268element of an empty set, so neither constructor targets \texttt{Fin O}.
270A useful application of the \tTC{Fin} family is to represent numbers with
271guaranteed bounds. For example, the following function which looks up an element in a \tTC{Vect}
272is defined in the prelude:
274\begin{SaveVerbatim}{vlookup}
276lookup : Fin n -> Vect a n -> a;
277lookup fO (x :: xs) = x;
278lookup (fS k) (x :: xs) = lookup k xs;
280\end{SaveVerbatim}
281\useverb{vlookup}
283This function looks up a value at a given location in a vector. The location is
284bounded by the length of the vector (\texttt{n} in each case), so there is no
285need for a run-time bounds check. The type checker guarantees that the location
286is no larger than the length of the vector.
288Note also that there is no case for \texttt{Nil} here. This is because it is
289impossible. Since there is no element of \texttt{Fin O}, and the location is a
290\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
291look up an element in an empty vector would give a compile time type error,
292since it would force \texttt{n} to be \tDC{O}.
294\subsubsection{Dependent Function Types}
296\subsubsection{Implicit Arguments}
298\subsection{Useful Data Types}
300Lists, syntactic sugar.
301Maybe, Either.
302Pairs, dependent pairs, syntactic sugar.
304\subsection{I/O}
306\subsection{Modules and Namespaces}