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
BTree.idr
):
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)
The modifiers export
and 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:
BTree.BTree
BTree.Leaf
BTree.Node
BTree.insert
BTree.toList
BTree.toTree
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.
The with
keyword in expressions comes in two variants:
with BTree.insert (insert x empty)
for one namewith [BTree.insert, BTree.empty] (insert x empty)
for multiple names
This is particularly useful with do
notation, where it can often improve
error messages: 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 Main.idr
.
Export Modifiers
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: private
, export
, or
public export
. Their general meaning is as follows:
private
meaning that it is not exported at all. This is the default.export
meaning that its top level type is exported.public export
meaning 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, public
export
definitions cannot use private
or export
names, and export
types cannot use private
names. This is to prevent private names leaking
into a module’s interface.
Meaning for Functions
export
the type is exportedpublic export
the 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 namepublic export
is intended to make you think twice about doing this.
Note
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
synonym for.
Since 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.
Note
For beginners:
If the function needs to be accessed only at runtime, use export
.
However, if it’s also meant to be used at compile time (e.g. to prove
a theorem), use public export
.
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 m
(and hence obtain thm : m = m
).
To achieve this, it will need access to the definition of plus
,
which includes the equation plus Z m = m
.
Therefore, in this case, plus
has to be marked as public export
.
Meaning for Data Types
For data types, the meanings are:
export
the type constructor is exportedpublic export
the type constructor and data constructors are exported
Meaning for Interfaces
For interfaces, the meanings are:
export
the interface name is exportedpublic export
the 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:
private
means the fixity declaration is only visible within the file.public export
andexport
are 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
the public
modifier on an import
. For example:
module A
import B
import public C
The module A
will export the name a
, as well as any public or
abstract names in module C
, but will not re-export anything from
module B
.
Renaming imports
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
This module A
has access to the exported names from module Data.List
,
but can also explicitly access them via the module name L
. import...as
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
interfaces of Books.Hardback
and Books.Comic
both under the namespace
Books
.
Explicit Namespaces
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
qualified names Foo.X.test
and 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 export
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. data
or record
),
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"
Parameterised blocks
Groups of functions can be parameterised over a number of arguments
using a 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
explicitly. The 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
To use Vects
or append
outside the block, we must also give the
xs
and 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]"