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, 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)
35Then, this gives a main program (in a file
36``bmain.idr``) which uses the ``bst`` module to sort a list::
45 main = do let t = toTree [1,8,2,7,9,3]
46 print (btree.toList t)
48The same names can be defined in multiple modules. This is possible
49because in practice names are *qualified* with the name of the module.
50The names defined in the ``btree`` module are, in full:
59If names are otherwise unambiguous, there is no need to give the fully
60qualified name. Names can be disambiguated either by giving an explicit
61qualification, or according to their type.
63There is no formal link between the module name and its filename,
64although it is generally advisable to use the same name for each. An
65``import`` statement refers to a filename, using dots to separate
66directories. For example, ``import foo.bar`` would import the file
67``foo/bar.idr``, which would conventionally have the module declaration
68``module foo.bar``. The only requirement for module names is that the
69main module, with the ``main`` function, must be called
70``Main``—although its filename need not be ``Main.idr``.
75By default, all names defined in a module are exported for use by other
76modules. However, it is good practice only to export a minimal interface
77and keep internal details abstract. Idris allows functions, types,
78and classes to be marked as: ``public``, ``abstract`` or ``private``:
80- ``public`` means that both the name and definition are exported. For
81 functions, this means that the implementation is exported (which
82 means, for example, it can be used in a dependent type). For data
83 types, this means that the type name and the constructors are
84 exported. For classes, this means that the class name and method
87- ``abstract`` means that only the name is exported. For functions,
88 this means that the implementation is not exported. For data types,
89 this means that the type name is exported but not the constructors.
90 For classes, this means that the class name is exported but not the
93- ``private`` means that neither the name nor the definition is
97 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
99For our ``btree`` module, it makes sense for the tree data type and the
100functions to be exported as ``abstract``, as we see below:
106 abstract data BTree a = Leaf
107 | Node (BTree a) a (BTree a)
110 insert : Ord a => a -> BTree a -> BTree a
111 insert x Leaf = Node Leaf x Leaf
112 insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
113 else (Node l v (insert x r))
116 toList : BTree a -> List a
118 toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
121 toTree : Ord a => List a -> BTree a
123 toTree (x :: xs) = insert x (toTree xs)
125Finally, the default export mode can be changed with the ``%access``
126directive, for example:
128In this case, any function with no access modifier will be exported as
129``abstract``, rather than left ``private``.
131Additionally, a module can re-export a module it has imported, by using
132the ``public`` modifier on an ``import``. For example:
138 import B import public C
140 public a : AType a = ...
142The module ``A`` will export the name ``a``, as well as any public or
143abstract names in module ``C``, but will not re-export anything from
149Defining a module also defines a namespace implicitly. However,
150namespaces can also be given *explicitly*. This is most useful if you
151wish to overload names within the same module:
162 test : String -> String
165This (admittedly contrived) module defines two functions with fully
166qualified names ``foo.x.test`` and ``foo.y.test``, which can be
167disambiguated by their types:
179Groups of functions can be parameterised over a number of arguments
180using a ``parameters`` declaration, for example:
184 parameters (x : Nat, y : Nat)
188The effect of a ``parameters`` block is to add the declared parameters
189to every function, type and data constructor within the block. Outside
190the block, the parameters must be given explicitly:
195 addAll : Nat -> Nat -> Nat -> Nat
197Parameters blocks can be nested, and can also include data declarations,
198in which case the parameters are added explicitly to all type and data
199constructors. They may also be dependent types with implicit arguments:
203 parameters (y : Nat, xs : Vect x a)
204 data Vects : Type -> Type where
205 MkVects : Vect y a -> Vects a
207 append : Vects a -> Vect (x + y) a
208 append (MkVects ys) = xs ++ ys
210To use ``Vects`` or ``append`` outside the block, we must also give the
211``xs`` and ``y`` arguments. Here, we can use placeholders for the values
212which can be inferred by the type checker:
216 *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
217 "[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