git.iko.soy/Idris-dev
on e62b7ea help sign in
Idris-dev/tutorial/modules.tex
176 lines 5.6 kB history raw
1\section{Modules and Namespaces}
2\label{sect:namespaces}
4An \Idris{} program consists of a collection of modules. Each module includes
5an optional \texttt{module} declaration giving the name of the module, a
6list of \texttt{import} statements giving the other modules which are to be imported,
7and a collection of declarations and definitions of types, classes and functions.
8For example, Figure \ref{bstmod} gives a module which defines a binary
9tree 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.
13\begin{SaveVerbatim}{bstmod}
15module btree;
17data BTree a = Leaf
18 | Node (BTree a) a (BTree a);
20insert : Ord a => a -> BTree a -> BTree a;
21insert x Leaf = Node Leaf x Leaf;
22insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
23 else (Node l v (insert x r));
25toList : BTree a -> List a;
26toList Leaf = [];
27toList (Node l v r) = app (toList l) (v :: toList r);
29toTree : Ord a => List a -> BTree a;
30toTree [] = Leaf;
31toTree (x :: xs) = insert x (toTree xs);
33\end{SaveVerbatim}
34\codefig{bstmod}{Binary Tree module}
36\begin{SaveVerbatim}{bstmain}
38module main;
40import btree;
42main : IO ();
43main = do { let t = toTree [1,8,2,7,9,3];
44 print (toList t);
45 };
47\end{SaveVerbatim}
48\codefig{bstmain}{Binary Tree main program}
50The same names can be defined in multiple modules. This is possible because in practice names
51are \emph{qualified} with the name of the module.
52The names defined in the \texttt{btree} module are, in full:
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}
59\noindent
60If names are otherwise unambiguous, there is no need to give the fully qualified name.
61Names can be disambiguated either by giving an explicit qualification, or according to
62their type.
64There is no formal link between the module name and its filename, although it is generally
65advisable to use the same name for each. An \texttt{import} statement refers to a filename,
66using dots to separate directories. For example, \texttt{import foo.bar} would import
67the 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
69the \texttt{main} function, must be called \texttt{main} (though its filename need not be
70\texttt{main.idr}).
72\subsection{Export Modifiers}
74By default, all names defined in a module are exported for use by other modules.
75However, it is good practice only to export a minimal interface and keep internal
76details abstract. \Idris{} allows functions, types and classes to be marked
77as \texttt{public}, \texttt{abstract} or \texttt{private}:
79\begin{itemize}
80\item \texttt{public} means that both the name and definition are exported.
81For functions, this means that the implementation is exported (which means, for example,
82it can be used in a dependent type). For data types, this means that the type name and
83the constructors are exported. For classes, this means that the class name and
84method names are exported.
85\item \texttt{abstract} means that only the name is exported. For functions, this means
86that the implementation is not exported. For data types, this means that the type name
87is exported but not the constructors. For classes, this means that the class name is exported
88but not the method names/
89\item \texttt{private} means that neither the name nor the definition is exported.
90\end{itemize}
92\noindent
93If any definition is given an export modifier, then all names with no modifier are assumed
94to be \texttt{private}. For our \texttt{btree} module, it makes sense for the
95tree data type and the functions to be exported as \texttt{abstract}, as we see in
96Figure \ref{bstmodp}.
98\begin{SaveVerbatim}{bstmodp}
100module btree;
102abstract data BTree a = Leaf
103 | Node (BTree a) a (BTree a);
105abstract
106insert : Ord a => a -> BTree a -> BTree a;
107insert x Leaf = Node Leaf x Leaf;
108insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
109 else (Node l v (insert x r));
111abstract
112toList : BTree a -> List a;
113toList Leaf = [];
114toList (Node l v r) = app (toList l) (v :: toList r);
116abstract
117toTree : Ord a => List a -> BTree a;
118toTree [] = Leaf;
119toTree (x :: xs) = insert x (toTree xs);
121\end{SaveVerbatim}
122\codefig{bstmodp}{Binary Tree module, with export modifiers}
124\noindent
125Finally, the default export mode can be changed with the \texttt{\%access} directive,
126for example:
128\begin{SaveVerbatim}{access}
130%access abstract
132\end{SaveVerbatim}
133\useverb{access}
135\noindent
136In this case, any function with no access modifier will be exported as \texttt{abstract},
137rather than left \texttt{private}.
139\subsection{Explicit Namespaces}
141Defining a module also defines a namespace implicitly. However, namespaces can also
142be given \emph{explicitly}. This is most useful if you wish to overload names within
143the same module:
145\begin{SaveVerbatim}{nsfoo}
147module foo;
149namespace x {
150 test : Int -> Int;
151 test x = x * 2;
154namespace y {
155 test : String -> String;
156 test x = x ++ x;
159\end{SaveVerbatim}
160\useverb{nsfoo}
162\noindent
163This (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
165types:
167\begin{SaveVerbatim}{usetest}
169*foo> test 3
1706 : Int
171*foo> test "foo"
172"foofoo" : String
174\end{SaveVerbatim}
175\useverb{usetest}