git.iko.soy/Idris-dev
on master help sign in
Modules and namespaces section in tutorial
17ad913Edwin Brady
lib/prelude/list.idr+4
compare with master
unifiedsplit
@@ -16,6 +16,10 @@ rev xs = revAcc [] xs where {
16 revAcc acc (x :: xs) = revAcc (x :: acc) xs;
16 revAcc acc (x :: xs) = revAcc (x :: acc) xs;
17}
17}
18
18
19+app : List a -> List a -> List a;
20+app [] xs = xs;
21+app (x :: xs) ys = x :: app xs ys;
22+
19length : List a -> Int;
23length : List a -> Int;
20length [] = 0;
24length [] = 0;
21length (x :: xs) = 1 + length xs;
25length (x :: xs) = 1 + length xs;
tutorial/classes.tex+16−1
@@ -158,13 +158,28 @@ The \texttt{Ord} class allows us to compare two values and determine their order
158Only the \texttt{compare} method is required; every other method has a default definition.
158Only the \texttt{compare} method is required; every other method has a default definition.
159Using
159Using
160this we can write functions such as \texttt{sort}, a function which sorts a list into
160this we can write functions such as \texttt{sort}, a function which sorts a list into
161−increasing order, provided that the element type of the list is in the \texttt{Ord} class:
161+increasing order, provided that the element type of the list is in the \texttt{Ord} class.
162+We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
163+function type to the right of the fat arrow:
162
164
163\begin{SaveVerbatim}{sortty}
165\begin{SaveVerbatim}{sortty}
164
166
165sort : Ord a => List a -> List a;
167sort : Ord a => List a -> List a;
166
168
167\end{SaveVerbatim}
169\end{SaveVerbatim}
170+\useverb{sortty}
171+
172+\noindent
173+Functions, classes and instances can have multiple constraints. Multiple constaints are
174+written in brackets in a comma separated list, for example:
175+
176+\begin{SaveVerbatim}{sortshow}
177+
178+sortAndShow : (Ord a, Show a) => List a -> String;
179+sortAndShow xs = show (sort xs);
180+
181+\end{SaveVerbatim}
182+\useverb{sortshow}
168
183
169\subsection{Monads and \texttt{do}-notation}
184\subsection{Monads and \texttt{do}-notation}
170
185
tutorial/examples/bmain.idrnew file+9
@@ -0,0 +1,9 @@
1+module main;
2+
3+import btree;
4+
5+main : IO ();
6+main = do { let t = toTree [1,8,2,7,9,3];
7+ print (toList t);
8+ };
9+
tutorial/examples/btree.idrnew file+18
@@ -0,0 +1,18 @@
1+module btree;
2+
3+data BTree a = Leaf
4+ | Node (BTree a) a (BTree a);
5+
6+insert : Ord a => a -> BTree a -> BTree a;
7+insert x Leaf = Node Leaf x Leaf;
8+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
9+ else (Node l v (insert x r));
10+
11+toList : BTree a -> List a;
12+toList Leaf = [];
13+toList (Node l v r) = app (toList l) (v :: toList r);
14+
15+toTree : Ord a => List a -> BTree a;
16+toTree [] = Leaf;
17+toTree (x :: xs) = insert x (toTree xs);
18+
tutorial/examples/classes.idr+3
@@ -3,3 +3,6 @@ m_add x y = do { x' <- x; -- Extract value from x
3 y' <- y; -- Extract value from y
3 y' <- y; -- Extract value from y
4 return (x' + y'); -- Add them
4 return (x' + y'); -- Add them
5 };
5 };
6+
7+sortAndShow : (Ord a, Show a) => List a -> String;
8+sortAndShow xs = show (sort xs);
tutorial/examples/foo.idrnew file+12
@@ -0,0 +1,12 @@
1+module foo;
2+
3+namespace x {
4+ test : Int -> Int;
5+ test x = x * 2;
6+}
7+
8+namespace y {
9+ test : String -> String;
10+ test x = x ++ x;
11+}
12+
tutorial/modules.tex+172
@@ -1,4 +1,176 @@
1\section{Modules and Namespaces}
1\section{Modules and Namespaces}
2\label{sect:namespaces}
2\label{sect:namespaces}
3
3
4+An \Idris{} program consists of a collection of modules. Each module includes
5+an optional \texttt{module} declaration giving the name of the module, a
6+list of \texttt{import} statements giving the other modules which are to be imported,
7+and a collection of declarations and definitions of types, classes and functions.
8+For example, Figure \ref{bstmod} gives a module which defines a binary
9+tree type \texttt{BTree} (in a file \texttt{btree.idr}) and Figure
10+\ref{bstmain} gives a main program (in a file \texttt{bmain.idr} which uses the
11+\texttt{bst} module to sort a list.
12+
13+\begin{SaveVerbatim}{bstmod}
14+
15+module btree;
16+
17+data BTree a = Leaf
18+ | Node (BTree a) a (BTree a);
19+
20+insert : Ord a => a -> BTree a -> BTree a;
21+insert x Leaf = Node Leaf x Leaf;
22+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
23+ else (Node l v (insert x r));
24+
25+toList : BTree a -> List a;
26+toList Leaf = [];
27+toList (Node l v r) = app (toList l) (v :: toList r);
28+
29+toTree : Ord a => List a -> BTree a;
30+toTree [] = Leaf;
31+toTree (x :: xs) = insert x (toTree xs);
32+
33+\end{SaveVerbatim}
34+\codefig{bstmod}{Binary Tree module}
35+
36+\begin{SaveVerbatim}{bstmain}
37+
38+module main;
39+
40+import btree;
41+
42+main : IO ();
43+main = do { let t = toTree [1,8,2,7,9,3];
44+ print (toList t);
45+ };
46+
47+\end{SaveVerbatim}
48+\codefig{bstmain}{Binary Tree main program}
49+
50+The same names can be defined in multiple modules. This is possible because in practice names
51+are \emph{qualified} with the name of the module.
52+The names defined in the \texttt{btree} module are, in full:
53+
54+\begin{itemize}
55+\item \texttt{btree.BTree}, \texttt{btree.Leaf}, \texttt{btree.Node}, \texttt{btree.insert},
56+\texttt{btree.toList} and \texttt{btree.toTree}.
57+\end{itemize}
58+
59+\noindent
60+If names are otherwise unambiguous, there is no need to give the fully qualified name.
61+Names can be disambiguated either by giving an explicit qualification, or according to
62+their type.
63+
64+There is no formal link between the module name and its filename, although it is generally
65+advisable to use the same name for each. An \texttt{import} statement refers to a filename,
66+using dots to separate directories. For example, \texttt{import foo.bar} would import
67+the file \texttt{foo/bar.idr}, which would conventionally have the module declaration
68+\texttt{module foo.bar}. The only requirement for module names is that the main module, with
69+the \texttt{main} function, must be called \texttt{main} (though its filename need not be
70+\texttt{main.idr}).
71+
72+\subsection{Export Modifiers}
73+
74+By default, all names defined in a module are exported for use by other modules.
75+However, it is good practice only to export a minimal interface and keep internal
76+details abstract. \Idris{} allows functions, types and classes to be marked
77+as \texttt{public}, \texttt{abstract} or \texttt{private}:
78+
79+\begin{itemize}
80+\item \texttt{public} means that both the name and definition are exported.
81+For functions, this means that the implementation is exported (which means, for example,
82+it can be used in a dependent type). For data types, this means that the type name and
83+the constructors are exported. For classes, this means that the class name and
84+method names are exported.
85+\item \texttt{abstract} means that only the name is exported. For functions, this means
86+that the implementation is not exported. For data types, this means that the type name
87+is exported but not the constructors. For classes, this means that the class name is exported
88+but not the method names/
89+\item \texttt{private} means that neither the name nor the definition is exported.
90+\end{itemize}
91+
92+\noindent
93+If any definition is given an export modifier, then all names with no modifier are assumed
94+to be \texttt{private}. For our \texttt{btree} module, it makes sense for the
95+tree data type and the functions to be exported as \texttt{abstract}, as we see in
96+Figure \ref{bstmodp}.
97+
98+\begin{SaveVerbatim}{bstmodp}
99+
100+module btree;
101+
102+abstract data BTree a = Leaf
103+ | Node (BTree a) a (BTree a);
104+
105+abstract
106+insert : Ord a => a -> BTree a -> BTree a;
107+insert x Leaf = Node Leaf x Leaf;
108+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
109+ else (Node l v (insert x r));
110+
111+abstract
112+toList : BTree a -> List a;
113+toList Leaf = [];
114+toList (Node l v r) = app (toList l) (v :: toList r);
115+
116+abstract
117+toTree : Ord a => List a -> BTree a;
118+toTree [] = Leaf;
119+toTree (x :: xs) = insert x (toTree xs);
120+
121+\end{SaveVerbatim}
122+\codefig{bstmodp}{Binary Tree module, with export modifiers}
123+
124+\noindent
125+Finally, the default export mode can be changed with the \texttt{\%access} directive,
126+for example:
127+
128+\begin{SaveVerbatim}{access}
129+
130+%access abstract
131+
132+\end{SaveVerbatim}
133+\useverb{access}
134+
135+\noindent
136+In this case, any function with no access modifier will be exported as \texttt{abstract},
137+rather than left \texttt{private}.
138+
139+\subsection{Explicit Namespaces}
140+
141+Defining a module also defines a namespace implicitly. However, namespaces can also
142+be given \emph{explicitly}. This is most useful if you wish to overload names within
143+the same module:
144+
145+\begin{SaveVerbatim}{nsfoo}
146+
147+module foo;
148+
149+namespace x {
150+ test : Int -> Int;
151+ test x = x * 2;
152+}
153+
154+namespace y {
155+ test : String -> String;
156+ test x = x ++ x;
157+}
158+
159+\end{SaveVerbatim}
160+\useverb{nsfoo}
161+
162+\noindent
163+This (admittedly contrived) module defines two functions with fully qualified names
164+\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their
165+types:
166+
167+\begin{SaveVerbatim}{usetest}
168+
169+*foo> test 3
170+6 : Int
171+*foo> test "foo"
172+"foofoo" : String
173+
174+\end{SaveVerbatim}
175+\useverb{usetest}
4
176