Cannot find default value for field

Stream: lean4

[Gabriel Ebner]

As discussed in https://github.com/leanprover/lean4/issues/813, I've tried to make Function.const and Function.comp semireducible. https://github.com/leanprover/lean4/compare/master...gebner:compconstsemired?expand=1

However I ran into a weird problem:

Init/Control/Lawful.lean:169:63: error: field 'comp_map' is missing
Init/Control/Lawful.lean:215:63: error: field 'comp_map' is missing
Init/Control/Lawful.lean:297:62: error: field 'comp_map' is missing

But I didn't change anything about comp_map (except the reducibility of a function in its type), it's still got the same default value as before. The default value is not an auto param either.

Any ideas what could be going wrong here? I can't find anything relevant in the Meta.isDefEq and Elab. It even mentions the default value: [Elab.struct] elabStruct comp_map := <default>, ...

[Leonardo de Moura]

@Gabriel Ebner I pushed a fix for 813. I also had problems with Lawful.lean, but I think it was just broken proofs for me.

[Tomas Skrivan]

I'm using comp and similarly defined curry, uncurry all over the place when stating typeclass instance. Removing reducible breaks my code now.

For example now there is a difference between:

instance : IsLinear (λ x : X×X => x.1+x.2) := sorry

and

instance : IsLinear (uncurry (HAdd.hAdd : X → X → X)) := sorry

Not a real issue, but now I have to prefer one over the other. Not sure which one as sometimes it is easier to write one over the other.

[Mario Carneiro]

If you are relying on reducibility of comp, then you should probably be using the lambda form, with these functions already unfolded

[Mac]

@Mario Carneiro In my opinion, that greatly reduces the readability of the code. Functions like comp, curry, uncurry are much prettier than their lambda counterparts and much more natural for those coming from a functional programming language background (e.g., Haskell).

[Mario Carneiro]

Yes, I know. Pointfree style is not as well supported in lean as in haskell, but it's not clear how much of that is just a side effect of the fact that haskellers aren't trying to prove facts about their code

[Mario Carneiro]

For something like Tomas Skrivan 's IsLinear typeclass, which consists of a bunch of carefully stated lemmas to prove a nontrivial property about a class of functions using type class inference, I think it is to be expected that the lemma statements have certain constraints on them which may not correspond to "mathematical naturality" so to speak. For general lemmas you can usually afford to be more lax

[Mac]

@Mario Carneiro I feel like this change is unnecessarily bias in a particular direction whereas there are vey good arguments for the opposite approach. I think it would be most helpful if there was both a reducible (or macro) and semi-reducible versions of these functions, since there are times both are useful.

[Mario Carneiro]

a macro that eliminates itself would be ideal, but it might be difficult to get it to do the right thing in all sorts of higher order scenarios (which seems to be the main reason to use it)

[Mac]

@Mario Carneiro what problems do you foresee? My naive implementation would just be:

macro (priority := high) f:term:91 " ∘ " g:term:90 : term =>
  `(fun x => $f ($g x))

def comp (f : β → δ) (g : α → β) := f ∘ g

This way both sides can be made happy. But I imagine I may be missing something here.

[Mario Carneiro]

If you do something like comp comp comp you will get a bunch of beta redexes

[Mac]

@Mario Carneiro what do you think of my suggestion?

[Gabriel Ebner]

I think the macro is the more Lean-y choice than an abbreviation (e.g. $ is also a macro and not a definition). Note that we already some macros for function composition, you can write (f $ g $ h ·) instead of f ∘ g ∘ h.

[Gabriel Ebner]

much more natural for those coming from a functional programming language background (e.g., Haskell).

Whether comp etc. is reducible or not basically only makes a difference when used in type-class arguments or when writing proofs (using simp). I don't know the current state of dependent haskell, but for a long time you couldn't write type classes like IsLinear at all in haskell. So I don't think you can bring this as an argument for what haskell users would expect. (And even then I don't know if ghc reduces ∘ during type class search).

[Mac]

@Gabriel Ebner fyi, my reference to /Haskell was simply to highlight that there is a subset of programmers who prefer the operator for function composition to its lambda representation, which, in turn, was just a piece of evidence as to why losing the ability to do so in typeclass signatures could be viewed as a feature regression.