[REVIEW]: Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation

whedon commented 3 years ago

Submitting author: @ 0x0f0f0f (Alessandro Cheli) Repository: https://github.com/0x0f0f0f/Metatheory.jl Version: v0.3.2 Editor: @dpsanders Reviewers: @mwillsey, @jpfairbanks, @philzook58 Archive: 10.5281/zenodo.4646136

:warning: JOSS reduced service mode :warning:

Due to the challenges of the COVID-19 pandemic, JOSS is currently operating in a "reduced service mode". You can read more about what that means in our blog post.

Status

Status badge code:

HTML: <a href="https://joss.theoj.org/papers/3266e8a08a75b9be2f194126a9c6f0e9"><img src="https://joss.theoj.org/papers/3266e8a08a75b9be2f194126a9c6f0e9/status.svg"></a>
Markdown: [![status](https://joss.theoj.org/papers/3266e8a08a75b9be2f194126a9c6f0e9/status.svg)](https://joss.theoj.org/papers/3266e8a08a75b9be2f194126a9c6f0e9)

Reviewers and authors:

Please avoid lengthy details of difficulties in the review thread. Instead, please create a new issue in the target repository and link to those issues (especially acceptance-blockers) by leaving comments in the review thread below. (For completists: if the target issue tracker is also on GitHub, linking the review thread in the issue or vice versa will create corresponding breadcrumb trails in the link target.)

Reviewer instructions & questions

@mwillsey & @jpfairbanks & @philzook58, please carry out your review in this issue by updating the checklist below. If you cannot edit the checklist please:

Make sure you're logged in to your GitHub account
Be sure to accept the invite at this URL: https://github.com/openjournals/joss-reviews/invitations

The reviewer guidelines are available here: https://joss.readthedocs.io/en/latest/reviewer_guidelines.html. Any questions/concerns please let @dpsanders know.

✨ Please start on your review when you are able, and be sure to complete your review in the next six weeks, at the very latest ✨

Review checklist for @mwillsey

Conflict of interest

[x] I confirm that I have read the JOSS conflict of interest (COI) policy and that: I have no COIs with reviewing this work or that any perceived COIs have been waived by JOSS for the purpose of this review.

Code of Conduct

[x] I confirm that I read and will adhere to the JOSS code of conduct.

General checks

[x] Repository: Is the source code for this software available at the repository url?
[x] License: Does the repository contain a plain-text LICENSE file with the contents of an OSI approved software license?
[x] Contribution and authorship: Has the submitting author (@ 0x0f0f0f) made major contributions to the software? Does the full list of paper authors seem appropriate and complete?
[x] Substantial scholarly effort: Does this submission meet the scope eligibility described in the JOSS guidelines

Functionality

[x] Installation: Does installation proceed as outlined in the documentation?
[x] Functionality: Have the functional claims of the software been confirmed?
[x] Performance: If there are any performance claims of the software, have they been confirmed? (If there are no claims, please check off this item.)

Documentation

[x] A statement of need: Does the paper have a section titled 'Statement of Need' that clearly states what problems the software is designed to solve and who the target audience is?
[x] Installation instructions: Is there a clearly-stated list of dependencies? Ideally these should be handled with an automated package management solution.
[x] Example usage: Do the authors include examples of how to use the software (ideally to solve real-world analysis problems).
[x] Functionality documentation: Is the core functionality of the software documented to a satisfactory level (e.g., API method documentation)?
[x] Automated tests: Are there automated tests or manual steps described so that the functionality of the software can be verified?
[x] Community guidelines: Are there clear guidelines for third parties wishing to 1) Contribute to the software 2) Report issues or problems with the software 3) Seek support

Software paper

[x] Summary: Has a clear description of the high-level functionality and purpose of the software for a diverse, non-specialist audience been provided?
[x] A statement of need: Do the authors clearly state what problems the software is designed to solve and who the target audience is?
[x] State of the field: Do the authors describe how this software compares to other commonly-used packages?
[x] Quality of writing: Is the paper well written (i.e., it does not require editing for structure, language, or writing quality)?
[x] References: Is the list of references complete, and is everything cited appropriately that should be cited (e.g., papers, datasets, software)? Do references in the text use the proper citation syntax?

Review checklist for @jpfairbanks

Conflict of interest

[x] I confirm that I have read the JOSS conflict of interest (COI) policy and that: I have no COIs with reviewing this work or that any perceived COIs have been waived by JOSS for the purpose of this review.

Code of Conduct

[x] I confirm that I read and will adhere to the JOSS code of conduct.

General checks

[x] Repository: Is the source code for this software available at the repository url?
[x] License: Does the repository contain a plain-text LICENSE file with the contents of an OSI approved software license?
[x] Contribution and authorship: Has the submitting author (@ 0x0f0f0f) made major contributions to the software? Does the full list of paper authors seem appropriate and complete?
[x] Substantial scholarly effort: Does this submission meet the scope eligibility described in the JOSS guidelines

Functionality

[x] Installation: Does installation proceed as outlined in the documentation?
[x] Functionality: Have the functional claims of the software been confirmed?
[x] Performance: If there are any performance claims of the software, have they been confirmed? (If there are no claims, please check off this item.)

Documentation

[x] A statement of need: Does the paper have a section titled 'Statement of Need' that clearly states what problems the software is designed to solve and who the target audience is?
[x] Installation instructions: Is there a clearly-stated list of dependencies? Ideally these should be handled with an automated package management solution.
[x] Example usage: Do the authors include examples of how to use the software (ideally to solve real-world analysis problems).
[x] Functionality documentation: Is the core functionality of the software documented to a satisfactory level (e.g., API method documentation)?
[x] Automated tests: Are there automated tests or manual steps described so that the functionality of the software can be verified?
[x] Community guidelines: Are there clear guidelines for third parties wishing to 1) Contribute to the software 2) Report issues or problems with the software 3) Seek support

Software paper

[x] Summary: Has a clear description of the high-level functionality and purpose of the software for a diverse, non-specialist audience been provided?
[x] A statement of need: Do the authors clearly state what problems the software is designed to solve and who the target audience is?
[x] State of the field: Do the authors describe how this software compares to other commonly-used packages?
[x] Quality of writing: Is the paper well written (i.e., it does not require editing for structure, language, or writing quality)?
[x] References: Is the list of references complete, and is everything cited appropriately that should be cited (e.g., papers, datasets, software)? Do references in the text use the proper citation syntax?

Review checklist for @philzook58

Conflict of interest

[x] I confirm that I have read the JOSS conflict of interest (COI) policy and that: I have no COIs with reviewing this work or that any perceived COIs have been waived by JOSS for the purpose of this review.

Code of Conduct

[x] I confirm that I read and will adhere to the JOSS code of conduct.

General checks

[x] Repository: Is the source code for this software available at the repository url?
[x] License: Does the repository contain a plain-text LICENSE file with the contents of an OSI approved software license?
[x] Contribution and authorship: Has the submitting author (@ 0x0f0f0f) made major contributions to the software? Does the full list of paper authors seem appropriate and complete?
[x] Substantial scholarly effort: Does this submission meet the scope eligibility described in the JOSS guidelines

Functionality

[x] Installation: Does installation proceed as outlined in the documentation?
[x] Functionality: Have the functional claims of the software been confirmed?
[x] Performance: If there are any performance claims of the software, have they been confirmed? (If there are no claims, please check off this item.)

Documentation

[x] A statement of need: Does the paper have a section titled 'Statement of Need' that clearly states what problems the software is designed to solve and who the target audience is?
[x] Installation instructions: Is there a clearly-stated list of dependencies? Ideally these should be handled with an automated package management solution.
[x] Example usage: Do the authors include examples of how to use the software (ideally to solve real-world analysis problems).
[x] Functionality documentation: Is the core functionality of the software documented to a satisfactory level (e.g., API method documentation)?
[x] Automated tests: Are there automated tests or manual steps described so that the functionality of the software can be verified?
[x] Community guidelines: Are there clear guidelines for third parties wishing to 1) Contribute to the software 2) Report issues or problems with the software 3) Seek support

Software paper

[x] Summary: Has a clear description of the high-level functionality and purpose of the software for a diverse, non-specialist audience been provided?
[x] A statement of need: Do the authors clearly state what problems the software is designed to solve and who the target audience is?
[x] State of the field: Do the authors describe how this software compares to other commonly-used packages?
[x] Quality of writing: Is the paper well written (i.e., it does not require editing for structure, language, or writing quality)?
[x] References: Is the list of references complete, and is everything cited appropriately that should be cited (e.g., papers, datasets, software)? Do references in the text use the proper citation syntax?

whedon commented 3 years ago

Hello human, I'm @whedon, a robot that can help you with some common editorial tasks. @mwillsey, @jpfairbanks, @philzook58 it looks like you're currently assigned to review this paper :tada:.

:warning: JOSS reduced service mode :warning:

Due to the challenges of the COVID-19 pandemic, JOSS is currently operating in a "reduced service mode". You can read more about what that means in our blog post.

:star: Important :star:

If you haven't already, you should seriously consider unsubscribing from GitHub notifications for this (https://github.com/openjournals/joss-reviews) repository. As a reviewer, you're probably currently watching this repository which means for GitHub's default behaviour you will receive notifications (emails) for all reviews 😿

To fix this do the following two things:

Set yourself as 'Not watching' https://github.com/openjournals/joss-reviews:

watching

You may also like to change your default settings for this watching repositories in your GitHub profile here: https://github.com/settings/notifications

notifications

For a list of things I can do to help you, just type:

@whedon commands

For example, to regenerate the paper pdf after making changes in the paper's md or bib files, type:

@whedon generate pdf

whedon commented 3 years ago

Software report (experimental):

github.com/AlDanial/cloc v 1.88  T=0.38 s (158.9 files/s, 10624.5 lines/s)
-------------------------------------------------------------------------------
Language                     files          blank        comment           code
-------------------------------------------------------------------------------
Julia                           44            574            303           2258
Markdown                         7            145              0            418
TeX                              2             21              0            164
YAML                             4              1             10             83
TOML                             2              4              0             29
SVG                              1              0              0              3
-------------------------------------------------------------------------------
SUM:                            60            745            313           2955
-------------------------------------------------------------------------------

Statistical information for the repository 'ba80bcb2091f1b9ae0a21830' was
gathered on 2021/03/02.
No commited files with the specified extensions were found.

whedon commented 3 years ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

whedon commented 3 years ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1145/3434304 is OK
- 10.1137/141000671 is OK
- 10.1145/2813885.2737959 is OK
- 10.1145/2737924.2737959 is OK
- 10.1145/322186.322198 is OK

MISSING DOIs

- None

INVALID DOIs

- None

0x0f0f0f commented 3 years ago

I will release 0.1.2 in the next days, can the version be updated here in the review?

dpsanders commented 3 years ago

@0x0f0f0f The version under review is not fixed until the end of the process, so there is nothing to do.

If you make changes as a result of the review process, please cross-reference them so the reviewers know what was changed.

0x0f0f0f commented 3 years ago

Thanks. I've tried to change the version number in the pre review but I did not have editor permissions to do so. Please keep in mind that a lot of things changed since v0.1.0 (many bugfixes) and the documentation in the repo is currently referring to the latest commit in the master branch of Metatheory.jl. The general concepts explained in the paper are unaltered.

dpsanders commented 3 years ago

There is no version number associated at the review stage. The reviewers will be looking at the master branch. That is why it is useful for you to link PRs here so that they can see what is being changed at each step.

Once the review is finished, that finalised version will be the one that is associated with the published paper.

dpsanders commented 3 years ago

@0x0f0f0f: I think it would be helpful to include a simple example of the application of the library in the paper.

dpsanders commented 3 years ago

@0x0f0f0f: The package will need proper narrative documentation, not just a quick README and the API reference. See https://documentation.divio.com/ for a discussion of the four different types of documentation required for a package.

jpfairbanks commented 3 years ago

The main figure is a reproduction from the EGG paper. There should be a novel figure highlighting the contributions of this library over and above the EGG library.
The primary benefit of using Metatheory is the algebraic nature of the specification of a simplification system. I would like that to be highlighted in the text.
Examples of specifying algebraic theories should be provided including the composition of theories by concatenating their rules.
Why is concatenating rules sufficient for composition in this setting? Is it because these are all single-sorted theories with universally quantified equations?

I agree with David that this package needs additional narrative documentation. Some content in the readme would be appropriate for that documentation.

0x0f0f0f commented 3 years ago

Points

The main figure is a reproduction from the EGG paper. There should be a novel figure highlighting the contributions of this library over and above the EGG library.

The primary benefit of using Metatheory is the algebraic nature of the specification of a simplification system. I would like that to be highlighted in the text.

Examples of specifying algebraic theories should be provided including the composition of theories by concatenating their rules.

Why is concatenating rules sufficient for composition in this setting? Is it because these are all single-sorted theories with universally quantified equations?

These 4 points should have been added in the paper in the latest commit.

0x0f0f0f commented 3 years ago

@whedon generate pdf

whedon commented 3 years ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

mwillsey commented 3 years ago

Low-level feedback

Line 26: "Theories can then be executed". Theories should be introduced first, this is an abrupt start.
"rust" should be "Rust" throughout

Overall the paper, software, and documentation (especially) looks good. As the egg author, I view "egg in Julia" as a sufficient contribution, given that Metatheory.jl capitalizes on then dynamic nature of Julia with, e.g. homoiconicity, runtime code generation, and so on.

My only overall comment is that (classical, directed) rewriting deserves a slightly longer treatment. Lots of work has gone into making rewriting fast and effective (e.g. completion, reduction orders, etc.), and using equality saturation will be slower in many use cases; this is simply a tradeoff.

0x0f0f0f commented 3 years ago

Thank you max! I really appreciate your comments and suggestions. I wanted to keep this paper short and introductory (focusing on the important contributions) to leave a more theoretical (and analytical) approach to a follow-up. I'd be really happy to read and write more about classical rewriting. Please send me an email if you have any paper to suggest!

mwillsey commented 3 years ago

@0x0f0f0f I really like this survey paper, it discusses most of the seminal works in this area: http://www.math.tau.ac.il/~nachumd/papers/taste-fixed.pdf

0x0f0f0f commented 3 years ago

@jpfairbanks how does the current documentation look? Anything you think I should add? Thank you Max! Very interesting paper. Well written and full of examples.

whedon commented 3 years ago

:wave: @jpfairbanks, please update us on how your review is going (this is an automated reminder).

whedon commented 3 years ago

:wave: @mwillsey, please update us on how your review is going (this is an automated reminder).

whedon commented 3 years ago

:wave: @philzook58, please update us on how your review is going (this is an automated reminder).

philzook58 commented 3 years ago

I have already found Metatheory.jl to be an extremely useful addition to the space with thoughtful insights in regards to usability, flexibility, and integration with the host language.

I have an intermixing of syntactic/grammar/style comments and actual content questions. I marked these comments as Style, since their suggestions are even more optional. I hope I am not overstepping my purview as a reviewer.

" a well-known paradigm similar to several LISP idioms such as Scheme." >> I wouldn't call Scheme a "Lisp idiom". I would call it a dialect. Suggestion : "a well-known paradigm found in LISP dialects such as Scheme". I've had discussions about what exactly homoiconicity is and I'm personally not sure. I'm unclear if it is a "paradigm" persay. But this is very subjective. Wikipedia seems to use the term "property" of a programming language which feels more appropriate to me. https://en.wikipedia.org/wiki/Homoiconicity
Style - "Julia programming language, designed to take advantage of >> its << powerful reflection capabilities to". Or possibly "Julia's"
"Intuitively, Metatheory.jl transforms Julia expressions in other Julia expressions at both compile and run time.". I think this makes sense and I see what you're going for, but Julia has a looser notion of compile and run time than most languages. I don't have a good suggestion.
Style - "Theories can then be executed throught two, highly composable, rewriting backends. The first one, is based just on standard rewriting built on top of the pattern matcher developed in [@matchcore]." I think you do not need any of these commas. There is also a typo "throught"
Style - "Such an approach suffers of the usual problems of rewriting systems. Even trivial equational rules such as commutativity may lead to non-terminating systems and thus need to be adjusted by some sort of structuring or rewriting order. This requires extensive user reasoning."
Style - "The other back-end for Metatheory.jl, the core of our contribution, is designed to not require the user to reason about rewriting order by relying on >> equality saturation on e-graphs, the state-of-the-art technique adapted from the egg rust library [@egg]. <<" adjustment of sentence.
Provided with a theory of equational rewriting rules, defined in pure Julia, e-graphs compactly represent many equivalent programs. >>> An egraph can be usefully used without equational pattern matching rewriting rules by merely inserting a fixed number of ground terms and equivalences into it. This is the usual mode in which they are used in quantifier free SMT queries. I feel this may be conflating two distinct aspects of the egraph technique as inseparable.
"Saturation iteratively executes an e-graph specific pattern matcher to efficiently compute (and analyze) all possible equivalent expressions contained in the e-graph congruence closure." >>> In my understanding, the definition of the egraph includes that it propagates all congruence closures at some point. The term saturation refers to saturation with respect to the rules, not with respect to the congruence closure.
Style - " beyond being easy to use and composable, " >> I erased "to be"
Style - I would suggest removing basically all colons ":" throughout the paper and just starting new sentences.
"such as costs of nodes or logical statements attached to terms." The logical statements part is unclear to me how it would work. I think this may be referring to discussions we've had so I want to bring this up. Is this an expected thing to be able to do or something already done?
"the most fitting expressions from an >> equivalence class represented in an e-graph." >> I don't think congruence closure is the appropriate term here.
Style - "Many applications of equality saturation have been recently published, tailoring advanced optimization tasks." This use of the word "tailoring" feels a little odd to me. Suggestion: "Many applications of equality saturation to advanced optimization tasks have been recently published."
Style - "In [@yang2021equality], authors used egg to superoptimize tensor signal flow graphs describing neural networks. However, Herbie requires interoperation and conversion of expressions between different languages and libraries." I would switch these sentences. Finish talking about Herbie.

mwillsey commented 3 years ago

@philzook58 these are great points, I agree with them. Aside from that, I consider my review complete.

philzook58 commented 3 years ago

I think I need a new invitation link as I can't edit my checkboxes and it appears to have expired. My apologies

I would also like to note for the sake of transparency that I have been in private discussion with the author on progress and usage of the library before even this article was submitted (it is mentioned in the acknowledgements of the paper also). We have no other prior connections besides that. I do not consider this to be a true conflict of interest.

0x0f0f0f commented 3 years ago

@philzook58 I don't think it is a true conflict of interest. AFAIK you've been constantly reviewing my implementation decisions even before I've submitted the paper.

dpsanders commented 3 years ago

@whedon add @philzook58 as reviewer

whedon commented 3 years ago

OK, @philzook58 is now a reviewer

dpsanders commented 3 years ago

@philzook58: I re-invited you; let me know if that didn't work. Thanks!

dpsanders commented 3 years ago

@jpfairbanks: Are you done with your review? Could you please fill in the remaining checkboxes at the top of this page? Thanks!

0x0f0f0f commented 3 years ago

Updated the paper with corrections from @philzook58 and @mwillsey

0x0f0f0f commented 3 years ago

@whedon generate pdf

whedon commented 3 years ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

jpfairbanks commented 3 years ago

I agree with @philzook58's suggestions. I think that the Metatheory library is rapidly evolving as we review this document, and I am not sure about the editorial standard for JOSS. Are libraries supposed to be mostly mature at the time of JOSS publication? Metatheory.jl is rapidly gaining new features, which might prompt a delay in JOSS publication, but I would leave that decision to the editors including @dpsanders. For example, since the original submission, Metatheory now defines an interface for term like types, which enables support for user supplied types to be used for terms. This is a large improvement over the original EGG implementation and should be called out in this article. I'm not sure what the editorial standard on this is. I am happy to see improvements in the library, but I think we will need a new JOSS submission in a month to document all the new features. Then again, if JOSS entries are living documents that always point to the latest version of the libraries docs, then this is less of a concern.

I also have been in contact with @0x0f0f0f about the integration of typed expressions with the goal of using Metatheory in my own work.

0x0f0f0f commented 3 years ago

I'm planning to write another full length paper in detail explaining all the features! This is an introductory paper to serve as canonical citation in the style of Flux.jl. In this paper I want to illustrate the core features and high level architecture of Metatheory.jl (egraphs and classical rewriting), which are unlikely to change.

0x0f0f0f commented 3 years ago

I made a single breaking change and I've updated the example in the paper. Will be present in next commit pushed.

0x0f0f0f commented 3 years ago

@whedon generate pdf

whedon commented 3 years ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

0x0f0f0f commented 3 years ago

Only change is that on the last line of example you do not need anymore to add the analysis explicitly but you can directly call extract!(egraph, cost_function). @philzook58 everything looking ok? Were you able to edit the whedon comment with the list after Daniel re-added you?

philzook58 commented 3 years ago

Everything looks good. Two more comments:

I've been added as a reviewer twice in the paper draft
I suspect the code is not quite displaying right in the draft for me. In particular, i think the \cup occurring in the theory combination is not rendering. Maybe I'm mistaken about the syntax. @0x0f0f0f should double check if there is anything else that looks off there

With these two points addressed, I think I consider my review complete

0x0f0f0f commented 3 years ago

Yep. The cup is not rendering. Will fix with union(...) asap!

0x0f0f0f commented 3 years ago

@whedon generate pdf

whedon commented 3 years ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

0x0f0f0f commented 3 years ago

Rendering looks good!! Thank you everybody for all the efforts in reviewing my first paper, for all the help, useful comments and all the long chats we had about this package!

dpsanders commented 3 years ago

👋 @philzook58, @mwillsey, @jpfairbanks: Many thanks for your comments. Could you please confirm here that you are happy with the paper and repository as is?

mwillsey commented 3 years ago

I am happy with it as is.

jpfairbanks commented 3 years ago

LGTM

philzook58 commented 3 years ago

Looks good to me. I am still listed as a reviewer twice in the sidebar of the paper though. I suspect the author has no control over this and it is something to do with whedon. Perhaps my old invitation needs to be cancelled?

0x0f0f0f commented 3 years ago

Should we open an issue in the whedon repo?

xuanxu commented 3 years ago

@whedon generate pdf

whedon commented 3 years ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

openjournals / joss-reviews