Chapter 7 Signatures and modules
7.1 Signatures
Need to allow qualified names on lhs of type reveal.
7.2 Specifications
7.2.1 Module specifications
7.2.2 Type specifications
7.2.3 Class specifications
7.2.4 Constant specifications
7.2.5 Value specifications
7.3 Modules
7.3.1 A module's implicit signature
Each module definition defines an implicit signature, which governs
how the outside world sees the contents of the module.
The implicit signature of a module can be determined by a simple
syntactic transformation of its declarations into specicifations.
If the resulting signature is not well formed, then the module
is not well formed.
The translation of a declaration to zero or more specifications
is as follows:
-
If the declaration is annotated with local then there is no
corresponding specification.
- If the declaration has the form ...
- If the declaration is a type declaration, then the specification is
identical.
- If the declaration is a constrained class declaration of the form
class C : ClassInterface { ... }
then the specification is
class C : ClassInterface
- If the declaration is an unconstrained class declaration of the form ...
- If the declaration is a value binding of the form
val (x1 : t1, ..., xn : tn) = Expression
Then there are n corresponding specifications
val x1 : t1
···
val xn : tn
What about type parameters??
Note that local is a fairly crude tool to define an abstract interface;
our intention is that one will use signature ascription to define abstraction
boundries at the package (or source group) level, and that the modules in
a given group will have access to each other's internal types.
7.4 Parameterized modules
Each instance of a parameterized module has its own state.
Here is an example of a generic list sorting module that is parameterized
over the element type and ordering function.
module ListSortFn (E : {type T val cmp : (T, T) -> Order})
{
fun sort (l : List(E.T)) -> List(E.T) {
fun ins : (E.T, List(E.T)) -> List(E.T) {
(x, Nil) => Cons(x, Nil),
(x, Cons(y, ys)) => if (E.cmp(x, y) is Greater)
then Cons(y, ins(x, ys))
else Cons(x, Cons(y, ys))
};
fun lp : (List(E.T), List(E.T)) -> List(E.T) {
(Nil, l) => l,
(Cons(x, xs), l) => lp (xs, ins(x, l))
};
lp (l, Nil)
}
}
7.5 Declarations
Declarations make up the body of a module.
A declaration may be annotated with the local keyword, which
means that it is not visible outside its module.
All other declarations are visible outside the module, although they
may be hidden later using signature ascription (see Section ??).
Moby provides declaration forms for submodules, types, classes,
constants, functions, and values.
Module declarations have already been discussed in Section 7.3,
and we postpone the discussion of type and class declarations to
chapters 8 and 9 respectively.
7.5.1 Constant declarations
Constant declarations introduce symbolic names for constant values.
Unlike in the case of value bindings, these names are in the class
of data-constructor identifiers and can be used in pattern matching.
Furthermore, Moby allows constants to be parameterized over a tuple
of free variables.
The right-hand-side of a constant declaration must be a pattern expression.
These restricted patterns are described in Section 12.4.
7.5.2 Function declarations
There are two forms of function definition: the first supports curried
definitions without pattern matching, whereas the second supports an
equational style of definition without currying.
The function definition syntax is also used in the syntax of
function expressions (see Section 11.11.1) and method
declarations (see Section 9.2.2).
The following example illustrates both forms of function declaration:
fun map [s, t] (f : s -> t) (l : List(s)) -> List(t) {
fun mapf : List(s) -> List(t) {
Nil => Nil,
Cons(x, xs) => Cons(f x, mapf xs)
};
mapf l
}
The map function is a curried definition and its body is a block
consisting of the definition of mapf and its application to
the list l (blocks are described in Section 11.1).
The definition of mapf uses the equational style.
explain s and t.
7.5.3 Value declarations
7.5.4 Recursive declarations and scope
Type, class and function declarations in Moby may be
recursive.
To allow programmers flexibility in the way they organize
their code, Moby allows declarations to include forward references
to other identifiers bound at the same level1.
To avoid nonsensical definitions and recursion through
nested modules, however, there are some restrictions.
Let d1 ··· dn be a sequence of declarations,
let Vi be the set of names bound by declaration
di, and let Fi be the free names of the right hand
side of di.
Then, we say that vÎ Vi is fully defined at
declaration j >= i, if for every v'Î Fi, it is
the case that there exists k < j with v'Î Vk.
Given this definition, we place five restrictions on the declarations
that make up a module body:
-
At the point of the last declaration in the module body, all names
defined in the module must be fully defined.
- Names may not be redefined.
we might weaken this restriction to apply only to type and module names
- The names defined by type abbreviations (see Section 8.1)
and value declarations (see Section 7.5.3) must
be fully defined at their point of declaration.
- Only fully defined names are visible inside a nested module.
- Type bounds must be fully defined.
The third restriction is sufficient to avoid nonsensical definitions
and the fourth avoids the problem of recursion through nested modules.
For example, the following declarations are well-formed:
fun f (x : Int) : Int { g (x-1) }
fun g (y : Int) : Int { y+1 }
module M {
val a = f 1
fun h () -> Int { a }
}
val w = M.h()
Notice that w has a dependency on f and g via the nested
module M.
Since module M imports f, we cannot move the definition of
g to after M.
If we did so, then f would not be fully defined at the point of M's
declaration and thus would not be visibile inside M.
7.6 Signature Matching
- 1
-
By level, we mean the module nesting level.