Default conventions in module importations

We have already explained our default convention when a submodule $M_{0}$ is imported indirectly and transitively into $M$ through the direct importation by $M$ of a module $M_{1}$ that itself imports $M_{0}$. Then, whatever was the mode (protecting, extending, or including) in which $M_{0}$ was imported by $M_{1}$ is also, by default, the mode in which $M_{0}$ is imported by $M$, unless $M$ contains an explicit declaration importing $M_{0}$ in a different mode. We now explain what our default convention is in the case of diamond importations.

We talk of a diamond importation of $M_{0}$ by $M$, when $M_{0}$ is imported indirectly by $M$ through the direct importation of two or more different modules, say $M_{1},M_{2}, \ldots, M_{k}$. The problem now is that $M_{0}$ can be imported by each of the modules $M_{1},M_{2}, \ldots, M_{k}$ in different modes. For example, $M_{1}$ could import it in protecting mode, $M_{2}$ in extending mode, $M_{3}$ in including mode, and so on. What should now be the default convention for the mode in which $M$ imports $M_{0}$? We adopt a convention that is consistent with a logical understanding of such importation declarations. Indeed, such declarations impose semantic constraints of decreasing strength; that is, we have:

$$\texttt{protecting} \; M_{0} \;\; \Rightarrow \;\; \texttt{ex... ...g} \; M_{0} \;\; \Rightarrow \;\; \texttt{including} \; M_{0} .$$

The default convention consistent with this logical reading is that the strongest mode wins, i.e., protecting prevails over extending, which itself prevails over including. This is because we view the set of all such importing mode declarations as a conjunction, and exploit the logical equivalence between $A \Rightarrow B$ and $(A \wedge B) \Leftrightarrow A$.

Note that this ``strongest wins'' default mode may not always be the correct or intended mode in which $M$ should import $M_{0}$. Sometimes it may not be, and then the user should overrule the default convention by declaring explicitly a different mode in which $M$ imports $M_{0}$. A pragmatic reason why this need for overruling the default mode may arise is that, although a weaker mode of importation (say extending) does not logically preclude such an importation also satisfying a stronger one (say protecting), in practice, when we declare an importation in a weaker mode it can often be because we know or suspect that it fails to satisfy a stronger mode. For example, when we say ``extending'' we may often mean ``extending and not protecting.''