noncomputable/irrelevant fields

Stream: lean4

[Reid Barton]

Has there been consideration of a feature like

structure Foo where
  x : Int
  noncomputable y : Int

meaning

• Foo.y becomes noncomputable
• Foo.mk x y is computable as soon as x is
• A Foo does not store the value y at runtime

It's possible to emulate this with a Erased type, but at the cost of some definitional equalities.

[Mario Carneiro]

(I just noticed that erased.out isn't marked noncomputable in the doc gen. We should probably do something about that)

[Mario Carneiro]

What is the type of Foo.mk? Is it possible to define a function with the same computability behavior as the proposed Foo.mk constructor?

[Mario Carneiro]

It might be easier to actually have an Erased type constructor. It can't really be a type alias because then the VM could confuse A and Erased A if a lean function abuses the defeq

[Reid Barton]

Right, I don't know how Lean determines which parts of the program are runtime relevant, but if it's based entirely on type information, then a special structure Erased A where val : A which gets erased would already be helpful

[Mario Carneiro]

The key function for this seems to be https://github.com/leanprover/lean4/blob/master/src/library/compiler/util.cpp#L401-L414 . I can't find any function along these lines in lean, although there is Arg.irrelevant and IRType.irrelevant for tracking it