Should we name all the pattern-matching lambdas?

[gallais]

Remember that two similar-looking pattern-matching lambdas are not judgmentally equal because each is elaborated to a different definition with a different internal name.

One possible workaround is to introduce a named where-clause that allows us to pick a name for this anonymous lambda. If we adopt a clear naming scheme for these, we could have very predictable names for users.

Using Codata.Thunk's cofix as an example, we could write:

  cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
-  cofix f = f (λ where .force → cofix f)
+  cofix f = f aux module Cofix where
+    aux = λ where .force → cofix f

And we would then be able to mention the anonymous lambda by its name Cofix.aux.

With this scheme, we could write some of the expressions that show up in the bisimilarity reasoning in e.g. Codata.Stream.Properties that have to be left blank at the moment.

Pros: we finally have names for these Cons: we pollute the name space with a lot of module names

[MatthewDaggitt]

I vaguely remember it being said in the Agda issue discussing this that the fact that identical lambdas had different names was considered a bug?

Unless there's places where the lambda's can't be inferred and that's causing problems, I'd probably err on the side of leaving as is and waiting for a fix upstream. As you say, it adds a lot of pollution to the namespace, for a comparatively small(?) increase in readability...

[jespercockx]

I don't think it is considered a bug. Having structural equality of pattern lambdas would certainly be possible in theory but it would require a lot of work to implement and it would come with a certain performance penalty, as comparing two definitions is definitely more expensive than merely comparing two names. So I don't expect there will be an upstream fix anytime soon.

[JacquesCarette]

My reaction, even after a few days of thinking about it, is still negative.

If a sub-function is really needed elsewhere, it should be given a real name. [For cofix, you'd use a mutual block].

[gallais]

The problem with the mutual blocks is that you need to specify the type of the auxiliary function. At this point you have to declare all coinductive functions twice.

[JacquesCarette]

True... but perhaps that's still a good thing? In the sense that if you wish to expose certain 'innards', then there is a cost, of an extra type signature. Perhaps that should cause you to pause and wonder if you truly want to expose that much.

[MatthewDaggitt]

@gallais I'm more than happy to defer to your and @JacquesCarette's decision on this as I've never really used the Codata part of the library...