git.iko.soy/Idris-dev
on a332d4e help sign in
Idris-dev/tutorial/modules.tex
231 lines 7.1 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) = 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
65is generally advisable to use the same name for each. An \texttt{import}
66statement refers to a filename, using dots to separate directories. For
67example, \texttt{import foo.bar} would import the file \texttt{foo/bar.idr},
68which would conventionally have the module declaration \texttt{module foo.bar}.
69The only requirement for module names is that the main module, with the
70\texttt{main} function, must be called \texttt{Main} (though its filename need
71not be \texttt{Main.idr}).
73\subsection{Export Modifiers}
75By default, all names defined in a module are exported for use by other modules.
76However, it is good practice only to export a minimal interface and keep internal
77details abstract. \Idris{} allows functions, types and classes to be marked
78as \texttt{public}, \texttt{abstract} or \texttt{private}:
80\begin{itemize}
81\item \texttt{public} means that both the name and definition are exported.
82For functions, this means that the implementation is exported (which means, for example,
83it can be used in a dependent type). For data types, this means that the type name and
84the constructors are exported. For classes, this means that the class name and
85method names are exported.
86\item \texttt{abstract} means that only the name is exported. For functions, this means
87that the implementation is not exported. For data types, this means that the type name
88is exported but not the constructors. For classes, this means that the class name is exported
89but not the method names.
90\item \texttt{private} means that neither the name nor the definition is exported.
91\end{itemize}
93\noindent
94If any definition is given an export modifier, then all names with no modifier are assumed
95to be \texttt{private}. For our \texttt{btree} module, it makes sense for the
96tree data type and the functions to be exported as \texttt{abstract}, as we see in
97Figure \ref{bstmodp}.
99\begin{SaveVerbatim}{bstmodp}
101module btree
103abstract data BTree a = Leaf
104 | Node (BTree a) a (BTree a)
106abstract
107insert : Ord a => a -> BTree a -> BTree a
108insert x Leaf = Node Leaf x Leaf
109insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
110 else (Node l v (insert x r))
112abstract
113toList : BTree a -> List a
114toList Leaf = []
115toList (Node l v r) = app (toList l) (v :: toList r)
117abstract
118toTree : Ord a => List a -> BTree a
119toTree [] = Leaf
120toTree (x :: xs) = insert x (toTree xs)
122\end{SaveVerbatim}
123\codefig{bstmodp}{Binary Tree module, with export modifiers}
125\noindent
126Finally, the default export mode can be changed with the \texttt{\%access} directive,
127for example:
129\begin{SaveVerbatim}{access}
131%access abstract
133\end{SaveVerbatim}
134\useverb{access}
136\noindent
137In this case, any function with no access modifier will be exported as \texttt{abstract},
138rather than left \texttt{private}.
140\subsection{Explicit Namespaces}
142Defining a module also defines a namespace implicitly. However, namespaces can also
143be given \emph{explicitly}. This is most useful if you wish to overload names within
144the same module:
146\begin{SaveVerbatim}{nsfoo}
148module foo
150namespace x
151 test : Int -> Int
152 test x = x * 2
154namespace y
155 test : String -> String
156 test x = x ++ x
158\end{SaveVerbatim}
159\useverb{nsfoo}
161\noindent
162This (admittedly contrived) module defines two functions with fully qualified names
163\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their
164types:
166\begin{SaveVerbatim}{usetest}
168*foo> test 3
1696 : Int
170*foo> test "foo"
171"foofoo" : String
173\end{SaveVerbatim}
174\useverb{usetest}
176\subsection{Parameterised blocks}
178Groups of functions can be parameterised over a number of arguments using a
179\texttt{parameters} declaration, for example:
181\begin{SaveVerbatim}{paramex}
183parameters (x : Nat, y : Nat)
184 addAll : Nat -> Nat
185 addAll z = x + y + z
187\end{SaveVerbatim}
188\useverb{paramex}
190\noindent
191The effect of a \texttt{parameters} block is to add the declared parameters to every
192function, type and data constructor within the block. Outside the block, the parameters
193must be given explicitly:
195\begin{SaveVerbatim}{addall}
197*params> :t addAll
198addAll : Nat -> Nat -> Nat -> Nat
200\end{SaveVerbatim}
201\useverb{addall}
203\noindent
204Parameters blocks can be nested, and can also include data declarations, in
205which case the parameters are added explicitly to all type and data
206constructors. They may also be dependent types with implicit arguments:
208\begin{SaveVerbatim}{paramdata}
210parameters (xs : Vect a x, y : Nat)
211 data Vects : Type -> Type where
212 MkVects : Vect a y -> Vects a
214 append : Vects a -> Vect a (x + y)
215 append (MkVects ys) = xs ++ ys
217\end{SaveVerbatim}
218\useverb{paramdata}
220\noindent
221To use \texttt{Vects} or \texttt{append} outside the block, we must also
222give the \texttt{xs} and \texttt{y} arguments. Here, we can use placeholders for
223the values which can be inferred by the type checker:
225\begin{SaveVerbatim}{paramuse}
227*params> show (append _ _ (MkVects [1,2,3] _ [4,5,6]))
228"[1, 2, 3, 4, 5, 6]" : String
230\end{SaveVerbatim}
231\useverb{paramuse}