5. Module System

The module system is based on the two primitive concepts of signatures and signature morphisms. Intuitively, a signature is a named list of declarations. Signature morphisms have a domain and a codomain signature and a signature morphism from S to T maps all declarations of S to expressions over T. Such a mapping induces mappings of all S-expressions to T-expressions by homomorphic extension.

Signature morphisms can be composed in the obvious way. The atomic signature morphisms are called links, and we distinguish two kinds of links: views and structures. A view from S to T is declared on toplevel and must provide an instantiation for every declaration of S. Views encode translations and representations of signatures. A structure from S to T is declared within T and has the effect of copying the declarations of S into T. A structure may have instantiations for some declarations of S, in which case the S-declarations are not only copied but also translated. Structures encode inheritance and instantiation.

5.1 Signature Declaration

Signatures are lists of declarations. Signature declarations introduce a name for a signature. Signatures may start with include declarations (see see section Include Declaration).

sigdecl  ::= id = { includes decls }.

decls    ::= 
           | decls decl

The following is an example of a signature declaration for the basic judgments of propositional logic. We will use this as our running example.

%sig JUDGMENTS = {
  o : type.		    %name o A.
 
  nd : o -> type.	    %name nd D.
}.

5.2 Structure Declaration

Structure declarations copy and translate the declarations of a signature into the current signature. The structure has a name that is used to form qualified names for the copied declarations. A structure may be defined by a list of instantiations (If omitted, the empty list is assumed.) or by a morphism. An instantiation assigns an object to a constant identifier or a morphism to a structure identifier.

A structure declaration may contain an open declaration (see see section Open Declaration).

strdecl ::= id : id               open.
          | id : id = { insts } open.
          | id : id = morph       open.

insts   ::=
          | insts         id := term.
          | insts %struct id := morph.

The following signatures contain a structure that copies the signature JUDGMENTS and adds declarations for implication and negation, respectively.

%sig IMPLICATION = {
  %struct J : JUDGMENTS.
  imp    : J.o -> J.o -> J.o.	    %infix right 10 imp.
  impi   : (J.nd A -> J.nd B) -> J.nd (A imp B).
  impe   : J.nd (A imp B) -> J.nd A -> J.nd B.
}.

%sig NEGATION = {
  %struct J : JUDGMENTS.
  not : J.o -> J.o.
  noti : (J.nd A -> {B} J.nd B) -> J.nd (not A).
  note : J.nd (not A) -> J.nd A -> {B} J.nd B.
}.

Twelf mirrors the structure declaration as well as the induced constant declarations. The mirrored declarations give the semantics of structure declarations in terms of non-modular declarations. In the implication example, Twelf prints:

%struct J : JUDGMENTS = {}.
%% induced: J.o : type.
%% induced: J.nd : J.o -> type.

The above example also shows that a structure declaration of the form s : S just abbreviates one with an empty list of instantiations, i.e., s : S = {}. If instantiations are given, they induce defined constants. This can be used to represent parametric theories as in the following example.

%sig List = {
  elem : type.
  list : type.
  nil  : list.
  cons : elem -> list -> list.
}.

%sig Nat = {
  nat  : type.
  zero : nat.
  succ : nat -> nat.
  %struct l : List = {elem := nat.}.
  010  : l.list = l.cons zero (l.cons (succ zero) (l.cons zero l.nil)).
}.

Here the structure is mirrored by Twelf as:

%struct l : List = {elem := nat.}.
%% induced: l.elem : type = nat.
%% induced: l.list : type.
%% induced: l.nil  : l.list.
%% induced: l.cons : l.elem -> l.list -> l.list.

Here elem := nat is an instantiation of a constant. We say that the constant elem of List (the domain of the link) is instantiated with the expression nat of Nat (the codomain of the link). Similarly, it is possible to instantiate a structure of the domain signature with a structure expression of the codomain signature. This is used in the following example, where IMPLICATION and NEGATION are combined into a signature PL sharing the common structure J.

%sig PL = { 
  %struct I : IMPLICATION.
  %struct N : NEGATION = {%struct J := I.J.}.
}.

Here in J := I.J, J is the structure declared in NEGATION, and I.J is the structure J declared in IMPLICATION and then copied into PL by the structure I. The structure N leads to the following induced declarations:

%struct N : NEGATION = {%struct J := I.J.}.
%% induced: %struct N.J = I.J.
%% induced: N.J.o = I.J.o.
%% induced: N.J.nd = I.J.nd.
%% induced: N.not : N.J.o -> N.J.o.
%% induced: N.noti : (N.J.nd A -> {B} N.J.nd B) -> N.J.nd (N.not A).
%% induced: N.note : N.J.nd (N.not A) -> N.J.nd A -> {B} N.J.nd B.

Two things should be noted here: Firstly, all induced constants of NEGATION lead to induced constants in PL, e.g., N.J.o; these are generated in depth-first order (and thus can be looked up in constant time). Secondly, just like structure declarations induce constant declarations, the structure instantiation J := I.J induces constant instantiations leading to, e.g., the definiens I.J.o of N.J.o.

It is not necessary to instantiate structures; instead, the induced constants can be instantiated directly. Consider the structure N of PL: If we write J.o := I.J.o. J.nd := I.J.nd instead of J := I.J, we obtain the same induced constant declarations as above.

5.3 View Declaration

The syntax for views is similar to that of structures. The main difference is that the codomain signature is given explicitly.

viewdecl ::= id : id -> id = { insts }.
           | id : id -> id = morph.

To give an example of a view, let us assume a variant of PL that uses falsity instead of negation:

%sig PL' = {
  %struct I : IMPLICATION.
  false : I.o.
  falseE : I.nd false -> {A} I.nd A.
}.

A view from PL' to PL expresses that negation can be represented in terms of falsity. Such a view must provide instantiations for all constants of the domain.

%view PL2PL' : PL -> PL' = {
  %struct I := I.
  N.not  := [A] A I.imp false.
  N.noti := [A] [D:I.J.nd A -> {B} I.J.nd B] I.impi D false.
  N.note := [A] [D:I.J.nd (A I.imp false)] [E:I.J.nd A] [B] falseE (impe D E) B.
}.

Note that implicit arguments, e.g., A of N.noti must be bound explicitly due to a restriction of the current implementation. They must be listed in the same order in which they occur in the declaration of the instantiated constant.

Above the instantiation %struct I := I. induces constant instantiations I.c := I.c. for all constants c of IMPLICATION, including its induced constants. Alternatively, these instantiations could have been given separately. For example, the following instantiations have the same semantics as %struct I := I.

  %struct I.J := I.J.
  I.imp  := [A][B] A I.imp B.
  I.impi := [A][B][D] I.impi D.
  I.impe := [A][B][D][E] I.impe D E.

The view is only well-formed if all instantiations type-check against the translated type. In the above example, this means that [A] [D:I.J.nd A -> {B} I.J.nd B] I.impi D false must type check against the translation of {A}{B}(N.J.nd A -> {B} N.J.nd B) -> N.J.nd (N.not A) along v, which yields {A}{B}(I.J.nd A -> {B} I.J.nd B) -> I.J.nd (A imp false) after normalization. Note that this translation is only possible if the instantiation of N.not is already known. Therefore, the order of instantiations in a view must respect the dependency order of the declarations in the domain.

5.4 Include Declaration

A structure with domain S imports S in the sense that it creates a fresh copy of S. Multiple imports of the same signature are always distinguished, and the names of the structures are used to disambiguate them. This is not always the desired behavior. Consider the following signatures for the basic algebraic hierarchy (where we omit the axioms).

%sig FOL = { 
  i : type.        %% terms
  o : type.        %% formulas
  nd : o -> type. %% truth judgment
}.

%sig Monoid = { 
  %include FOL.
  comp : FOL..i -> FOL..i -> FOL..i. %% composition
  unit : FOL..i.                     %% unit element
}.

%sig CommutativeGroup = {
  %include FOL.
  %struct mon : Monoid.
  inv : FOL..i -> FOL..i.            %% inverse element
}.

%sig Ring = {
  %include FOL.
  %struct add : CommutativeGroupg.   %% additive operations
  %struct mult : Ring                %% multiplicative operations
}.

Here the signature Monoid is imported into Ring in two different ways: via add.mon and via mult. This results for example in the constants add.mon.comp (addition) and mult.comp (multiplication). However, the signature FOL, which is also imported in multiple ways, should be the same in all signatures. This is the role of include declarations.

An include declaration creates an unnamed inclusion morphism into the current signature. Inclusions are transitive, and if the same signature is included in multiple ways, multiply included constants are identified. (Here two signatures are equal iff they have the same name.) References to included symbols are formed by prefixing the symbol name with the signature name using the separator ...

An include declaration may contain an open declaration (see see section Open Declaration).

includes ::= 
           | includes %include id open.

Due to a restriction of the current implementation, links cannot contain instantiations of included constants. Rather, the codomain of every link must include (possibly indirectly) all signatures that are included in the domain signature. For example, if the inclusion from FOL to Ring were removed, then the structures add and mult would be ill-formed.

5.5 Morphisms

A morphism is a list of link identifiers.

morph   ::=
          | morph id

Iuxtaposition is composition of morphisms in diagram order, and with respect to inclusions morphism typing is co- and contravariant in the usual way of function types.

More formally, let < be the reflexive-transitive closure of the is-included-into relation. Then a morphism of the form l_1 ... l_n where each l_i is a view or a structure (where the structure name must be prefixed with the name of the containing signature) from S_i to T_i is well-formed with domain S and codomain T iff: S<S_1, T_i<S_{i+1} for i=1,...,n-1, and T_n<T. Morphisms translate included symbols to themselves.

For example, we have that IMPLICATION..J PL..I PL2PL' is a morphism from JUDGMENTS to PL' in the logic example.

Two morphisms are equal if they are identical after expanding defined links. For example, CommutativeGroup..mon Ring..add and Ring..add.mon are two equal morphisms from Monoid to Ring in the algebra example.

5.6 Open Declaration

Structure and include declarations may carry optional open declarations These permit to avoid qualified names.

open ::= 
       | %open ids.
ids  ::=
       | ids id

The semantics of %open i is that the identifier i is resolved in the domain signature of the structure or inclusion, and i is installed as a short-cut to the resolution. i must be an available name in the signature containing the open declaration.

For example, one would normally write the signatures IMPLICATION and Monoid from the examples above as

%sig IMPLICATION = {
  %struct J : JUDGMENTS %open o nd.
  imp    : o -> o -> o.	    %infix right 10 imp.
  impi   : (nd A -> nd B) -> nd (A imp B).
  impe   : nd (A imp B) -> nd A -> nd B.
}.

%sig Monoid = { 
  %include FOL %open i.
  comp : i -> i -> i.
  unit : i.
}.

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.