RFC: `Unit` types in FFI

Stream: lean4

[Cameron Zwarich]

At the moment, inductive types like Unit that have a single constructor with no (relevant) fields are represented as a boxed scalar 0, including in the FFI. It would be more efficient to not represent these types at runtime (either as function arguments, return values, or in structure fields). Is there any reason that this might be a bad idea?

Just to be clear, I'm not talking about changing how Unit (and other relevant types) suffice for preserving data dependencies, e.g. for implementing IO. However, at the C language level (and the Lean IR level), pure data dependencies don't really buy you much, and I don't see how this would be useful for enforcing any desirable properties at this level of abstraction.

[Aaron Liu]

Proofs are also represented as 0 I think

[Edward van de Meent]

i seem to recall this is sometimes done to delay certain computations? i see you already adressed that

[Cameron Zwarich]

Aaron Liu said:

Proofs are also represented as 0 I think

Prop and type-formers are represented as 0 (when they are required to be represented). The compiler goes out of its way to extract _redArg versions of Lean functions that omit the irrelevant/unused parameters, and then replaces the original function with a call to the _redArg one, so in most situations they are effectively eliminated.

For extern functions, they are entirely eliminated. For export functions defined in Lean, they are not eliminated (just like for other Lean functions).

[Eric Wieser]

I think such a change might be quite disruptive to existing FFI users. Is there any hope of lean4#5829 happening first, so that such ABI changes become API build failure instead of mysterious crashes?

[Cameron Zwarich]

@Eric Wieser The likely disruption is my main hesitation. I did cause some minor ABI breakage in some followup changes to the new compiler switch just by fixing bugs/asymmetries (which would have likely caused some future correctness problems if they weren't fixed), but this would be a different level.

I was unaware of that issue you filed, so thanks for pointing it out. I'm not sure if it would be sufficient mitigation for the fallout of this change, but I think it would definitely be necessary.