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, interfaces and functions. For example, the listing below gives a
12module which defines a binary tree type ``BTree`` (in a file
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
29 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
31 toTree : Ord a => List a -> BTree a
33 toTree (x :: xs) = insert x (toTree xs)
36Then, this gives a main program (in a file
37``bmain.idr``) which uses the ``Btree`` module to sort a list:
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:
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``.
78Idris allows for fine-grained control over the visibility of a
79module's contents. By default, all names defined in a module are kept
80private. This aides in specification of a minimal interface and for
81internal details to be left hidden. Idris allows for functions,
82types, and interfaces to be marked as: ``private``, ``export``, or
83``public export``. Their general meaning is as follows:
85- ``private`` meaning that it's not exported at all. This is the
88- ``export`` meaning that its top level type is exported.
90- ``public export`` meaning that the entire definition is exported.
93A further restriction in modifying the visibility is that definitions
94must not refer to anything within a lower level of visibility. For
95example, ``public export`` definitions cannot use private names, and
96``export`` types cannot use private names. This is to prevent private
97names leaking into a module's interface.
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
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
119Meaning for Data Types
120----------------------
122For data types, the meanings are:
124- ``export`` the type constructor is exported
126- ``public export`` the type constructor and data constructors are
130Meaning for Interfaces
131----------------------
133For 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
144For our ``BTree`` module, it makes sense for the tree data type and the
145functions to be exported as ``export``, as we see below:
151 export data BTree a = Leaf
152 | Node (BTree a) a (BTree a)
155 insert : Ord a => a -> BTree a -> BTree a
156 insert x Leaf = Node Leaf x Leaf
157 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
158 else (Node l v (insert x r))
161 toList : BTree a -> List a
163 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
166 toTree : Ord a => List a -> BTree a
168 toTree (x :: xs) = insert x (toTree xs)
171----------------------
173Finally, the default export mode can be changed with the ``%access``
174directive, for example:
183 | Node (BTree a) a (BTree a)
185 insert : Ord a => a -> BTree a -> BTree a
186 insert x Leaf = Node Leaf x Leaf
187 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
188 else (Node l v (insert x r))
190 toList : BTree a -> List a
192 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
194 toTree : Ord a => List a -> BTree a
196 toTree (x :: xs) = insert x (toTree xs)
198In this case, any function with no access modifier will be exported as
199``export``, rather than left ``private``.
201Propagating Inner Module API's
202-------------------------------
204Additionally, a module can re-export a module it has imported, by using
205the ``public`` modifier on an ``import``. For example:
214 public a : AType a = ...
216The module ``A`` will export the name ``a``, as well as any public or
217abstract names in module ``C``, but will not re-export anything from
223Defining a module also defines a namespace implicitly. However,
224namespaces can also be given *explicitly*. This is most useful if you
225wish to overload names within the same module:
236 test : String -> String
239This (admittedly contrived) module defines two functions with fully
240qualified names ``foo.x.test`` and ``foo.y.test``, which can be
241disambiguated by their types:
253Groups of functions can be parameterised over a number of arguments
254using a ``parameters`` declaration, for example:
258 parameters (x : Nat, y : Nat)
262The effect of a ``parameters`` block is to add the declared parameters
263to every function, type and data constructor within the
264block. Specifically, adding the parameters to the front of the
265argument list. Outside the block, the parameters must be given
266explicitly. The ``addAll`` function, when called from the REPL, will
267thus have the following type signature.
272 addAll : Nat -> Nat -> Nat -> Nat
274and the following definition.
278 addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
279 addAll x y z = x + y + z
281Parameters blocks can be nested, and can also include data declarations,
282in which case the parameters are added explicitly to all type and data
283constructors. They may also be dependent types with implicit arguments:
287 parameters (y : Nat, xs : Vect x a)
288 data Vects : Type -> Type where
289 MkVects : Vect y a -> Vects a
291 append : Vects a -> Vect (x + y) a
292 append (MkVects ys) = xs ++ ys
294To use ``Vects`` or ``append`` outside the block, we must also give the
295``xs`` and ``y`` arguments. Here, we can use placeholders for the values
296which can be inferred by the type checker:
300 *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
301 "[1, 2, 3, 4, 5, 6]" : String
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list