@@ -75,56 +75,91 @@ main module, with the ``main`` function, must be called
7575Export Modifiers
7676================
7777
78−By default, all names defined in a module are exported for use by other
79−modules. However, it is good practice only to export a minimal interface
80−and keep internal details abstract. Idris allows functions, types,
81−and interfaces to be marked as: ``public``, ``abstract`` or ``private``:
78+Idris allows for fine-grained control over the visibility of a
79+module's contents. By default, all names defined in a module are kept
80+private. This aides in specification of a minimal interface and for
81+internal details to be left hidden. Idris allows for functions,
82+types, and interfaces to be marked as: ``private``, ``export``, or
83+``public export``. Their general meaning is as follows:
8284
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 interfaces, this means that the interface name and method
88− names are exported.
85+- ``private`` meaning that it's not exported at all. This is the
86+ default.
8987
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 interfaces, this means that the interface name is exported but not the
94− method names.
88+- ``export`` meaning that its top level type is exported.
9589
96−- ``private`` means that neither the name nor the definition is
97− exported.
90+- ``public export`` meaning that the entire definition is exported.
9891
99−.. note::
100− If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
10192
102−For our ``Btree`` module, it makes sense for the tree data type and the
103−functions to be exported as ``abstract``, as we see below:
93+A further restriction in modifying the visibility is that definitions
94+must not refer to anything within a lower level of visibility. For
95+example, ``public export`` definitions cannot use private names, and
96+``export`` types cannot use private names. This is to prevent private
97+names leaking into a module's interface.
98+
99+Meaning for Functions
100+---------------------
101+
102+- ``export`` the type is exported
103+
104+- ``public export`` the type and definition are exported, and the
105+ definition can be used after it is imported. In other words, the
106+ definition itself is considered part of the module's interface. The
107+ long name ``public export`` is intended to make you think twice
108+ about doing this...
109+
110+Meaning for Data Types
111+----------------------
112+
113+For data types, the meanings are:
114+
115+- ``export`` the type constructor is exported
116+
117+- ``public export`` the type constructor and data constructors are
118+ exported
119+
120+
121+Meaning for Interfaces
122+----------------------
123+
124+For interfaces, the meanings are:
125+
126+- ``export`` the interface name is exported
127+- ``public export`` the interface name, method names and default
128+ definitions are exported
129+
130+
131+``BTree`` Revisited
132++++++++++++++++++++
133+
134+For our ``BTree`` module, it makes sense for the tree data type and the
135+functions to be exported as ``export``, as we see below:
104136
105137.. code-block:: idris
106138
107− module Btree
139+ module BTree
108140
109− abstract data BTree a = Leaf
110− | Node (BTree a) a (BTree a)
141+ export data BTree a = Leaf
142+ | Node (BTree a) a (BTree a)
111143
112− abstract
144+ export
113145 insert : Ord a => a -> BTree a -> BTree a
114146 insert x Leaf = Node Leaf x Leaf
115147 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
116148 else (Node l v (insert x r))
117149
118− abstract
150+ export
119151 toList : BTree a -> List a
120152 toList Leaf = []
121153 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
122154
123− abstract
155+ export
124156 toTree : Ord a => List a -> BTree a
125157 toTree [] = Leaf
126158 toTree (x :: xs) = insert x (toTree xs)
127159
160+``%access`` Directive
161+----------------------
162+
128163Finally, the default export mode can be changed with the ``%access``
129164directive, for example:
130165
@@ -132,7 +167,7 @@ directive, for example:
132167
133168 module Btree
134169
135− %access abstract
170+ %access export
136171
137172 data BTree a = Leaf
138173 | Node (BTree a) a (BTree a)
@@ -151,7 +186,10 @@ directive, for example:
151186 toTree (x :: xs) = insert x (toTree xs)
152187
153188In this case, any function with no access modifier will be exported as
154−``abstract``, rather than left ``private``.
189+``export``, rather than left ``private``.
190+
191+Propagating Inner Module API's
192+-------------------------------
155193
156194Additionally, a module can re-export a module it has imported, by using
157195the ``public`` modifier on an ``import``. For example: