@@ -1,4 +1,176 @@
11\section{Modules and Namespaces}
22\label{sect:namespaces}
33
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}
4176