8000 TypeChecking.Pretty: add missing SPECIALIZE & some INLINE, eta-contract by andreasabel · Pull Request #7485 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

TypeChecking.Pretty: add missing SPECIALIZE & some INLINE, eta-contract #7485

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Sep 10, 2024
Merged

TypeChecking.Pretty: add missing SPECIALIZE & some INLINE, eta-contract #7485

merged 1 commit into from
Sep 10, 2024

Conversation

andreasabel
Copy link
Member
@andreasabel andreasabel commented Sep 10, 2024 •
edited
Loading

TypeChecking.Pretty: add missing SPECIALIZE & some INLINE, eta-contract

Also organize the code in a more tabular form, so it is harder to forget SPECIALIZE pragmas with new instances.

See also:

@andreasabel
TypeChecking.Pretty: add missing SPECIALIZE & some INLINE, eta-contract
c33ebaf 
Also organize the code in a more tabular form, so it is harder to
forget SPECIALIZE pragmas with new instances.
@andreasabel andreasabel changed the title Refactor Agda.Utils.Bag: use List1 to enforce non-emptiness of groups TypeChecking.Pretty: add missing SPECIALIZE & some INLINE, eta-contract Sep 10, 2024
@andreasabel andreasabel added performance Slow type checking, interaction, compilation or execution of Agda programs ux: printing Issues relating to how terms are printed for display refactor Changes to the code base which do not affect users (not in changelog) labels Sep 10, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 10, 2024
@andreasabel andreasabel merged commit c33ebaf into master Sep 10, 2024
28 checks passed
@AndrasKovacs
Copy link
Contributor
AndrasKovacs commented Sep 10, 2024 •
edited
Loading

I haven't used both INLINE and SPECIALIZE on the same symbol, and I'm not sure if it's useful, and probably harmful. Is there a source on what happens in this case? My current mental model says that the specialization mostly doesn't do anything. If the symbol is inlined, its specialization is never referenced in downstream modules, and becomes dead (but still compiled) code.

Btw, there's a separate SPECIALIZE INLINE pragma, which creates a specialization and the marks that to be inline, but that's not relevant for us here.

More about inlining and specialization:

  • Very small functions are OK to INLINE, but we need to ensure that their bodies are sufficiently specialized. E.g. if f is defined simply as an application of g, we can inline f but have to ensure that g is specialized at its own definition site.
  • Non-exported functions are OK to INLINE even when somewhat small, if the exported functions are properly specialized. But there aren't many explicit export lists in Agda and manually tracking exported symbol usages is rather tedious and fragile.
  • Cold code is OK to either SPECIALIZE or NOINLINE. So far I have used very few NOINLINE because it's not always clear which code is truly cold, and non-specialized code has a large overhead. IIRC I only put some NOINLINE in the serializer, on private functions. For pretty printing we could try to NOINLINE everything but we'd need to check if it slows down printing enough to be noticeable by users.

@andreasabel
Copy link
Member Author

Thanks for the comment!

So in this PR, all functions that are marked as INLINE lift a pure function into the monad, using pure, fmap, liftA2 etc.
And the SPECIALIZE pragmas instantiate the monad to TCM.
If a function is inlined, the SPECIALIZE would of course not apply, but it is also obsolete because the monad is "gone", except for the generic functions pure, fmap, liftA2.
I don't have a good mental model for inlining and specialization, but could this go wrong somewhere?

@AndrasKovacs
Copy link
Contributor

The short summary is that a symbol should be either INLINE or SPECIALIZE but not both, and if something is INLINE then we should make sure to have enough definition-site specialization for symbols occurring in the inlined code.

The ideal situation that we try to approximate: every symbol which is not inlined, has all of its specializations placed at the definition site.

@andreasabel andreasabel deleted the specialize-prettyTCM branch September 12, 2024 18:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@AndrasKovacs AndrasKovacs Awaiting requested review from AndrasKovacs

Assignees
No one assigned
Labels
performance Slow type checking, interaction, compilation or execution of Agda programs refactor Changes to the code base which do not affect users (not in changelog) ux: printing Issues relating to how terms are printed for display
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.
2 participants
@andreasabel @AndrasKovacs
0