Alpha-equivalence for recursive let-bindings
Simon Peyton Jones
simonpj at microsoft.com
Mon Nov 8 12:02:39 UTC 2021
Huh! Dead right!
Would you like to:
* Open a ticket (you can use the text from this email)
* Submit a MR?
On the MR,
* Add a Note that again gives your killer example; and mention why we don't need the check for NonRec
* Worth also pointing out that letrec { x = e1; y = e2 } in b is NOT considered equal to letrec { y = e1; x = e1 } in b. Nor are let x=e1 in let y = e2 in b considered equal to let y = e1 in let x = e1 in b. This is fine; but worth pointing out.
Thanks for pointing this out!
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj at microsoft.com<mailto:simonpj at microsoft.com> will cease to work. Use simon.peytonjones at gmail.com<mailto:simon.peytonjones at gmail.com> instead. (For now, it just forwards to simonpj at microsoft.com.)
From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Christiaan Baaij
Sent: 07 November 2021 21:08
To: ghc-devs <ghc-devs at haskell.org>
Subject: Alpha-equivalence for recursive let-bindings
Hi list,
I was looking at the `Eq (DeBruijn CoreExpr)` instance and I noticed that the types of recursive let-bindings aren't checked for alpha-equivalence:
https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Core/Map/Expr.hs#L166-174<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fblob%2Fmaster%2Fcompiler%2FGHC%2FCore%2FMap%2FExpr.hs%23L166-174&data=04%7C01%7Csimonpj%40microsoft.com%7C4e4f1afdc4d64d66f2ef08d9a232bca8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719161836942634%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=6TGl3MHDSGLyUFjfMwce13K%2FVprCl7YRMQnRGrJj%2BAI%3D&reserved=0>
go (Let (Rec ps1) e1) (Let (Rec ps2) e2)
= equalLength ps1 ps2
&& D env1' rs1 == D env2' rs2
&& D env1' e1 == D env2' e2
where
(bs1,rs1) = unzip ps1
(bs2,rs2) = unzip ps2
env1' = extendCMEs env1 bs1
env2' = extendCMEs env2 bs2
But doesn't that mean that:
let (x :: Int) = x in x
and
let (y :: Bool) = y in y
are considered alpha-equivalent?
If that is the case, then I think that's wrong. Agree?
I understand that you don't have to check types for non-recursive let-bindings: when the RHSs match, the types must be the same.
-- Christiaan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211108/fe906a14/attachment.html>
More information about the ghc-devs
mailing list