bug#47992: [External] : bug#47992: 27; 28; Phase out use of `equal` in `add-hook`, `remove-hook`

[Daniel Mendler <mail@daniel-mendler.de>]

On 4/25/21 1:04 AM, Stefan Monnier wrote:
>> The structural equality does not even perform alpha conversion.
> 
> It partly does actually, by accident, when the code is byte-compiled,
> but only for the variables internal to the function and not for the
> formal arguments (because they "escape" into the docstring).
> 
> Hopefully this will be "broken" at some point, when we add enough debug
> info to bytecode to be able to find the value of (and set) local
> variables by name.

Hopefully.

> Equality on functions is fundamentally undecidable and it's nigh-on
> impossible to provide a sane and well-defined "approximation" of it
> either (at least not without significantly restricting the set of
> optimizations that the compiler can be allowed to perform).

Yes, for structural equality of functions there seem to be no other sane 
choices than the equality of the representation, maybe with additional 
alpha conversion. It would be okay to use object identity.

> The upside is that this fundamental problem was the motivation for the
> development of type classes in Haskell which are a great feature
> (nowadays used in most proof assistants and in several other programming
> languages such as Scala and Rust).

Indeed. The Eq type class simply forbids equality for functions. But in 
proof assistants the equality problem strikes again, when checking if 
two functions are definitionally equal. And then there is this whole 
equality rabbit hole in type theory.

Daniel