git.iko.soy/Idris-dev
on cd4e91d help sign in
Idris-dev/docs/tutorial/modules.rst
243 lines 7.4 kB history raw
1.. _sect-namespaces:
3**********************
4Modules and Namespaces
5**********************
7An Idris program consists of a collection of modules. Each module
8includes an optional ``module`` declaration giving the name of the
9module, a list of ``import`` statements giving the other modules which
10are to be imported, and a collection of declarations and definitions of
11types, classes and functions. For example, the listing below gives a
12module which defines a binary tree type ``BTree`` (in a file
13``Btree.idr``):
15.. code-block:: idris
17 module Btree
19 data BTree a = Leaf
20 | Node (BTree a) a (BTree a)
22 insert : Ord a => a -> BTree a -> BTree a
23 insert x Leaf = Node Leaf x Leaf
24 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
25 else (Node l v (insert x r))
27 toList : BTree a -> List a
28 toList Leaf = []
29 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
31 toTree : Ord a => List a -> BTree a
32 toTree [] = Leaf
33 toTree (x :: xs) = insert x (toTree xs)
36Then, this gives a main program (in a file
37``bmain.idr``) which uses the ``bst`` module to sort a list:
39.. code-block:: idris
41 module Main
43 import Btree
45 main : IO ()
46 main = do let t = toTree [1,8,2,7,9,3]
47 print (Btree.toList t)
51The same names can be defined in multiple modules. This is possible
52because in practice names are *qualified* with the name of the module.
53The names defined in the ``btree`` module are, in full:
55+ ``Btree.BTree``
56+ ``Btree.Leaf``
57+ ``Btree.Node``
58+ ``Btree.insert``
59+ ``Btree.toList``
60+ ``Btree.toTree``
62If names are otherwise unambiguous, there is no need to give the fully
63qualified name. Names can be disambiguated either by giving an explicit
64qualification, or according to their type.
66There is no formal link between the module name and its filename,
67although it is generally advisable to use the same name for each. An
68``import`` statement refers to a filename, using dots to separate
69directories. For example, ``import foo.bar`` would import the file
70``foo/bar.idr``, which would conventionally have the module declaration
71``module foo.bar``. The only requirement for module names is that the
72main module, with the ``main`` function, must be called
73``Main``—although its filename need not be ``Main.idr``.
75Export Modifiers
76================
78By default, all names defined in a module are exported for use by other
79modules. However, it is good practice only to export a minimal interface
80and keep internal details abstract. Idris allows functions, types,
81and classes to be marked as: ``public``, ``abstract`` or ``private``:
83- ``public`` means that both the name and definition are exported. For
84 functions, this means that the implementation is exported (which
85 means, for example, it can be used in a dependent type). For data
86 types, this means that the type name and the constructors are
87 exported. For classes, this means that the class name and method
88 names are exported.
90- ``abstract`` means that only the name is exported. For functions,
91 this means that the implementation is not exported. For data types,
92 this means that the type name is exported but not the constructors.
93 For classes, this means that the class name is exported but not the
94 method names.
96- ``private`` means that neither the name nor the definition is
97 exported.
99.. note::
100 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
102For our ``btree`` module, it makes sense for the tree data type and the
103functions to be exported as ``abstract``, as we see below:
105.. code-block:: idris
107 module Btree
109 abstract data BTree a = Leaf
110 | Node (BTree a) a (BTree a)
112 abstract
113 insert : Ord a => a -> BTree a -> BTree a
114 insert x Leaf = Node Leaf x Leaf
115 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
116 else (Node l v (insert x r))
118 abstract
119 toList : BTree a -> List a
120 toList Leaf = []
121 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
123 abstract
124 toTree : Ord a => List a -> BTree a
125 toTree [] = Leaf
126 toTree (x :: xs) = insert x (toTree xs)
128Finally, the default export mode can be changed with the ``%access``
129directive, for example:
131.. code-block:: idris
133 module Btree
135 %access abstract
137 data BTree a = Leaf
138 | Node (BTree a) a (BTree a)
140 insert : Ord a => a -> BTree a -> BTree a
141 insert x Leaf = Node Leaf x Leaf
142 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
143 else (Node l v (insert x r))
145 toList : BTree a -> List a
146 toList Leaf = []
147 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
149 toTree : Ord a => List a -> BTree a
150 toTree [] = Leaf
151 toTree (x :: xs) = insert x (toTree xs)
153In this case, any function with no access modifier will be exported as
154``abstract``, rather than left ``private``.
156Additionally, a module can re-export a module it has imported, by using
157the ``public`` modifier on an ``import``. For example:
159.. code-block:: idris
161 module A
163 import B
164 import public C
166 public a : AType a = ...
168The module ``A`` will export the name ``a``, as well as any public or
169abstract names in module ``C``, but will not re-export anything from
170module ``B``.
172Explicit Namespaces
173===================
175Defining a module also defines a namespace implicitly. However,
176namespaces can also be given *explicitly*. This is most useful if you
177wish to overload names within the same module:
179.. code-block:: idris
181 module Foo
183 namespace x
184 test : Int -> Int
185 test x = x * 2
187 namespace y
188 test : String -> String
189 test x = x ++ x
191This (admittedly contrived) module defines two functions with fully
192qualified names ``foo.x.test`` and ``foo.y.test``, which can be
193disambiguated by their types:
195::
197 *foo> test 3
198 6 : Int
199 *foo> test "foo"
200 "foofoo" : String
202Parameterised blocks
203====================
205Groups of functions can be parameterised over a number of arguments
206using a ``parameters`` declaration, for example:
208.. code-block:: idris
210 parameters (x : Nat, y : Nat)
211 addAll : Nat -> Nat
212 addAll z = x + y + z
214The effect of a ``parameters`` block is to add the declared parameters
215to every function, type and data constructor within the block. Outside
216the block, the parameters must be given explicitly:
218::
220 *params> :t addAll
221 addAll : Nat -> Nat -> Nat -> Nat
223Parameters blocks can be nested, and can also include data declarations,
224in which case the parameters are added explicitly to all type and data
225constructors. They may also be dependent types with implicit arguments:
227.. code-block:: idris
229 parameters (y : Nat, xs : Vect x a)
230 data Vects : Type -> Type where
231 MkVects : Vect y a -> Vects a
233 append : Vects a -> Vect (x + y) a
234 append (MkVects ys) = xs ++ ys
236To use ``Vects`` or ``append`` outside the block, we must also give the
237``xs`` and ``y`` arguments. Here, we can use placeholders for the values
238which can be inferred by the type checker:
240::
242 *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
243 "[1, 2, 3, 4, 5, 6]" : String