git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/content/modules.tex
201 lines 6.8 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{code}[caption={Binary Tree module}, label=bstmod]
14module btree
16data BTree a = Leaf
17 | Node (BTree a) a (BTree a)
19insert : Ord a => a -> BTree a -> BTree a
20insert x Leaf = Node Leaf x Leaf
21insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
22 else (Node l v (insert x r))
24toList : BTree a -> List a
25toList Leaf = []
26toList (Node l v r) = toList l ++ (v :: toList r)
28toTree : Ord a => List a -> BTree a
29toTree [] = Leaf
30toTree (x :: xs) = insert x (toTree xs)
31\end{code}
33\begin{code}[caption={Binary Tree main program},label=bstmain]
34module Main
36import btree
38main : IO ()
39main = do let t = toTree [1,8,2,7,9,3]
40 print (toList t)
41\end{code}
43\noindent
44The same names can be defined in multiple modules. This is possible because in practice names
45are \emph{qualified} with the name of the module.
46The names defined in the \texttt{btree} module are, in full:
48\begin{itemize}
49\item \texttt{btree.BTree}, \texttt{btree.Leaf}, \texttt{btree.Node}, \texttt{btree.insert},
50\texttt{btree.toList} and \texttt{btree.toTree}.
51\end{itemize}
53\noindent
54If names are otherwise unambiguous, there is no need to give the fully qualified name.
55Names can be disambiguated either by giving an explicit qualification, or according to
56their type.
58There is no formal link between the module name and its filename, although it
59is generally advisable to use the same name for each. An \texttt{import}
60statement refers to a filename, using dots to separate directories. For
61example, \texttt{import foo.bar} would import the file \texttt{foo/bar.idr},
62which would conventionally have the module declaration \texttt{module foo.bar}.
63The only requirement for module names is that the main module, with the
64\texttt{main} function, must be called \texttt{Main} (though its filename need
65not be \texttt{Main.idr}).
67\subsection{Export Modifiers}
69By default, all names defined in a module are exported for use by other modules.
70However, it is good practice only to export a minimal interface and keep internal
71details abstract. \Idris{} allows functions, types and classes to be marked
72as \texttt{public}, \texttt{abstract} or \texttt{private}:
74\begin{itemize}
75\item \texttt{public} means that both the name and definition are exported.
76For functions, this means that the implementation is exported (which means, for example,
77it can be used in a dependent type). For data types, this means that the type name and
78the constructors are exported. For classes, this means that the class name and
79method names are exported.
80\item \texttt{abstract} means that only the name is exported. For functions, this means
81that the implementation is not exported. For data types, this means that the type name
82is exported but not the constructors. For classes, this means that the class name is exported
83but not the method names.
84\item \texttt{private} means that neither the name nor the definition is exported.
85\end{itemize}
87\noindent
88If any definition is given an export modifier, then all names with no modifier are assumed
89to be \texttt{private}. For our \texttt{btree} module, it makes sense for the
90tree data type and the functions to be exported as \texttt{abstract}, as we see in
91Figure \ref{bstmodp}.
93\begin{code}[caption={Binary Tree module, with export modifiers}, label=bstmodp]
94module btree
96abstract data BTree a = Leaf
97 | Node (BTree a) a (BTree a)
99abstract
100insert : Ord a => a -> BTree a -> BTree a
101insert x Leaf = Node Leaf x Leaf
102insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
103 else (Node l v (insert x r))
105abstract
106toList : BTree a -> List a
107toList Leaf = []
108toList (Node l v r) = app (toList l) (v :: toList r)
110abstract
111toTree : Ord a => List a -> BTree a
112toTree [] = Leaf
113toTree (x :: xs) = insert x (toTree xs)
114\end{code}
116\noindent
117Finally, the default export mode can be changed with the \texttt{\%access} directive,
118for example:
120\begin{code}
121%access abstract
122\end{code}
124\noindent
125In this case, any function with no access modifier will be exported as \texttt{abstract},
126rather than left \texttt{private}.
128\subsection{Explicit Namespaces}
130Defining a module also defines a namespace implicitly. However, namespaces can also
131be given \emph{explicitly}. This is most useful if you wish to overload names within
132the same module:
134\begin{code}
135module foo
137namespace x
138 test : Int -> Int
139 test x = x * 2
141namespace y
142 test : String -> String
143 test x = x ++ x
144\end{code}
146\noindent
147This (admittedly contrived) module defines two functions with fully qualified names
148\texttt{foo.x.test} and \texttt{foo.y.test}, which can be disambiguated by their
149types:
151\begin{lstlisting}
152*foo> test 3
1536 : Int
154*foo> test "foo"
155"foofoo" : String
156\end{lstlisting}
158\subsection{Parameterised blocks}
160Groups of functions can be parameterised over a number of arguments using a
161\texttt{parameters} declaration, for example:
163\begin{code}
164parameters (x : Nat, y : Nat)
165 addAll : Nat -> Nat
166 addAll z = x + y + z
167\end{code}
169\noindent
170The effect of a \texttt{parameters} block is to add the declared parameters to every
171function, type and data constructor within the block. Outside the block, the parameters
172must be given explicitly:
174\begin{lstlisting}
175*params> :t addAll
176addAll : Nat -> Nat -> Nat -> Nat
177\end{lstlisting}
179\noindent
180Parameters blocks can be nested, and can also include data declarations, in
181which case the parameters are added explicitly to all type and data
182constructors. They may also be dependent types with implicit arguments:
184\begin{code}
185parameters (xs : Vect x a, y : Nat)
186 data Vects : Type -> Type where
187 MkVects : Vect a y -> Vects a
189 append : Vects a -> Vect (x + y) a
190 append (MkVects ys) = xs ++ ys
191\end{code}
193\noindent
194To use \texttt{Vects} or \texttt{append} outside the block, we must also
195give the \texttt{xs} and \texttt{y} arguments. Here, we can use placeholders for
196the values which can be inferred by the type checker:
198\begin{lstlisting}
199*params> show (append _ _ (MkVects [1,2,3] _ [4,5,6]))
200"[1, 2, 3, 4, 5, 6]" : String
201\end{lstlisting}