6. Compilation

6.3. Context

A compilation context consists of a set of packages and each package consists of a set of modules. A reference to a module has the form

author.package.name

where author.package uniquely identifies the package. The author has to be a valid github user and the package is the name of the repository.

Package dependencies and module dependencies have to be noncircular. The alba packages must not depend on any other packages. The package alba.core depends on no other package.

A compilation context consists of a set of used modules. Each module has an interface and an implementation. For the used modules only the interface part of the used modules are important.

Each module is a set of global declarations. Definitions can be given in the interface part or not depending on whether the definitions are exported.

6.4. Term Elaboration

The user term is given as an abstract syntax tree.

6.5. Elaboration Context

All terms are elaborated in an elaboration context. The elaboration context has information about the implicit and explicit arguments to which the term to be elaborated has to be applied and about the expected result. The expected result might be an object of a certain type (maybe given with metavariables) or just the information that a type is expected.

6.6. Sorts

The following are valid sorts and their corresponding types:

Level                       : Any omega
--                                  ^-- cannot appear in user code
Prop                        : Any 0
Any 10                      : Any 11
Any (u + 4)                 : Any (u + 5)
Any (max u (v + 3) z)       : Any (max u (v + 3) z + 1)

Any     -- treated as 'Any u' with the default universe 'u'.

For all global declarations the elaborator adds the default universe:

{u: Level}

All terms Any are elaborated in the default universe i.e. Any is elaborated as Any 0 and its type is Any 1. In case that the default universe u is not used, i.e. there is no Any in the gobal declaration without a universe specification, the default universe can be removed and the declaration is not universe polymorphic.

6.7. Types

All expressions to the right of a colon must be types. In the following A, B and R are types:

all (x: A) (y: B): R

f (x: A) (y: B): R := e

All sorts are types by construction. They can be elaborated as shown above. All other types must have the type Any u for some universe expression u. The elaborator introduces a metavariable:

?u: Level
-- u0 u1 ... are all universe variables in the context.

and tries to elaborate the type T with the expected type ?u.

6.8. Products

A product has the general form:

all (x: A) (y: B) ... : R

We treat A -> B -> ... as a shorthand for all (_: A) (_: B) ....

The type of a product is always a sort. I.e. a product can only be successfully elaborated where a type is required. A product cannot be applied to arguments.

First the argument types have to be elaborated as types and the result type has to be elaborated as type (see above).

After successful elaboration of each type a local variable with the elaborated type and the corresponding name is shifted into the context. The following type might depend on the variable.

After the successful elaboration of the types it has to be checked, which variables are optionally (they occur in one of the following types) and mandatory implicit (they occur in one of the following types and are kinds occur in propositions). The user declaration has to respect the mandatory implicitness and the mandatory explicitness.

6.9. Identifier / Operator

If the identifier is a local name, then the identifier has to be elaborated as the local variable (local variables are shadowing all other names).

If the identifier is a global name, then it can be ambiguous. There are the following possibilities to disambiguate the name:

Namespace specification
Argument types and/or result type

In order to disambiguate through types each type of a global gets a signature where we distinguish between unknowns U, implicits I, sorts S and global names. Some examples:

-- type                                     signature

Any -> Any                                  [S, S]

all {A: Any}: List A -> Natural             [I, List, Natural]

Int -> Int -> Int                           [Int, Int, Int]

all {A: Any}: A                             [I, U]

all {A: Any}: A -> A                        [I, U, U]

all {A: Any} {B: A->Any} (a: A) -> (all x: B x) -> B a
                                            [I, I, U, [U,U], U]

Having the signature we can check, if the global can accept sufficient arguments. If yes, we can strip off the given arguments and get a signature for the result type and can compare it with the signature of the expected result type.

If there remain ambiguities we have to elaborate the arguments which can distinguish the possibilities.

If we cannot resolve the ambituities neither by names space specifications nor by the result type nor by argument types then the elaboration fails. The only possibility to recover from this failure is when the result type could distinguish the ambiguity but is not yet known (it is still described by a metavariable). In the latter case we could resume the elaboration when the result type is known exactly.

6.10. Function Application

Syntax:

f a b ...

Every term is a function application even if there are no explicit arguments. There can be implicit arguments.

First we elaborate f.

Then forall given arguments (implicit or explicit) we introduce metavariables for all not given implicit arguments and elaborate the argument with an expected result type.

Finally we unify the actual result type with the expected result type.