Module Types

Support is provided for defining module types . These are essentially record types  , where the type of each field of an instance can depend on previous fields of the instance. They are very useful for defining ADT's  (abstract data types  ) and algebraic classes. Module types are allowed to have parameters. For example, an ADT for queues could be created that takes the type of queue elements as a parameter. Module types are currently implemented using Nuprl 's type.

An ML function create_module  helps with setting up new module type definitions, adding projection functions, and updating the

AbReduce tactic to recognize applications of the projection functions.

The create_module function should be used as follows:

1. Pick a name for your module; say modname.
2. Create an ML object create_ modname to hold the create_module invocation. The invocation needs to be part of the library to ensure that the relevant computation rules are added each time the theory containing the module definition is loaded. The function only creates the definition objects themselves if they are initially absent. The invocation also serves to document the module. With the abstractions explained below, it presents a clearer and more succinct account of the module structure than do the definitions themselves that make up the module.

3. It is most elegant to use a few abstractions to pretty up the invocation. Remember, when you have a text cursor in a text sequence, a term slot can be opened up using C-U , and when you have a term cursor at an empty term slot, a text sequence can be inserted using C-; .

   The abstractions for modules currently reside in the ml_1 theory.

   The abstraction holding the create_module invocation has the editor alias classdecl. Enter it in the ML object by opening up a term slot in the object's top level text sequence, and typing the name classdecl. By keeping the top level of the ML object a text sequence, you are free for example to add ML comments preceding the create_module invocation. Without fields filled in, the class declaration template should look like:

   

4. Enter modname for the Long Name  and some abbreviation of this for the Short Name . The short name is used as a prefix for the names of the projection functions.

5. Initialize the [parms] and [fields] slots with empty text sequences.

6. Open up a term slot in the Parameters list for each parameter. Parameters are pairs of variable names and types. They should be entered using another abstraction with alias name mlbd. This initially looks like

   

   where [var] is a text slot for the variable name, and [type] is a term slot for the corresponding type of the variable. If there are no parameters, just leave the empty text sequence in this slot.

7. Open up a term slot in the Fields list for each field. As with parameters, you can use the mlbd abstraction for the fieldname and field type. Alternatively, you can use the mlbde abstraction:

   

   This has an extra term slot for an example of the projection function for that field. Initially, leave the term slot empty. Enter in the [var] slot the name of the field. The name of the projection function will be the name entered here with a suffix of the short module name. The type of a field can refer to constant types, the inhabitants of earlier fields or parameters.

   Since the mlbd or mlbde terms are embedded in a text sequence, you can insert linebreaks in the sequence, by simply getting a text cursor in the sequence and typing RETURN .

8. Fill in the [uni] slot with an appropriate universe term. This should be the lowest universe that the module type inhabits. For example, if the module type itself involves no universes, then this probably will be ; if the module type involves universe terms , then this will be , (commonly abbreviated to ).

   Here is an example of a class definition that has been instantiated according to the procedure given so far:

   

9. If you now check this object (use C-X ch), the definitions for the module are created in the library. For the above example, the following definitions are created:

   

10. If desired, edit the display forms for the module type and for the projections. For example, the display forms could be changed to:

    

    Here a couple of abbreviated display forms are defined for the the module type, one of which hides the level expression in the case that it is simply the level variable i. Standard notation is chosen for the carrier, and the action is denoted by a ` ' character. To avoid clutter, a display form for the action is defined that hides the instance of the action_set module. This can nearly always be determined from context.

11. Fill in the [example] slots in the module declaration. These serve purely to document the module, and are discarded when the system unfolds the class declaration abstraction into raw ML code. In the [example] slot on the first line, you should put an instance of the module type, with the same parameter names as declared in the Parameters section. You might also insert a membership term or an mlbd term to indicate a prototypical element. For the above example, you could insert the term s ASet(T) indicating that s is a prototypical element.

    Fill in the example slots of the mlbd terms with examples of the relevant projection functions, operating on the prototypical element declared in the uppermost example slot. In the example, the terms |s| and s could be used.

    With the given display form changes, and example terms, the final version of the example class definition looks like:

    

12. Exit the create_ modname object.

Examples of class definitions can be found in many of the algebra theories.