Can a structure implement multiple signatures in Standard ML?

Question

I've recently got wondering whether Standard ML structures can implement multiple signatures, similar to how a class can implement multiple interfaces in Java. A quick search revealed this web page where Bob Harper says that this would, indeed, be possible (emphasis mine): [...] the relationship between signatures and structures in ML is many-to-many, whereas in some languages (such as Modula-2) the relationship is one-to-one or many-to-one. This means that in ML a signature may serve as the interface for many different structures, and that a structure may implement many different signatures. However, I can't find the syntax and a cursory look over the grammar of modules in the revised definition doesn't seem to support the above quote. My questions are: - Is it possible? - If yes, what's the syntax? EDIT: After some playing around, I think that Bob Harper was actually referring to signature matching. This snippet is a small example where a structure is found as a match for two differ…

Accepted Answer

There is no syntax to enforce it with a single annotation, but you could e.g. do

```
structure C = struct ... end
structure C1 : S1 = C
structure C2 : S2 = C
```

If you merely want to have the sanity checks but avoid polluting the scope with auxiliary structure names, you could make them local:

```
structure C = struct ... end
local
  structure C1 : S1 = C
  structure C2 : S2 = C
in end
```

Unfortunately, one cannot use wildcards in structure bindings...

The notation you suggested would be tricky, since it effectively would introduce an intersection operator on signatures. That has far-reaching consequences. Consider, for example:

```
signature S1 = sig type 'a t; val v : int t; val w : string t end
signature S2 = sig val v : int end
functor F (X : S1 and S2) = (* what is X.t here? *)
```

There are two possible solutions for what type `X.t` could be so that the type of `X.v` is consistent with both signatures: either

```
type 'a t = int
```

or

```
type 'a t = 'a
```

The problem is that they are incomparable, i.e., none is better than the other. In one case `X.w` would be an int, in the other a string. Essentially, what is happening here is that you'd introduce a form of higher-order unification through the backdoor, which is known to be undecidable in the general case.

Can a structure implement multiple signatures in Standard ML?

Solution

Problem