Modules and Namespaces
An Idris program consists of a collection of modules. Each module
includes an optional
module declaration giving the name of the
module, a list of
import statements giving the other modules which
are to be imported, and a collection of declarations and definitions of
types, interfaces and functions. For example, the listing below gives a
module which defines a binary tree type
BTree (in a file
module BTree public export data BTree a = Leaf | Node (BTree a) a (BTree a) export insert : Ord a => a -> BTree a -> BTree a insert x Leaf = Node Leaf x Leaf insert x (Node l v r) = if (x < v) then (Node (insert x l) v r) else (Node l v (insert x r)) export toList : BTree a -> List a toList Leaf =  toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r) export toTree : Ord a => List a -> BTree a toTree  = Leaf toTree (x :: xs) = insert x (toTree xs)
public export say which names are visible
from other namespaces. These are explained further below.
Then, this gives a main program (in a file
bmain.idr) which uses the
BTree module to sort a list:
module Main import BTree main : IO () main = do let t = toTree [1,8,2,7,9,3] print (BTree.toList t)
The same names can be defined in multiple modules: names are qualified with
the name of the module. The names defined in the
BTree module are, in full:
If names are otherwise unambiguous, there is no need to give the fully
qualified name. Names can be disambiguated either by giving an explicit
qualification, using the
with keyword, or according to their type.
with keyword in expressions comes in two variants:
with BTree.insert (insert x empty)for one name
with [BTree.insert, BTree.empty] (insert x empty)for multiple names
This is particularly useful with
do notation, where it can often improve
with MyModule.(>>=) do ...
There is no formal link between the module name and its filename,
although it is generally advisable to use the same name for each. An
import statement refers to a filename, using dots to separate
directories. For example,
import foo.bar would import the file
foo/bar.idr, which would conventionally have the module declaration
module foo.bar. The only requirement for module names is that the
main module, with the
main function, must be called
Main — although its filename need not be
Idris allows for fine-grained control over the visibility of a
namespace’s contents. By default, all names defined in a namespace are kept
private. This aids in specification of a minimal interface and for
internal details to be left hidden. Idris allows for functions,
types, and interfaces to be marked as:
public export. Their general meaning is as follows:
privatemeaning that it is not exported at all. This is the default.
exportmeaning that its top level type is exported.
public exportmeaning that the entire definition is exported.
A further restriction in modifying the visibility is that definitions must not
refer to anything within a lower level of visibility. For example,
export definitions cannot use
export names, and
types cannot use
private names. This is to prevent private names leaking
into a module’s interface.
Meaning for Functions
exportthe type is exported
public exportthe type and definition are exported, and the definition can be used after it is imported. In other words, the definition itself is considered part of the module’s interface. The long name
public exportis intended to make you think twice about doing this.
Type synonyms in Idris are created by writing a function. When
setting the visibility for a module, it is usually a good idea to
public export all type synonyms if they are to be used outside
the module. Otherwise, Idris won’t know what the synonym is a
public export means that a function’s definition is exported,
this effectively makes the function definition part of the module’s API.
Therefore, it’s generally a good idea to avoid using
public export for
functions unless you really mean to export the full definition.
If the function needs to be accessed only at runtime, use
However, if it’s also meant to be used at compile time (e.g. to prove
a theorem), use
For example, consider the function
plus : Nat -> Nat -> Nat discussed
previously, and the following theorem:
thm : plus Z m = m.
In order to prove it, the type checker needs to reduce
plus Z m to
(and hence obtain
thm : m = m).
To achieve this, it will need access to the definition of
which includes the equation
plus Z m = m.
Therefore, in this case,
plus has to be marked as
Meaning for Data Types
For data types, the meanings are:
exportthe type constructor is exported
public exportthe type constructor and data constructors are exported
Meaning for Interfaces
For interfaces, the meanings are:
exportthe interface name is exported
public exportthe interface name, method names and default definitions are exported
Meaning for fixity declarations
The modifiers differ slightly when applied to fixities. Un-labelled fixities are exported rather than be private. There is no difference between public export and export. In summary:
privatemeans the fixity declaration is only visible within the file.
exportare the same and the fixity is exported. The access modifier could also be eluded for the same effect.
Propagating Inner Module API’s
Additionally, a module can re-export a module it has imported, by using
public modifier on an
import. For example:
module A import B import public C
A will export the name
a, as well as any public or
abstract names in module
C, but will not re-export anything from
Sometimes it is convenient to be able to access the names in another module via a different namespace (typically, a shorter one). For this, you can use import…as. For example:
module A import Data.List as L
A has access to the exported names from module
but can also explicitly access them via the module name
can also be combined with
import public to create a module which exports
a larger API from other sub-modules:
module Books import public Books.Hardback as Books import public Books.Comic as Books
Here, any module which imports
Books will have access to the exported
Books.Comic both under the namespace
Defining a module also defines a namespace implicitly. However, namespaces can also be given explicitly. This is most useful if you wish to overload names within the same module:
module Foo namespace X export test : Int -> Int test x = x * 2 namespace Y export test : String -> String test x = x ++ x
This (admittedly contrived) module defines two functions with fully
Foo.Y.test, which can be
disambiguated by their types:
*Foo> test 3 6 : Int *Foo> test "foo" "foofoo" : String
The export rules,
public export and
export, are per namespace,
not per file, so the two
test definitions above need the
flag to be visible outside their own namespaces.
Explicit namespaces inside functions
Explicit namespaces can be defined inside
where-blocks of functions.
Unlike other definitions (e.g.
such namespace definitions are understood as belonging to the scope of the
function definition itself.
For example, the following code should typecheck.
withNSInside : Nat withNSInside = g where namespace X export g : Nat g = 5 useNSFromOutside : Nat useNSFromOutside = X.g
Notice that if a function that contains namespace definition has parameters, then definitions inside this namespace will have these parameters too. This is done because such definitions have access to values of the parameters.
These parameters must be passed explicitly when accessing namespaced definitions from outside the function where they are declared, and must not be passed when accessed from the inside. This behaviour is similar to parameterised blocks described below. Look at the following example.
withNSInside' : String -> Nat withNSInside' str = String.length g where namespace Y export g : String g = str ++ "a" useNSFromOutside' : String useNSFromOutside' = Y.g "x" -- value is "xa"
Groups of functions can be parameterised over a number of arguments
parameters declaration, for example:
parameters (x : Nat, y : Nat) addAll : Nat -> Nat addAll z = x + y + z
The effect of a
parameters block is to add the declared parameters
to every function, type and data constructor within the
block. Specifically, adding the parameters to the front of the
argument list. Outside the block, the parameters must be given
addAll function, when called from the REPL, will
thus have the following type signature.
*params> :t addAll addAll : Nat -> Nat -> Nat -> Nat
and the following definition.
addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat addAll x y z = x + y + z
Parameters blocks can be nested, and can also include data declarations, in which case the parameters are added explicitly to all type and data constructors. They may also be dependent types with implicit arguments:
parameters (y : Nat, xs : Vect x a) data Vects : Type -> Type where MkVects : Vect y a -> Vects a append : Vects a -> Vect (x + y) a append (MkVects ys) = xs ++ ys
append outside the block, we must also give the
y arguments. Here, we can use placeholders for the values
which can be inferred by the type checker:
Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6])) "[1, 2, 3, 4, 5, 6]"