Skip to content
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.

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

Performance Of Reasoning Combinators #622

Open
oisdk opened this Issue Feb 16, 2019 · 3 comments

Comments

Projects
None yet
2 participants
@oisdk
Copy link
Contributor

oisdk commented Feb 16, 2019

When I was trying to fix some performance problems which seemed to involve the equational reasoning combinators, I came across this message on the mailing list. It basically suggests replacing the following definition:

_∼⟨_⟩_ :  x {y z}  x ∼ y  y IsRelatedTo z  x IsRelatedTo z
_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

With this:

step-∼ :  x {y z}  y IsRelatedTo z  x ∼ y  x IsRelatedTo z
step-∼ _ (relTo y∼z) x∼y = relTo (trans x∼y y∼z)

syntax step-∼ x y∼z x∼y = x ∼⟨ x∼y ⟩ y∼z

This changes the order of typechecking, meaning that Agda will look first at y IsRelatedTo z to find the definition of y, rather than looking at x ∼ y. This should yield a pretty big speedup, because y IsRelatedTo z will have y explicitly stated on the next line (the message mentions a five-fold speedup).

I've found some other benefits, also. The improved type inference means that I can integrate an automated solver into the equational reasoning:

lemma :  x y  x + y * 1 + 32 + 1 + y + x
lemma x y = begin
  x + y * 1 + 3 ≈⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩
  y * 1 + x + 3 ≈⟨ solveOver (x ∷ y ∷ []) Int.ring ⟩
  3 + y + x     ≡⟨⟩
  2 + 1 + y + x ∎

I can't get this to work with the current combinators.

How disruptive a change would the flipped combinators be? Would it be worth a pull request?

@gallais

This comment has been minimized.

Copy link
Member

gallais commented Feb 16, 2019

Would it be worth a pull request?

I think so. The solver integration is a really nice selling point!

@oisdk

This comment has been minimized.

Copy link
Contributor Author

oisdk commented Feb 16, 2019

Would a new module (Relation.Binary.Reasoning.Flipped or something) be the way to go? Or should I replace the current definitions with the syntax above?

@gallais

This comment has been minimized.

Copy link
Member

gallais commented Feb 16, 2019

I'd say replace them: if I understand nad & you correctly they're basically the same,
but better. Given that we are using the reasoning kit in the stdlib, that will also
give us a nice test case to see whether it breaks existing use cases anywhere.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.