|
From: | Daniel Mendler |
Subject: | bug#47992: [External] : bug#47992: 27; 28; Phase out use of `equal` in `add-hook`, `remove-hook` |
Date: | Sun, 25 Apr 2021 01:38:17 +0200 |
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
[Prev in Thread] | Current Thread | [Next in Thread] |