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, classes and functions. For example, Listing :ref:`bstmod` gives a
12module which defines a binary tree type ``BTree`` (in a file
13``btree.idr``) and Listing :ref:`bstmain` gives a main program (in a file
14``bmain.idr`` which uses the ``bst`` module to sort a list.
18 :caption: Binary Tree Module
23 | Node (BTree a) a (BTree a)
25 insert : Ord a => a -> BTree a -> BTree a
26 insert x Leaf = Node Leaf x Leaf
27 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
28 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)
34 toTree : Ord a => List a -> BTree a
36 toTree (x :: xs) = insert x (toTree xs)
40 :caption: Binary Tree Main Program
47 main = do let t = toTree [1,8,2,7,9,3]
48 print (btree.toList t)
50The same names can be defined in multiple modules. This is possible
51because in practice names are *qualified* with the name of the module.
52The names defined in the ``btree`` module are, in full:
61If names are otherwise unambiguous, there is no need to give the fully
62qualified name. Names can be disambiguated either by giving an explicit
63qualification, or according to their type.
65There is no formal link between the module name and its filename,
66although it is generally advisable to use the same name for each. An
67``import`` statement refers to a filename, using dots to separate
68directories. For example, ``import foo.bar`` would import the file
69``foo/bar.idr``, which would conventionally have the module declaration
70``module foo.bar``. The only requirement for module names is that the
71main module, with the ``main`` function, must be called
72``Main``—although its filename need not be ``Main.idr``.
77By default, all names defined in a module are exported for use by other
78modules. However, it is good practice only to export a minimal interface
79and keep internal details abstract. ``Idris`` allows functions, types,
80and classes to be marked as: ``public``, ``abstract`` or ``private``:
82- ``public`` means that both the name and definition are exported. For
83 functions, this means that the implementation is exported (which
84 means, for example, it can be used in a dependent type). For data
85 types, this means that the type name and the constructors are
86 exported. For classes, this means that the class name and method
89- ``abstract`` means that only the name is exported. For functions,
90 this means that the implementation is not exported. For data types,
91 this means that the type name is exported but not the constructors.
92 For classes, this means that the class name is exported but not the
95- ``private`` means that neither the name nor the definition is
99 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
101For our ``btree`` module, it makes sense for the tree data type and the
102functions to be exported as ``abstract``, as we see in
103Listing :ref:`bstmodp`.
107 :caption: Binary Tree Module, with export modifiers
111 abstract data BTree a = Leaf
112 | Node (BTree a) a (BTree a)
115 insert : Ord a => a -> BTree a -> BTree a
116 insert x Leaf = Node Leaf x Leaf
117 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
118 else (Node l v (insert x r))
121 toList : BTree a -> List a
123 toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
126 toTree : Ord a => List a -> BTree a
128 toTree (x :: xs) = insert x (toTree xs)
130Finally, the default export mode can be changed with the ``%access``
131directive, for example:
133In this case, any function with no access modifier will be exported as
134``abstract``, rather than left ``private``.
136Additionally, a module can re-export a module it has imported, by using
137the ``public`` modifier on an ``import``. For example:
143 import B import public C
145 public a : AType a = ...
147The module ``A`` will export the name ``a``, as well as any public or
148abstract names in module ``C``, but will not re-export anything from
154Defining a module also defines a namespace implicitly. However,
155namespaces can also be given *explicitly*. This is most useful if you
156wish to overload names within the same module:
167 test : String -> String
170This (admittedly contrived) module defines two functions with fully
171qualified names ``foo.x.test`` and ``foo.y.test``, which can be
172disambiguated by their types:
184Groups of functions can be parameterised over a number of arguments
185using a ``parameters`` declaration, for example:
189 parameters (x : Nat, y : Nat)
193The effect of a ``parameters`` block is to add the declared parameters
194to every function, type and data constructor within the block. Outside
195the block, the parameters must be given explicitly:
200 addAll : Nat -> Nat -> Nat -> Nat
202Parameters blocks can be nested, and can also include data declarations,
203in which case the parameters are added explicitly to all type and data
204constructors. They may also be dependent types with implicit arguments:
208 parameters (y : Nat, xs : Vect x a)
209 data Vects : Type -> Type where
210 MkVects : Vect y a -> Vects a
212 append : Vects a -> Vect (x + y) a
213 append (MkVects ys) = xs ++ ys
215To use ``Vects`` or ``append`` outside the block, we must also give the
216``xs`` and ``y`` arguments. Here, we can use placeholders for the values
217which can be inferred by the type checker:
221 *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
222 "[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