feat: tighten inductive FFI description#863
Conversation
|
|
||
| If an inductive type has exactly one constructor, and that constructor has exactly one run-time relevant parameter, then the inductive type is represented identically to its parameter. | ||
|
|
||
| For a public inductive type under the module system, any private information that prevents these conditions from being tested in other modules will disable this optimization even in the current module. |
There was a problem hiding this comment.
This took me some time to parse out and think through, so let me unpack my understanding to check for correctness:
If a public inductive type is defined in a module and its constructor is private, then this optimization is not applied even in the module that defines it. This is because the ABI of a module's types is determined by the module's interface (that is, its public information). If the optimization were applied only in the defining module, then this would lead to an ABI mismatch. Furthermore, the structure of the private constructor could change without affecting the module's public information. Making the entire type private or its constructor public re-enables the optimization because all clients are able to decide this.
Is that a correct understanding? If so, then presumably one could work around it by having a non-exposed public def that names the type externally? If not, then why not?
There was a problem hiding this comment.
Correct! But a non-exposed type def is not sufficient as judging its run-time relevancy still requires accessing private data
There was a problem hiding this comment.
Which actually is the reason such a non-exposed type def is currently denied if the RHS is not publicly imported. It would be nice to lift both restrictions at once in the future...
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
2 participants
Addresses both #13679 and more general compiler freedom