Why can modules only import other modules?

Stream: lean4

[Mario Xerxes Castelán Castro 🇲🇽]

<https://lean-lang.org/doc/reference/latest/The-Module-System/>

modules can only import other modules so adoption has to be done top-down.

Why does this restriction exist?

[Niels Voss]

Not sure, but if A imports B and B is a module, then B's restrictions on things like definitional equalities and private definitions only apply to A if A is a module as well. So if we could have X imports Y which imports Z, where X and Z are modules and Y isn't, then we could have that Y uses private theorems in Z, then we could have that X gains access to private definitions in Z indirectly.

[Robin Arnez]

modules impose certain restrictions that non-modules can easily break. For example, consider this non-module:

private def myPrivateProposition := True

theorem myPublicProof : myPrivateProposition := trivial

modules have the restriction that types of public declarations can't refer to private declarations. Why? Well, when in a module, private declarations are not imported by default. That means that if you could import this non-module in a module, you'd have a public declaration, myPublicProof, in the environment which refers to myPrivateProposition which, to the knowledge of the importer, doesn't exist!