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
21 | Node (BTree a) a (BTree a)
24 insert : Ord a => a -> BTree a -> BTree a
25 insert x Leaf = Node Leaf x Leaf
26 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
27 else (Node l v (insert x r))
30 toList : BTree a -> List a
32 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
35 toTree : Ord a => List a -> BTree a
37 toTree (x :: xs) = insert x (toTree xs)
39The modifiers ``export`` and ``public export`` say which names are visible
40from other modules. These are explained further below.
42Then, this gives a main program (in a file
43``bmain.idr``) which uses the ``Btree`` module to sort a list:
52 main = do let t = toTree [1,8,2,7,9,3]
53 print (Btree.toList t)
55The same names can be defined in multiple modules: names are *qualified* with
56the name of the module. The names defined in the ``Btree`` module are, in full:
65If names are otherwise unambiguous, there is no need to give the fully
66qualified name. Names can be disambiguated either by giving an explicit
67qualification, or according to their type.
69There is no formal link between the module name and its filename,
70although it is generally advisable to use the same name for each. An
71``import`` statement refers to a filename, using dots to separate
72directories. For example, ``import foo.bar`` would import the file
73``foo/bar.idr``, which would conventionally have the module declaration
74``module foo.bar``. The only requirement for module names is that the
75main module, with the ``main`` function, must be called
76``Main`` — although its filename need not be ``Main.idr``.
81Idris allows for fine-grained control over the visibility of a
82module's contents. By default, all names defined in a module are kept
83private. This aides in specification of a minimal interface and for
84internal details to be left hidden. Idris allows for functions,
85types, and interfaces to be marked as: ``private``, ``export``, or
86``public export``. Their general meaning is as follows:
88- ``private`` meaning that it's not exported at all. This is the default.
90- ``export`` meaning that its top level type is exported.
92- ``public export`` meaning that the entire definition is exported.
94A further restriction in modifying the visibility is that definitions
95must not refer to anything within a lower level of visibility. For
96example, ``public export`` definitions cannot use private names, and
97``export`` types cannot use private names. This is to prevent private
98names leaking into a module's interface.
103- ``export`` the type is exported
105- ``public export`` the type and definition are exported, and the
106 definition can be used after it is imported. In other words, the
107 definition itself is considered part of the module's interface. The
108 long name ``public export`` is intended to make you think twice
113 Type synonyms in Idris are created by writing a function. When
114 setting the visibility for a module, it might be a good idea to
115 ``public export`` all type synonyms if they are to be used outside
116 the module. Otherwise, Idris won't know what the synonym is a
119Since ``public export`` means that a function's definition is exported,
120this effectively makes the function definition part of the module's API.
121Therefore, it's generally a good idea to avoid using ``public export`` for
122functions unless you really mean to export the full definition.
124Meaning for Data Types
125----------------------
127For data types, the meanings are:
129- ``export`` the type constructor is exported
131- ``public export`` the type constructor and data constructors are exported
134Meaning for Interfaces
135----------------------
137For interfaces, the meanings are:
139- ``export`` the interface name is exported
141- ``public export`` the interface name, method names and default
142 definitions are exported
145----------------------
147The default export mode can be changed with the ``%access``
148directive, for example:
158 | Node (BTree a) a (BTree a)
160 insert : Ord a => a -> BTree a -> BTree a
161 insert x Leaf = Node Leaf x Leaf
162 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
163 else (Node l v (insert x r))
165 toList : BTree a -> List a
167 toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
169 toTree : Ord a => List a -> BTree a
171 toTree (x :: xs) = insert x (toTree xs)
173In this case, any function with no access modifier will be exported as
174``export``, rather than left ``private``.
176Propagating Inner Module API's
177-------------------------------
179Additionally, a module can re-export a module it has imported, by using
180the ``public`` modifier on an ``import``. For example:
189The module ``A`` will export the name ``a``, as well as any public or
190abstract names in module ``C``, but will not re-export anything from
196Defining a module also defines a namespace implicitly. However,
197namespaces can also be given *explicitly*. This is most useful if you
198wish to overload names within the same module:
209 test : String -> String
212This (admittedly contrived) module defines two functions with fully
213qualified names ``Foo.x.test`` and ``Foo.y.test``, which can be
214disambiguated by their types:
226Groups of functions can be parameterised over a number of arguments
227using a ``parameters`` declaration, for example:
231 parameters (x : Nat, y : Nat)
235The effect of a ``parameters`` block is to add the declared parameters
236to every function, type and data constructor within the
237block. Specifically, adding the parameters to the front of the
238argument list. Outside the block, the parameters must be given
239explicitly. The ``addAll`` function, when called from the REPL, will
240thus have the following type signature.
245 addAll : Nat -> Nat -> Nat -> Nat
247and the following definition.
251 addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
252 addAll x y z = x + y + z
254Parameters blocks can be nested, and can also include data declarations,
255in which case the parameters are added explicitly to all type and data
256constructors. They may also be dependent types with implicit arguments:
260 parameters (y : Nat, xs : Vect x a)
261 data Vects : Type -> Type where
262 MkVects : Vect y a -> Vects a
264 append : Vects a -> Vect (x + y) a
265 append (MkVects ys) = xs ++ ys
267To use ``Vects`` or ``append`` outside the block, we must also give the
268``xs`` and ``y`` arguments. Here, we can use placeholders for the values
269which can be inferred by the type checker:
273 *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
274 "[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