Eliminating spurious errors related to "dependent computations"

[msprotz]

Based on a long discussion with @denismerigoux. Here's a Catala example:

definition bar under condition paragraph_a_applies consequence equals $0
definition foo under condition paragraph_a_applies consequence equals bar
definition foo under condition paragraph_b_applies consequence equals $1

The only output that I care about is the value of foo. However, if I call this scope with paragraph_b_applies = true, then I get a fatal error because the definition of bar is empty, even though I do not need bar for computing my output foo.

The reason is that this gets translated to:

let bar = < | paragraph_a_applies: $0 > in
let foo = < < | paragraph_a_applies: bar >; < | paragraph_b_applies: $1 > | > in
bar, foo

and the evaluation of bar is unconditional

If, however, I were able to annotate foo with an attribute that says "this is an output of my top-level scope", then the program above would contain more opportunities for rewriting; for instance, a simple syntactic analysis could uncover that bar is only needed in the first computation, and the program could be rewritten as such:

let foo = < < | paragraph_a_applies: let bar = < | paragraph_a_applies: $0 > in bar >; < | paragraph_b_applies: $1 > | > in
foo

This would provide a superior user experience; rather than providing an un-needed default case for bar when paragraph_b_applies (which legally does not make sense), we ensure instead that the compiler "figures out" that bar is needed only for the computation of foo under condition paragraph_a_applies and rewrite the default calculus term accordingly.

Questions to work out:

• how to express this rewriting formally
• can we always guarantee that this optimization triggers and therefore eliminates all spurious empty errors?
• what is the corresponding standard compiler transformation, and what can we learn from existing implementations?

[AltGr]

I only now stumbled upon this old issue, but similar questions keep arising regularly.

At the risk of stating the obvious, inlining or lazy evaluation come to mind, although in a restricted setting. But the actual implementation triggered another idea: what if we were to remove the ErrorOnEmpty guarding all (non-output) variables, and move them to the positions where the variables are being used ? Semantics wise, that will probably be more difficult to express (additional wrapping, or another kind of exceptions ?) but it might be worth exploring.