.. _sect-namespaces: **********************Modules and Namespaces********************** An Idris program consists of a collection of modules. Each moduleincludes an optional ``module`` declaration giving the name of themodule, a list of ``import`` statements giving the other modules whichare to be imported, and a collection of declarations and definitions oftypes, interfaces and functions. For example, the listing below gives amodule which defines a binary tree type ``BTree`` (in a file``BTree.idr``): .. code-block:: idris     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 visiblefrom 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: .. code-block:: idris     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* withthe 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 fullyqualified name. Names can be disambiguated either by giving an explicitqualification, or according to their type. 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 separatedirectories. 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 themain 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 anamespace's contents. By default, all names defined in a namespace are keptprivate.  This aids in specification of a minimal interface and forinternal 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 notrefer to anything within a lower level of visibility. For example, ``publicexport`` definitions cannot use ``private`` or ``export`` names, and ``export``types cannot use ``private`` names. This is to prevent private names leakinginto a module's interface. Meaning for Functions--------------------- - ``export`` the type is exported - ``public 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 name ``public 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`` forfunctions unless you really mean to export the full definition. Meaning for Data Types---------------------- For data types, the meanings are: - ``export`` the type constructor is exported - ``public export`` the type constructor and data constructors are exported  Meaning for Interfaces---------------------- For interfaces, the meanings are: - ``export`` the interface name is exported - ``public export`` the interface name, method names and default  definitions are exported Propagating Inner Module API's------------------------------- Additionally, a module can re-export a module it has imported, by usingthe ``public`` modifier on an ``import``. For example: .. code-block:: idris   :force:     module A     import B    import public C The module ``A`` will export the name ``a``, as well as any public orabstract names in module ``C``, but will not re-export anything frommodule ``B``. Explicit Namespaces=================== Defining a module also defines a namespace implicitly. However,namespaces can also be given *explicitly*. This is most useful if youwish to overload names within the same module: .. code-block:: idris     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 fullyqualified names ``Foo.X.test`` and ``Foo.Y.test``, which can bedisambiguated 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. Parameterised blocks==================== Groups of functions can be parameterised over a number of argumentsusing a ``parameters`` declaration, for example: .. code-block:: idris     parameters (x : Nat, y : Nat)      addAll : Nat -> Nat      addAll z = x + y + z The effect of a ``parameters`` block is to add the declared parametersto every function, type and data constructor within theblock. Specifically, adding the parameters to the front of theargument list. Outside the block, the parameters must be givenexplicitly. The ``addAll`` function, when called from the REPL, willthus have the following type signature. ::     *params> :t addAll    addAll : Nat -> Nat -> Nat -> Nat and the following definition. .. code-block:: idris     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 dataconstructors. They may also be dependent types with implicit arguments: .. code-block:: idris     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 valueswhich can be inferred by the type checker: ::     Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))    "[1, 2, 3, 4, 5, 6]"