@@ -75,56 +75,101 @@ 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``:
82−
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.
89−
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.
95−
96−- ``private`` means that neither the name nor the definition is
97− exported.
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:
84+
85+- ``private`` meaning that it's not exported at all. This is the
86+ default.
87+
88+- ``export`` meaning that its top level type is exported.
89+
90+- ``public export`` meaning that the entire definition is exported.
91+
92+
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.
98109
99110.. note::
100− If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
101111
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:
112+ Type synonyms in Idris are created by writing a function. When
113+ setting the visibility for a module, it might be a good idea to
114+ ``public export`` all type synonyms if they are to be used outside
115+ the module. Otherwise, Idris won't know what the synonym is a
116+ synonym for.
117+
118+
119+Meaning for Data Types
120+----------------------
121+
122+For data types, the meanings are:
123+
124+- ``export`` the type constructor is exported
125+
126+- ``public export`` the type constructor and data constructors are
127+ exported
128+
129+
130+Meaning for Interfaces
131+----------------------
132+
133+For interfaces, the meanings are:
134+
135+- ``export`` the interface name is exported
136+- ``public export`` the interface name, method names and default
137+ definitions are exported
138+
139+
140+
141+``BTree`` Revisited
142++++++++++++++++++++
143+
144+For our ``BTree`` module, it makes sense for the tree data type and the
145+functions to be exported as ``export``, as we see below:
104146
105147.. code-block:: idris
106148
107− module Btree
149+ module BTree
108150
109− abstract data BTree a = Leaf
110− | Node (BTree a) a (BTree a)
151+ export data BTree a = Leaf
152+ | Node (BTree a) a (BTree a)
111153
112− abstract
154+ export
113155 insert : Ord a => a -> BTree a -> BTree a
114156 insert x Leaf = Node Leaf x Leaf
115157 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
116158 else (Node l v (insert x r))
117159
118− abstract
160+ export
119161 toList : BTree a -> List a
120162 toList Leaf = []
121163 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
122164
123− abstract
165+ export
124166 toTree : Ord a => List a -> BTree a
125167 toTree [] = Leaf
126168 toTree (x :: xs) = insert x (toTree xs)
127169
170+``%access`` Directive
171+----------------------
172+
128173Finally, the default export mode can be changed with the ``%access``
129174directive, for example:
130175
@@ -132,7 +177,7 @@ directive, for example:
132177
133178 module Btree
134179
135− %access abstract
180+ %access export
136181
137182 data BTree a = Leaf
138183 | Node (BTree a) a (BTree a)
@@ -151,7 +196,10 @@ directive, for example:
151196 toTree (x :: xs) = insert x (toTree xs)
152197
153198In this case, any function with no access modifier will be exported as
154−``abstract``, rather than left ``private``.
199+``export``, rather than left ``private``.
200+
201+Propagating Inner Module API's
202+-------------------------------
155203
156204Additionally, a module can re-export a module it has imported, by using
157205the ``public`` modifier on an ``import``. For example: