Order for testing subtyping between modules

[alexcrichton]

This is an issue for the design proposed in #3 (assumed to be merged in the near-ish future) where I'm curious how the subtyping relationship works between modules. Talking with @lukewagner it sounds like import strings are going to be taken into account, but this raises a question about what to do with imports that import from the same string? For example I'm curious if this module is intended to validate:

(module 
    (module $a
        (import "anything_here" (module (;$a.b;)
            (import "" (instance (;$a.1;)
                (export "bar" (func))
                (export "foo" (func))
            ))
            (import "" (instance (;$a.2;)
                (export "foo" (func))
            ))
        ))
    )

    (module $b
        (import "" (instance (;$b.1;)
            (export "bar" (func))
        ))
        (import "" (instance (;$b.2;)
            (export "foo" (func))
        ))
    )
    
    (instance (instantiate $a (module $b)))
)

A similar question would be if the imports of $b were swapped, would it still validate?

I think one possible way to test if $a is a subtype of $b would be to:

• Build a map from import string to number of items imported from that import string of $b
• For each import name n of $a, look up its import string in this map.
• If n exists in $b with only one item imported, then the subtyping check recurses (switching order for covariance/contravariance?)
• If n exists in $b, but with multiple items imported, then the first unused import (so far) of $b is tested against the import.
• If n doesn't exist in $b it could do the same as above (check the first unused import) or return an error.

The thinking is that on collisions (multiple imports from the same name) implementations would fall back to order-based comparisons of types. Otherwise you'd do name-based comparisons. This would allow, in general, imports to get reordered or deleted and you wouldn't break code which depends on you (as it would still assert your older type). If, however, all your import names were the same string then it'd be stricter.

I'm curious though if others have thoughts about how this might work? Or how to handle the subtyping relationship between modules with respect to their imports and multiple imports from the same name?

[rossberg]

Ouch, yeah, that's a bit nasty. The canonical semantics would be treating multiple imports from the same name as a form of intersection type. That implies the rule that for each import in the subtype, there must exist a suitable import in the supertype. This is independent of any order. It may relate multiple sub-imports to the same super-import (or vice versa), but that's actually what you want.

What's annoying about this, though, is that for each sub-import you may have to try multiple super ones, i.e., it can be quadratic in the number of overlapping imports. That may be okay in this case, but still.

[lukewagner]

Interesting. So as currently written in the PR, an import $A:

(import "" (module $A
  (import "foo" (func))
  (import "foo" (func))
  (import "bar" (func))
))

would accept $B:

(module $B
  (func (import "foo"))
  (func (import "foo"))
  (func (import "bar"))
)

b/c it's the same type (no subtyping rule needed). But would $C be accepted:

(module $C
  (func (import "foo"))
  (func (import "foo"))
)

which requires subtyping? I suppose it could be made to if there was a prefix-compatibility rule added to subtyping. Presumably $D would be rejected due to ambiguity:

(module $D
  (func (import "foo"))
  (func (import "bar"))
  (func (import "foo"))
))

Perhaps we should disallow duplicates in the imports of module imports since it leads to all this wackiness?

[alexcrichton]

@lukewagner your examples have export, but did you mean import? (duplicate names are already disallowed in export directives IIRC)

[lukewagner]

Oops! Somehow I forgot that we already disallowed export duplicates and tried to "simplify" my examples :P I'll edit the comment in-place.

[rossberg]

@lukewagner, when interpreting same-named imports as intersection types then the order does not matter. For example,

(module $B
  (import "foo" (func))
  (import "foo" (func))
  (import "bar" (func))
)

morally would be

(module $B
  (import "foo" (func) /\ (func))
  (import "bar" (func))
)

And $D would be the same. So it would match just fine. (The intersection here can actually be simplified to just (func), but not so in other cases, such as module imports with different types.)

The subyping rules for intersection types are as follows:

(1) U /\ V <: T  iff U <: T or V <: T
(2) T <: U /\ V  iff T <: U and T <: V

(where T and U themselves cannot be intersections). Taken together, these allow U <: U /\ U, U /\ V <: U, or U /\ V <: V /\ U, for example. But you generally end up having to test multiple combinations due to the "or" for occurrences on the lhs (though imports are contravariant, so the checks would actually turn around).

Although attractive, I doubt that we can disallow duplicates in imports, for at least two reasons:

• It would be a breaking change for modules. And we want to be able to express the type of any valid module, so we cannot disallow it for module types either.
• The desugaring of multi-level imports depends on it, at least when mixing multiple levels (see my earlier comment).

What we could try to restrict, though, would be the subtyping rules, in order to avoid the "or". But we have to be careful to maintain crucial properties, such as reflexivity (i.e., the equivalent of U /\ V <: U /\ V must still hold).

One possibility avoiding the "or" would be to weaken the above rules to

(1A) U1 /\ ... /\ UN <: T1 /\ ... /\ TN  iff U1 <: T1 and ... and UN <: TN
(1B) U1 /\ ... /\ UN <: top

where T and U themselves can not be intersections anymore. The effect would be that matching multiple imports in a supertype becomes positional per name. That is, the only subtype of a module with multiple imports for "foo" is one with no "foo" imports at all (corresponding to top), or one with the exact same number and in a compatible order. Interleaving with imports of other name does not matter.

Concretely, that would allow (assume T <: T' and S <: S')

(module) <: (module (import "foo" T) (import "foo" S))
(module (import "foo" T') (import "foo" S')) <: (module (import "foo" T) (import "foo" S))

but not

(module (import "foo" T')) <: (module (import "foo" T) (import "foo" T))
(module (import "foo" T') (import "foo" T')) <: (module (import "foo" T))   (*)

This may be somewhat restrictive, though. Ruling out (*) makes it impossible to use a module with multi-imports in a context where one sufficiently general import is actually provided. We could remedy that by reintroducing an equivalent of rule (2):

(2') U <: T1 /\ ... /\ TN  iff U <: T1 and ... and U <: TN

This would allow (*), that is, a module with exactly one import for "foo" may still be matched by one with multiple ones. That's still fine, because there always is a uniquely determined import in the supertype to match against, so it remains linear. I kind of suspect that we'd need this to handle multi-level imports in an actual module definition sufficiently well (and we should disallow that sugar in module types!).

[lukewagner]

@rossberg Let me start by trying to digest the first bit with intersection types :) When you say that $B (as I wrote above) is equivalent to:

(module $B
  (import "foo" (func) /\ (func))
  (import "bar" (func))
)

Given that function closures have identity, I think this would only work if the type of $A was similarly equivalent to:

(import "" (module $A
  (import "foo" (func) /\ (func))
  (import "bar" (func))
))

With the critical implication that instantiate ends up taking two operands, not three. Because this situation applies just as well to two-level imports, I was thinking this would be a breaking change... but maybe not? Is that what you were thinking?

[rossberg]

@lukewagner, in contexts identifying imports by name (such as with the JS API's instantiate function) we already "merge" imports with the same name. So nothing changes there.

As for positional contexts, we don't currently have them anywhere in the standard (only in the C API), so I don't think it'd be a breaking change. Just like you proposed that subtyping can reorder imports, it could also merge imports, and instantiate uses whichever view the type at hand provides.

However, it is true that the "or" rule would make this "coercion" more tricky (or even ambiguous?), so perhaps another reason to avoid it.

[lukewagner]

Yes, that was my question; we can't allow:

(module (import "foo" T')) <: (module (import "foo" T) (import "foo" T))

because then there would be an ambiguity when two distinct funcaddrs are supplied to instantiate the supertype.

An alternative to weakening the rules to avoid "or" is to change the abstract syntax of module types to be an unordered map of names (with duplicates in the text/binary parsed into intersection types which, btw, nicely ensures the "no nested intersection types" property). Then there is never an ambiguity because there is always exactly 1 function value. The abstract syntax of instantiate could also take names and it's just a binary/text encoding detail that the names are lifted from the identified module type. This seems somewhat simpler to think about to me.

[rossberg]

An alternative to weakening the rules to avoid "or" is to change the abstract syntax of module types to be an unordered map of names

But that's incompatible with a positional interpretation of module imports in the instantiate construct.

[lukewagner]

@rossberg What I was perhaps-too-briefly suggesting in my last comment was that instantiate, in the abstract syntax (and thus validation and runtime semantics), would contain an ordered list of names (the order determining the order to pop operands) and it's just a binary and textual encoding detail that the way those names are specified is via the module index immediate (essentially "factoring out" the ordered list of names from N instantiate instructions to 1 module type definition).

[rossberg]

@lukewagner, I see, but how would that express the type of an existing module with multiple "foo" imports? You have to represent the intersection inherent in that somehow. Whether that's by multiple entries for "foo" or by one with multiple types is just a syntactic detail. If we want to avoid the "or" then this intersection must be ordered, no matter how it is represented.

[lukewagner]

@rossberg As long as duplicates are always collapsed into a single import of an intersection type (by necessity, if types are unordered maps), then I think there should never be any ambiguity (for any import, there will be exactly one value supplied by instantiate) so the "or" seems fine; I don't see a need to avoid it.

[rossberg]

@lukewagner, oh, okay, so you are just worrying about the value ambiguity, not the "or" per se. But you'd need to introduce intersection types as an explicit concept then. You could equivalently say that in a positional interpretation of imports, duplicate entries are omitted. That has the same net effect without introducing a new construct.

Btw, an unordered interpretation of imports won't work for other reasons: it is incompatible with having dependencies between imports, as with types. That is, the same reason why this proposal requires that static declarations within a module are ordered applies within module types as well.

[lukewagner]

@rossberg Ah hah, that's a good reason for maintaining positional order.

Could you explain a bit more of what you mean by saying "duplicate entries are omitted"? In all module types or just for the purposes of subtyping?

[rossberg]

@lukewagner, in contexts where a module type is interpreted positionally to determine argument values (e.g., an instantiate instruction), only the first occurrence of each top-level) import name would be taken into account. Of course, the value would still be checked against all the other types.

Sounds a bit more hacky perhaps, but I would have the exact same effect as introducing and rewriting to intersection types.