computable functions aren't closed under composition

Stream: lean4

[Alex Meiburg]

I've been running into some sad/frustrating issues where I'll have two not-noncomputable functions, f and g, but their composition is noncomputable. Essentially this happens because some of the compiler optimizations are nondeterministic. (Okay, they're "deterministic" in the strict sense, but what I mean is that they're very fragile and sensitive to small changes.)

Because the compiler tries to inline small-ish things, I've found it quite tricky to produce a #mwe, but there's an example of this I describe here.

--This works:
#eval (1 / 2 : ℝ).sign = 1

--This works:
#eval (if [1].length = 1 then 0 else (1 / 2) : ℝ) < 1

--This, which is just the logical and of the two above expressions, fails as its noncomputable:
#eval (if [1].length = 1 then 0 else (1 / 2) : ℝ) < 1 ∧ (1 / 2 : ℝ).sign = 1

[Alex Meiburg]

What's going on is that the expressions refers to noncomputable data (in this case, the division of two reals). So it is "structurally" noncomputable.

[Alex Meiburg]

But then the compiler recognizes that this data isn't actually used -- it gets referred to by some of the relevant instances, but then it's never actually used, so it doesn't need this value. So it compiles it and happily moves on, and it's computable.

[Alex Meiburg]

But the conditions on when it recognizes that it can drop the data seem kind of fragile. If it doesn't manage to do the right optimizations in the right order, then the compiled top-level function still takes the Real.instDiv'd data, which is noncomputable, and so it fails.

[Edward van de Meent]

could you complete your code snippet such that it works on live lean?

[Alex Meiburg]

Not easily, since it requires the ComputableReal package (and a lot of dependent code). This is what I mean by difficulty getting a good #mwe. :(

[Alex Meiburg]

I would like to find an easier way to trigger this behavior though, I'm trying

[Alex Meiburg]

It requires, at a minimum:

• A type A and a dependent type B : A -> Type
• A noncomputable function f : A
• A computable function g : (x : A) (y : B x) whose value depends only on data in y, not in x
• A computable function z : B f

Then when you try to evaluate g f z, sometimes the compiler will stop and not examine g's data dependency, and see that you depend on f which is noncomputable, and fail. And sometimes the compiler will recognize that g doesn't depend on f, and so it effectively compiles to something like g _ z, and can run it.

[Alex Meiburg]

The relevant compiler pass -- or maybe, one relevant pass -- is compiler.reduce_arity. But this happens before lots of other passes, which may make it more "obvious" that the data dependency isn't there. I think if this pass could get triggered again later it would fix "most" of the fragility.

[Alex Meiburg]

A couple of heuristics I've noticed:

• Adding the @[inline] attribute to g significantly improves the chances of it working. In the example above, it makes

#eval (if [1].length = 1 then 0 else (1 / 2) : ℝ) < 1 ∧ (1 / 2 : ℝ).sign = 1

work, for instance, whereas without the @[inline] attribute it doesn't. But then if I change the second term to (2 - 1 / 2 : ℝ).sign, that fails even with the inline attribute (and #eval (2 - 1 / 2 : ℝ).sign = 1 still works fine.)

• If you put all the "used" data arguments after all the "unused" data arguments, it seems much more likely to correctly drop them. In fact it might be strictly necessary. That is, supposed g has the signature g : (n : Nat) (x : A) (y : B x); and g uses the data in n and y. Then, in my experiments, this will never work and end up computable. But if you reorder the arguments to be g : (x : A) (n : Nat) (y : B x), then it will sometimes work.

[Kim Morrison]

Given that there is significant work on the new code generator at the moment, you may need to wait until it is deployed, as we're no longer modifying the old one barring critical bugs.

[Alex Meiburg]

I see, alright. Makes sense.
FWIW I was thinking about how I would ideally have this addressed. (I won't say "fixed", because it's not exactly a bug, just ... undesirable behavior.) I think anything based on compiler optimizations is ultimately kind of fragile.

So I was wondering, if somehow there could be something like a noData modifier, sort of similar to how outParam modifies a parameter but doesn't modify the type. And this would tell the compiler that, even though this is a data-carrying type being passed in, its value is not used anywhere and so it should make sure the type is dropped. And then there would be some kind of requirement, for this to pass, that the function only refers to that parameter in the context of Props, arguments to types, or other noData function parameters.

Of course, alternately it could become part of the spec that the compiler must identify all noData arguments (which it can do) and inline them; this is just sort of philosophically changing what is currently a compiler "optimization" into a compiler "spec".

I have no clue how much work such a feature or guarantee would be. :) Just thinking out loud

[Kyle Miller]

I remember looking into how to add something like noData to Lean 3 at some point. I'm not sure I can find the discussions from around 2022 about that.

Something else I remember is a Computable class, which would be a way to replace expressions with a computation: #general > computable class @ 💬 (it's not quite @[csimp] since a Computable instance can conditionally apply).

You might also look into discussions about the erased type from back then. I think one idea with "noData" was to make it so working with erased would be seamless somehow.

[Alex Meiburg]

Kim Morrison said:

Given that there is significant work on the new code generator at the moment, you may need to wait until it is deployed, as we're no longer modifying the old one barring critical bugs.

How can I try out the new generator? I tried set_option compiler.enableNew true but it didn't seem to have any effect. (It still says "compiling [old]".)

[Henrik Böving]

Enabling the new compiler enables it in addition to the old one as the new one is not yet at the point where it can produce a binary.

[Alex Meiburg]

Ah, ok.