From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Daniel Mendler Newsgroups: gmane.emacs.bugs 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 Message-ID: <3895c1c1-3387-a6f6-423b-a786bad24a5b@daniel-mendler.de> References: <090f8bd5-368c-5684-85e1-65420049d47a@daniel-mendler.de> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="12774"; mail-complaints-to="usenet@ciao.gmane.io" Cc: "47992@debbugs.gnu.org" <47992@debbugs.gnu.org>, "jakanakaevangeli@chiru.no" To: Stefan Monnier Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Sun Apr 25 01:39:19 2021 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1laRrq-00039y-HF for geb-bug-gnu-emacs@m.gmane-mx.org; Sun, 25 Apr 2021 01:39:18 +0200 Original-Received: from localhost ([::1]:57292 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1laRrp-0006SD-82 for geb-bug-gnu-emacs@m.gmane-mx.org; Sat, 24 Apr 2021 19:39:17 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:37366) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1laRra-0006S3-KL for bug-gnu-emacs@gnu.org; Sat, 24 Apr 2021 19:39:03 -0400 Original-Received: from debbugs.gnu.org ([209.51.188.43]:58391) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1laRra-0003mT-BE for bug-gnu-emacs@gnu.org; Sat, 24 Apr 2021 19:39:02 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1laRra-0005Ip-99 for bug-gnu-emacs@gnu.org; Sat, 24 Apr 2021 19:39:02 -0400 X-Loop: help-debbugs@gnu.org Resent-From: Daniel Mendler Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Sat, 24 Apr 2021 23:39:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 47992 X-GNU-PR-Package: emacs Original-Received: via spool by 47992-submit@debbugs.gnu.org id=B47992.161930750820342 (code B ref 47992); Sat, 24 Apr 2021 23:39:02 +0000 Original-Received: (at 47992) by debbugs.gnu.org; 24 Apr 2021 23:38:28 +0000 Original-Received: from localhost ([127.0.0.1]:41704 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1laRr2-0005I2-Cr for submit@debbugs.gnu.org; Sat, 24 Apr 2021 19:38:28 -0400 Original-Received: from server.qxqx.de ([178.63.65.180]:52053 helo=mail.qxqx.de) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1laRqz-0005Hp-UJ for 47992@debbugs.gnu.org; Sat, 24 Apr 2021 19:38:26 -0400 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=qxqx.de; s=mail1392553390; h=Content-Transfer-Encoding:Content-Type:In-Reply-To: MIME-Version:Date:Message-ID:From:References:Cc:To:Subject:Sender:Reply-To: Content-ID:Content-Description:Resent-Date:Resent-From:Resent-Sender: Resent-To:Resent-Cc:Resent-Message-ID:List-Id:List-Help:List-Unsubscribe: List-Subscribe:List-Post:List-Owner:List-Archive; bh=gbZ8/fnX88CtP/hhVy+1Pvh56A5iQhVq3rSBiBJ17eA=; b=e9gWxesGrkQjOrhg3rCBWTOack a2WESzBTCVkVrMfbOhUdF1vdG7C8muyHzTsmF0Ww9Bjxe1SoSUU+jI99ywOmVsGWbPWCAisoqGxDz VEDlmltpOFVxa+xBQ3lz1owc7rD8JL9z6L+POXBCPT+/VivDckhbaAce3NAHfZNe0iPk=; In-Reply-To: Content-Language: en-US X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: "bug-gnu-emacs" Xref: news.gmane.io gmane.emacs.bugs:204833 Archived-At: 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