1.6.1. higher-order functors

1.6.2. structure definition specs

1.6.3. where clause for structure definitions

1.6.4. Layered Redefinitions Ignored

Structure definition specs can easily give rise to redefinitions. Consider the following example:

  signature S1 =
  sig
    type t
  end;

  signature S2 =
  sig
    structure A : S1
    structure B : S1 = A
  end;

  signature S3 =
  sig
    structure C : S2
    structure D : S2 = C
  end;

Here the substructure D.B of S3 is defined within S2 in terms of D.A (implying D.B.t = D.A.t), while by the definitional spec in S3, D.B is equal to C.B (implying D.B.t = C.B.t).

There are two ways of dealing with such secondary, or layered definitional specs.

1. Secondary definitions can be treated as errors (excepting those cases where the equivalence of the definitions can easily be verified). This was the policy for 110.0.3 through 110.8, where examples like the above gave rise to the error message

           Error: possibly inconsistent structure definitions
         

   [This was bug 1354.]
2. The redefinitions can be regarded as producing implied sharing constraints (e.g. D.A.t = C.B.t in this case).

In case (2), these implied sharing constraints will be verified automatically during signature matching, in the process of matching all the definitional specifications. The question is whether they should be taken into account (i.e. satisfied) when instantiating a signature like S3. We adopt the lenient policy of not dealing with these implied constraints during instantiation. Instead, during instantiation secondary definitions are simply ignored. In the example, the inner definition D.B.t = D.A.t takes effect while the secondary definition D.B.t = C.B.t is ignored.

The consequence of this policy is that some additional inconsistent signatures will be successfully instantiated. As usual, any attempt to match these inconsistent signatures will fail.

The compiler flag

  Compiler.Control.multDefWarn : bool ref

controls whether a warning message will be generated when a secondary definition is ignored. It's default value is false, meaning no warning messages will be produced.

We follow a stricter policy in some other cases, such as layered type definition specs:

  signature S = sig
    type t
    type s = t
  end where type s = int

Here the secondary redefinition "where type s = int" is detected and causes an error message.

  Error: where type defn applied to definitional spec: s

NOTE: This is an SML/NJ divergence, since the above signature is legal in SML '97. See Note "Sharable Types" below.

1.6.4. type spec merging with include