3.10. Namespaces

Each package has a namespace of the form author.package. Each module within a package is has namespace of the form author.package.module. Each type declared within a module has a namespace of the form author.package.module.Type.

3.10.1. Declaration of Names

All declarations within a module belong to the namespace of the module. If a function is strongly associated with a type, it can be declared within the namespace of the corresponding type. E.g.

class ℕ := zero; succ (ℕ)

ℕ.(+): ℕ → ℕ → ℕ := case
    λ n     zero        :=      n
    λ n     (succ m)    :=      succ (n + m)

Here the operation + is declared within the namespace ℕ which is also declared within some package namespace. Since the natural numbers are builtin, they live in the module prelude of the package alba.standard. I.e. the fully qualified name of addition of natural numbers is alba.standard.prelude.ℕ.(+).

There are some restrictions to putting a function name within a namespace of a type:

  • The type must appear in the signature of the function.

  • The type must belong to a module namespace within the same package.

Each declaration of an inductive type puts implicitly all constructors of the type into the namespace of the type. I.e. the fully qualified names of the constructors for natural numbers are alba.standard.prelude.ℕ.zero and alba.standard.prelude.ℕ.succ.

All declarations within a namespace must be unique.

3.10.2. Usage of Names

Names can be used in fully qualified form. But this is very tedious. The language is quite liberal in using unqualified names. The elaborator has in many cases sufficient type information to figure out the fully qualified name of a symbol.

In case where the type information is not sufficient to find out the fully qualified name, the source code can be enriched with some path information. It is not necessary to give the full path to disambiguate symbol. Only a substring of the path which makes the symbol unique is sufficient. Examples:

ℕ.(+) 1 2

ℕ.(3 + 5 * 9)

-- type annotation which achieves the same disambiguation
3 + 5 * 9: ℕ