noncomputability across function calls

Stream: lean4

[James Gallicchio]

I am a bit curious how the computability checker works across function call boundaries. Which arguments to a function does the computability checker ensure are computable? Is there a way to mark that an argument should not be used for computation in the body?

[James Gallicchio]

as an example, I have a definition

def VEncCNF (L) [LitVar L ν] [Fintype ν] (α : Type u) (P : PropFun ν) :=
  { e : EncCNF L α // e.encodesProp P }

where EncCNF is essentially just a state monad. The Fintype argument and the P argument should both always be treated noncomputably. For example I have a function for constructing these values:

def for_all (arr : Array α) {P : α → PropFun ν} (f : (a : α) → VEncCNF L Unit (P a))
  : VEncCNF L Unit (.all (arr.toList.map P)) :=

and Lean currently seems to be marking that P is used for computation (i.e. I call for_all elsewhere with a noncomputable P and it complains), when in reality it should not be used anywhere.

[James Gallicchio]

using mathlib Erased seems like way more effort than it is worth. In the for_all example I would need to use the monad instance on erased, which substantially increases my proof burden

[James Gallicchio]

I somewhat successfully used Erased to make an ErasedFintype typeclass to prevent lean from computing that Fintype argument at callsites, but now that the P argument is demanding the same treatment I am getting worn down

[Eric Wieser]

I think in Lean 3, using @[inline] allowed Lean to unfold definitions to see that their arguments were not used for computation

[James Gallicchio]

I thought there was a discussion a while ago about how computability shouldn't rely on these optimization annotations, but I don't know whether anything came of it.

[James Gallicchio]

(also, I have had to mark various definitions noinline and nospecialize at places to prevent Lean's optimizations from taking 30 seconds during compilation for a single def...)

[James Gallicchio]

cc @Mario Carneiro

[James Gallicchio]

It seems here the suggestion was macro_inline, I'm not sure that is a viable hack in this case

[Mario Carneiro]

sorry, the best we have currently is Erased

[Mario Carneiro]

this is a known compiler issue but there isn't work on it these days

[Mario Carneiro]

using inline should help, assuming you can define the functions in terms of functions which do not take the erased values as arguments

[James Gallicchio]

I could also put PropFun in Prop, since it is never intended for computation anyways...

[Mario Carneiro]

what is it?

[Mario Carneiro]

certainly that will help

[James Gallicchio]

It is the inductive propositional formulas quotiented by equivalence

[Mario Carneiro]

...

[Mario Carneiro]

that's explicitly computational

[James Gallicchio]

It's definitely computable, yes, it just shouldn't be used in computation. The reason I am marking things noncomputable here is for performance, because Lean is insisting on building very large lean objects that are never used in the computations.

[Mario Carneiro]

have you looked at the IR? I can't see how lean could omit this if it wanted to

[James Gallicchio]

Because P is an argument to these functions and Lean doesn't know that it should be erasing P?

[James Gallicchio]

I haven't looked at the IR, but I am guessing it is what we expect

[Mario Carneiro]

to get erasure, you will have best results if all your erased indices are types and proofs

[Mario Carneiro]

And that includes the index of VEncCNF

[Mario Carneiro]

The Fintype issue is pretty easy to solve, just use Finite instead

[James Gallicchio]

got it :)

[Mario Carneiro]

Could PropFun ν be defined as just e.g. (ν -> Prop) -> Prop? I realize that's not necessarily finitely supported but encodesProp should imply that it is

[James Gallicchio]

Hm, that’s definitely an idea. Since I have the Fintype argument there anyways. Will try it out