git.iko.soy/Idris-dev
on 95ff97c help sign in
Idris-dev/tutorial/modules.tex
174 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)
46\end{SaveVerbatim}
47\codefig{bstmain}{Binary Tree main program}
49\noindent
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
153namespace y
154 test : String -> String
155 test x = x ++ x
157\end{SaveVerbatim}
158\useverb{nsfoo}
160\noindent
161This (admittedly contrived) module defines two functions with fully qualified names
162\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their
163types:
165\begin{SaveVerbatim}{usetest}
167*foo> test 3
1686 : Int
169*foo> test "foo"
170"foofoo" : String
172\end{SaveVerbatim}
173\useverb{usetest}