@@ -75,56 +75,101 @@ main module, with the ``main`` function, must be called
75Export Modifiers
75Export Modifiers
76================
76================
78+Idris allows for fine-grained control over the visibility of a
78−By default, all names defined in a module are exported for use by other
79+module's contents. By default, all names defined in a module are kept
79−modules. However, it is good practice only to export a minimal interface
80+private. This aides in specification of a minimal interface and for
80−and keep internal details abstract. Idris allows functions, types,
81+internal details to be left hidden. Idris allows for functions,
81−and interfaces to be marked as: ``public``, ``abstract`` or ``private``:
82+types, and interfaces to be marked as: ``private``, ``export``, or
82−
83+``public export``. Their general meaning is as follows:
83−- ``public`` means that both the name and definition are exported. For
84+
84− functions, this means that the implementation is exported (which
85+- ``private`` meaning that it's not exported at all. This is the
85− means, for example, it can be used in a dependent type). For data
86+ default.
86− types, this means that the type name and the constructors are
87+
87− exported. For interfaces, this means that the interface name and method
88+- ``export`` meaning that its top level type is exported.
88− names are exported.
89+
89−
90+- ``public export`` meaning that the entire definition is exported.
90−- ``abstract`` means that only the name is exported. For functions,
91+
91− this means that the implementation is not exported. For data types,
92+
92− this means that the type name is exported but not the constructors.
93+A further restriction in modifying the visibility is that definitions
93− For interfaces, this means that the interface name is exported but not the
94+must not refer to anything within a lower level of visibility. For
94− method names.
95+example, ``public export`` definitions cannot use private names, and
95−
96+``export`` types cannot use private names. This is to prevent private
96−- ``private`` means that neither the name nor the definition is
97+names leaking into a module's interface.
100+---------------------
102+- ``export`` the type is exported
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
100− If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
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
119+Meaning for Data Types
120+----------------------
122+For data types, the meanings are:
124+- ``export`` the type constructor is exported
126+- ``public export`` the type constructor and data constructors are
130+Meaning for Interfaces
131+----------------------
133+For interfaces, the meanings are:
135+- ``export`` the interface name is exported
136+- ``public export`` the interface name, method names and default
137+ definitions are exported
102−For our ``Btree`` module, it makes sense for the tree data type and the
144+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:
145+functions to be exported as ``export``, as we see below:
105.. code-block:: idris
147.. code-block:: idris
107− module Btree
149+ module BTree
109− abstract data BTree a = Leaf
151+ export data BTree a = Leaf
110− | Node (BTree a) a (BTree a)
152+ | Node (BTree a) a (BTree a)
113 insert : Ord a => a -> BTree a -> BTree a
155 insert : Ord a => a -> BTree a -> BTree a
114 insert x Leaf = Node Leaf x Leaf
156 insert x Leaf = Node Leaf x Leaf
115 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
157 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
116 else (Node l v (insert x r))
158 else (Node l v (insert x r))
119 toList : BTree a -> List a
161 toList : BTree a -> List a
120 toList Leaf = []
162 toList Leaf = []
121 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
163 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
124 toTree : Ord a => List a -> BTree a
166 toTree : Ord a => List a -> BTree a
125 toTree [] = Leaf
167 toTree [] = Leaf
126 toTree (x :: xs) = insert x (toTree xs)
168 toTree (x :: xs) = insert x (toTree xs)
170+``%access`` Directive
171+----------------------
128Finally, the default export mode can be changed with the ``%access``
173Finally, the default export mode can be changed with the ``%access``
129directive, for example:
174directive, for example:
@@ -132,7 +177,7 @@ directive, for example:
133 module Btree
178 module Btree
135− %access abstract
180+ %access export
137 data BTree a = Leaf
182 data BTree a = Leaf
138 | Node (BTree a) a (BTree a)
183 | Node (BTree a) a (BTree a)
@@ -151,7 +196,10 @@ directive, for example:
151 toTree (x :: xs) = insert x (toTree xs)
196 toTree (x :: xs) = insert x (toTree xs)
153In this case, any function with no access modifier will be exported as
198In this case, any function with no access modifier will be exported as
154−``abstract``, rather than left ``private``.
199+``export``, rather than left ``private``.
201+Propagating Inner Module API's
202+-------------------------------
156Additionally, a module can re-export a module it has imported, by using
204Additionally, a module can re-export a module it has imported, by using
157the ``public`` modifier on an ``import``. For example:
205the ``public`` modifier on an ``import``. For example: