SemIR fidelity when representing rewrite semantics #3833

chandlerc · 2024-03-29T05:01:53Z

The toolchain's Semantic IR should start off modeling the full,
complex, and rich library-based and generic extension point semantics of Carbon
without eliding any layers or rewrites for compile time efficiency. We shouldn't
front-load elision or optimization when implementing the designs.

Once we have a full-fidelity implementation, we should work to build an
efficient elision, short-circuit, or common case simplification into the design
itself sufficient to make the SemIR model efficient. Only if we cannot find a
reasonable approach for that should we diverge the SemIR model to optimize its
efficiency, and we should preserve full fidelity in an optional mode.

proposals/p3833.md

josh11b · 2024-03-30T00:03:32Z

proposals/p3833.md

+operators? This proposal suggests that _initially_, the implementation should
+aim to fully model the rewrite-based dispatch through interfaces in the prelude.
+That is, each use af `x + y` should turn into roughly equivalent SemIR as would
+be used to model the rewritten semantics of `x.(Core.AddWith(typeof(y)).Op)(y)`.


@zygoloid Is this syntax allowed?

Roughly, yes, I think so. I see a couple of issues here:

typeof doesn't exist (yet).

I would not expect us to need Core to be in scope -- I think we mean "the AddWith that lives in the prelude" rather than "the result of name lookup into the name Core" here. In Arithmetic expressions #1083, the rule was (supposed to be) that we look for an implementation of the interface from the standard library, not that we do a name lookup to find the name Core and look for these various names within whatever we find.

I think the syntax is now clarified as imagined syntax and not doing weird things with name lookup.

josh11b · 2024-03-30T00:04:54Z

proposals/p3833.md

+That is, each use af `x + y` should turn into roughly equivalent SemIR as would
+be used to model the rewritten semantics of `x.(Core.AddWith(typeof(y)).Op)(y)`.
+This in turn would dispatch to an exact-type implementation which would provide
+any implicit conversions, and so-on.


Could you explain the alternative(s) that is/are being decided against in terms of this example as well?

Maybe we could point out that this happens even when adding together (say) i32s.

Ah, that makes sense, I think done.

testing/file_test/autoupdate.cpp

proposals/p3833.md

chandlerc · 2024-04-01T21:43:59Z

(the brief diff issues should be fixed now, sorry for that)

zygoloid · 2024-04-24T21:07:54Z

proposals/p3833.md

+operators? This proposal suggests that _initially_, the implementation should
+aim to fully model the rewrite-based dispatch through interfaces in the prelude.
+That is, each use af `x + y` should turn into roughly equivalent SemIR as would
+be used to model the rewritten semantics of `x.(Core.AddWith(typeof(y)).Op)(y)`.


Roughly, yes, I think so. I see a couple of issues here:

typeof doesn't exist (yet).

I would not expect us to need Core to be in scope -- I think we mean "the AddWith that lives in the prelude" rather than "the result of name lookup into the name Core" here. In Arithmetic expressions #1083, the rule was (supposed to be) that we look for an implementation of the interface from the standard library, not that we do a name lookup to find the name Core and look for these various names within whatever we find.

zygoloid · 2024-04-24T21:10:53Z

proposals/p3833.md

+That is, each use af `x + y` should turn into roughly equivalent SemIR as would
+be used to model the rewritten semantics of `x.(Core.AddWith(typeof(y)).Op)(y)`.
+This in turn would dispatch to an exact-type implementation which would provide
+any implicit conversions, and so-on.


Maybe we could point out that this happens even when adding together (say) i32s.

zygoloid · 2024-04-24T21:11:52Z

proposals/p3833.md

+To be precise, the expectation is that the SemIR for `x + y` should as a
+consequence model all of:
+
+- Looking up the `Core.AddWith` interface.


Maybe:

Suggested change

- Looking up the `Core.AddWith` interface.

- Looking up the `AddWith` interface within the standard library package.

In particular, an unqualified lookup of the name Core isn't part of the design. (Performing a qualified lookup for the interface names wasn't my intent in #1083 either, but I don't think that's an important distinction, and I'd be OK with the rule being that you do perform that qualified lookup. But I'd be pretty strongly opposed to using an unqualified lookup for the name Core.)

Ah, now I understand the confusion when we've discussed this in the past.

Definitely not suggesting we should be doing arbitrary unqualified lookup. I agree that would be bad.

Really, this seems to suggest that there is a fundamental gap -- we should have some unambiguous way of looking up a name in the Core package without doing that name lookup. We have package.Name, we kind of need (package Core).Name but with some much better syntax. Is there a way I could frame this in pseudo syntax here?

I'd be fine with the syntax you suggested, eg:

Suggested change

- Looking up the `Core.AddWith` interface.

- Looking up the `(package Core).AddWith` interface, where `package Core` is pseudo-syntax that directly names the `Core` package.

I've added a slightly different imagined syntax and clarified the behavior and that these are all imagined syntaxes.

zygoloid · 2024-04-24T21:21:53Z

proposals/p3833.md

+shortcuts in the SemIR model for common cases with a option to disable them for
+testing and debugging.
+
+## Rationale


One thing I think would be worth discussing here is the impact of this proposal on cycles in the design: it'd be easy for us to accidentally define (for example) binding in terms of function calls and function calls in terms of bindings in such a way that we'd never bottom out. By requiring the toolchain to follow the design and not take shortcuts, at least under a flag, we can empirically test that our foundations actually work.

This means, for example, however we cut the loop of a function call desugaring into another function call needs to be determined in the design, not merely done in the toolchain at a convenient spot. So we shouldn't have the toolchain say "this is a direct call to a function; I'm not using the full function call machinery to dispatch it, because that would end up resulting in another function call", and instead we should have the design say that, if that's the intended approach. And if the intended approach is instead that we do use the full function call machinery, including impl lookup, but only once, then the design should say that instead.

I tried adding a section about this. Not sure I really explained it well though, so ssuggestions welcome. =]

chandlerc

Thanks for comments, most addressed, and one follow-up question inline!

chandlerc · 2024-05-02T18:11:39Z

proposals/p3833.md

+That is, each use af `x + y` should turn into roughly equivalent SemIR as would
+be used to model the rewritten semantics of `x.(Core.AddWith(typeof(y)).Op)(y)`.
+This in turn would dispatch to an exact-type implementation which would provide
+any implicit conversions, and so-on.


Ah, that makes sense, I think done.

chandlerc · 2024-05-02T18:14:03Z

proposals/p3833.md

+To be precise, the expectation is that the SemIR for `x + y` should as a
+consequence model all of:
+
+- Looking up the `Core.AddWith` interface.


Ah, now I understand the confusion when we've discussed this in the past.

Definitely not suggesting we should be doing arbitrary unqualified lookup. I agree that would be bad.

Really, this seems to suggest that there is a fundamental gap -- we should have some unambiguous way of looking up a name in the Core package without doing that name lookup. We have package.Name, we kind of need (package Core).Name but with some much better syntax. Is there a way I could frame this in pseudo syntax here?

chandlerc · 2024-05-02T18:24:33Z

proposals/p3833.md

+shortcuts in the SemIR model for common cases with a option to disable them for
+testing and debugging.
+
+## Rationale


I tried adding a section about this. Not sure I really explained it well though, so ssuggestions welcome. =]

The toolchain's [Semantic IR][semir] should start off modeling the full, complex, and rich library-based and generic extension point semantics of Carbon without eliding any layers or rewrites for compile time efficiency. We shouldn't front-load elision or optimization when implementing the designs. Once we have a full-fidelity implementation, we should work to build an efficient elision, short-circuit, or common case simplification into the design itself sufficient to make the SemIR model efficient. Only if we cannot find a reasonable approach for that should we diverge the SemIR model to optimize its efficiency, and we should preserve full fidelity in an optional mode. [semir]: https://docs.google.com/document/d/1RRYMm42osyqhI2LyjrjockYCutQ5dOf8Abu50kTrkX0/edit?resourcekey=0-kHyqOESbOHmzZphUbtLrTw#heading=h.503m6lfcnmui

Co-authored-by: josh11b <[email protected]>

chandlerc · 2024-05-09T02:05:01Z

(Fixed weird mis-merge, sorry about that)

chandlerc

PTAL, I think the comments are addressed now?

chandlerc added proposal A proposal proposal draft Proposal in draft, not ready for review labels Mar 29, 2024

chandlerc force-pushed the semir-rewrite-fidelity branch 2 times, most recently from 94a605c to 96f3fcb Compare March 29, 2024 07:27

chandlerc marked this pull request as ready for review March 29, 2024 07:28

github-actions bot added proposal rfc Proposal with request-for-comment sent out and removed proposal draft Proposal in draft, not ready for review labels Mar 29, 2024

github-actions bot requested a review from KateGregory March 29, 2024 07:28

jonmeow reviewed Mar 29, 2024

View reviewed changes

proposals/p3833.md Show resolved Hide resolved

josh11b reviewed Mar 29, 2024

View reviewed changes

proposals/p3833.md Show resolved Hide resolved

chandlerc force-pushed the semir-rewrite-fidelity branch from 96f3fcb to ac5ac31 Compare March 29, 2024 22:45

josh11b reviewed Mar 30, 2024

View reviewed changes

jonmeow reviewed Apr 1, 2024

View reviewed changes

testing/file_test/autoupdate.cpp Outdated Show resolved Hide resolved

proposals/p3833.md Show resolved Hide resolved

chandlerc force-pushed the semir-rewrite-fidelity branch from 51e359d to 3de52f7 Compare April 1, 2024 21:42

chandlerc force-pushed the semir-rewrite-fidelity branch 2 times, most recently from e588bd6 to 3809e49 Compare April 7, 2024 20:21

jonmeow mentioned this pull request Apr 24, 2024

Remove the builtin IR, and instead define builtin types locally. #3910

Merged

zygoloid reviewed Apr 24, 2024

View reviewed changes

chandlerc commented May 2, 2024

View reviewed changes

chandlerc and others added 6 commits May 8, 2024 19:02

add example

40c2557

fixes

43b0eb9

Update proposals/p3833.md

0bee0f8

Co-authored-by: josh11b <[email protected]>

further detail in example

977f8ac

Improve based on review.

c5538de

chandlerc force-pushed the semir-rewrite-fidelity branch from 8262d9c to c5538de Compare May 9, 2024 02:04

zygoloid mentioned this pull request May 11, 2024

Binding operators #3720

Open

chandlerc requested a review from zygoloid May 14, 2024 01:47

chandlerc added 2 commits May 16, 2024 19:21

Switch to more explicit imagined syntax and correct name lookup model.

1a5d22d

Tweak the wording

02283aa

chandlerc commented May 17, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SemIR fidelity when representing rewrite semantics #3833

SemIR fidelity when representing rewrite semantics #3833

chandlerc commented Mar 29, 2024 •

edited

josh11b Mar 30, 2024

zygoloid Apr 24, 2024 •

edited

chandlerc May 17, 2024

josh11b Mar 30, 2024

zygoloid Apr 24, 2024

chandlerc May 2, 2024

chandlerc commented Apr 1, 2024

zygoloid Apr 24, 2024 •

edited

zygoloid Apr 24, 2024

zygoloid Apr 24, 2024

chandlerc May 2, 2024

zygoloid May 3, 2024

chandlerc May 17, 2024

zygoloid Apr 24, 2024

chandlerc May 2, 2024

chandlerc left a comment

chandlerc May 2, 2024

chandlerc May 2, 2024

chandlerc May 2, 2024

chandlerc commented May 9, 2024

chandlerc left a comment

	- Looking up the `Core.AddWith` interface.
	- Looking up the `AddWith` interface within the standard library package.

	- Looking up the `Core.AddWith` interface.
	- Looking up the `(package Core).AddWith` interface, where `package Core` is pseudo-syntax that directly names the `Core` package.

SemIR fidelity when representing rewrite semantics #3833

Are you sure you want to change the base?

SemIR fidelity when representing rewrite semantics #3833

Conversation

chandlerc commented Mar 29, 2024 • edited

Choose a reason for hiding this comment

zygoloid Apr 24, 2024 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chandlerc commented Apr 1, 2024

zygoloid Apr 24, 2024 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chandlerc left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chandlerc commented May 9, 2024

chandlerc left a comment

Choose a reason for hiding this comment

chandlerc commented Mar 29, 2024 •

edited

zygoloid Apr 24, 2024 •

edited

zygoloid Apr 24, 2024 •

edited