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

Add simplifications that take advantage of associativity #274

Closed
wants to merge 2 commits into from

Conversation

@Gabriel439
Copy link
Contributor

Gabriel439 commented Nov 12, 2018

Fixes https://github.com/dhall-lang/dhall-haskell/issues/652

This change updates the language to exploit associativity to expose more
simplifications.

The test suite contains a non-trivial example of how this would work:

λ(x : Bool) → ((False == x) == True) == x

... which should simplify to:

λ(x : Bool) → False

I chose this test case because my original attempt to standardize this
did not handle this case correctly because it didn't normalize
(False == x) == True to (False == x) before attempting to detect an
opportunity to simplify (False == x) == x via associativity.

The second test case exercises reordering a pathological set of parentheses,
which would not reduce without this change:

λ(x : Natural) → 1 + ((2 + (x + 4)) + 5)

... but after this change would simplify to:

λ(x : Natural) → 3 + x + 9
Gabriel439 added 2 commits Nov 12, 2018
Fixes https://github.com/dhall-lang/dhall-haskell/issues/652

This change updates the language to exploit associativity to expose more
simplifications.

The test suite contains a non-trivial example of how this would work:

    λ(x : Bool) → ((False == x) == True) == x

... which should simplify to:

    λ(x : Bool) → False

I chose this test case because my original attempt to standardize this
did not handle this case correctly because it didn't normalize
`(False == x) == True` to `(False == x)` before attempting to detect an
opportunity to simplify `(False == x) == x` via associativity.

The second test case exercises reordering a pathological set of parentheses,
which would not reduce without this change:

    λ(x : Natural) → 1 + ((2 + (x + 4)) + 5)

... but after this change would simplify to:

    λ(x : Natural) → 3 + x + 9
Copy link
Collaborator

FintanH left a comment

Amazing, thank you!

@f-f

This comment has been minimized.

Copy link
Member

f-f commented Nov 13, 2018

@Gabriel439 could we wait until the PR for the Haskell implementation is up before merging this?
I'm a little bit worried that this is going to be hard to keep up with in other languages, so I'd like to take a look at the implementation first

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 13, 2018

@f-f: Yes, I plan to complete the Haskell implementation first and then give a week to review after that is ready

@MonoidMusician

This comment has been minimized.

Copy link
Collaborator

MonoidMusician commented Nov 14, 2018

I was wondering if we actually want to choose a strong normal form for the well-behaved (commutative, associative) operators ... something like a specific polynormial(-esque) form for operations on Natural, and maybe something for Booleans too.

Like, I was thinking that something like 1 + ((2 + (x + 4) + y*5) + 5 + z*(x+3) could actually normalize to 12 + x + 5*y + (3+x)*z. The constants would appear either first or last, variables would also appear in a sorted order (within products and outside of products). The question is, of course, would be how far we want to take it.

One of the advantages would be that constants would always coalesce (as opposed to the 3 + x + 9 example above). We could even go crazy and decide statements like \(x : Natural) -> (x+3) == 0 are false 😉.

I think some forms of my suggestion would be feasible to implement, and I might try it in my dhall-purescript project, but I don’t know if it’s something you would want to standardize. Just wanted to mention it :)

Gabriel439 added a commit to dhall-lang/dhall-haskell that referenced this pull request Nov 14, 2018
@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 14, 2018

Here is the matching pull request for the Haskell implementation: dhall-lang/dhall-haskell#681

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 14, 2018

@MonoidMusician: Yeah, feel free to experiment! Just be sure to provide some way for users to optionally specify pedantic adherence to the standard because differences in normalization behavior that don't match the standard will affect the semantic integrity check

Speaking of that, we might want a way for implementations to register deviations from the standard in the standard version field of the binary protocol. i.e. instead of encoding "3.0.0" they could encode "dhall-purescript-X.Y.Z"

@f-f

This comment has been minimized.

Copy link
Member

f-f commented Nov 16, 2018

I have two feelings/concerns about this:

  1. Is it obvious that the computations (with and without the "re-association") terminate with the same result?
    Intuitively it is - because the operators are associative - and it's easy to self-convince that this is true for Bool and Natural and their operations, but for stuff like Records and operators like and it is not that straightforward to me..
  2. Is this a slippery slope? As in: how much stuff is Dhall eventually going to be able to reduce?
    I feel we should consider/voice this aspect explicitly (in a more structured and "slower" way than case-by-case consideration?), otherwise we might face the risk that Dhall could become too complex for its original job (and this means being harder to bootstrap a new implementation, which is quite important at this point)

(P.S.: only the first question is really about this feature, the second one is about the language design process in general)

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 16, 2018

@f-f: The other operators are all also associative. Specifically . is the only non-associative operator in the language, and that's an undocumented design decision that I've been using so far that all new operators should be associative.

However, I'm totally fine closing this for now, because I'm actually not strongly attached to this specific feature. The initial reason I did this was for compact normal forms so that it's easier to reason about them. Formation had some very large expressions that their code was producing which would have been substantially smaller if we had applied the associativity exploits. The reason why is that they had a very large left-associated expression of the form:

x // { foo = a } // { foo = b } // .... { foo = z }

... and if it were right-associated, then it would collapse down to:

x // { foo = z }

Regarding the more general language design priorities that you brought up, the main use case that we are currently targeting is replacing YAML, for which this sort of thing is not necessary. Formation's use case is a bit unusual because they are using Dhall as a general purpose programming language.

However, if the language were to add dependent types in the future then the priority of adding robust simplification logic would go way up! As it says in the semantics.md document:

Dhall omits support for dependent function types because that would entail robustly detecting non-trivial type-level equivalences.

Given that we haven't committed to supporting dependent types, it's fine to postpone this for later.

Part of the reason I still went through with writing this up was because (A) I always volunteer to standardize things on behalf of users if they are unable to and (B) I perceived it to be pretty easy to add (just add two more cases to the pre-existing simplifications for each operator) and the scope was well-defined because there's a clear point at which you're done exploiting associativity.

However, I still understand the slippery slope argument and the need to make the language easier to port, so I'll close for now.

@Gabriel439 Gabriel439 closed this Nov 16, 2018
@f-f

This comment has been minimized.

Copy link
Member

f-f commented Nov 17, 2018

@Gabriel439 thanks for the writeup! 🙂

Would it make sense to pull the change in dhall-haskell anyways, as a pure performance optimization? (as there are already, e.g. build/fold fusion)

I think at this point it would make sense to even add a non-binding section for "optional performance optimizations" to the standard, so that we could clearly separate the semantics for "making it correct" and for "making it fast" (e.g. here in this PR the two aspects were going to be mixed).
In this way we could standardize all these nice things while still keeping the bar low for bootstrapping an implementation.

@FintanH

This comment has been minimized.

Copy link
Collaborator

FintanH commented Nov 17, 2018

Is it obvious that the computations (with and without the "re-association") terminate with the same result?

If this could be proven for each operator could we introduce these semantics?

Is this a slippery slope? As in: how much stuff is Dhall eventually going to be able to reduce?

I think Dhall's normalisation is one of its selling points thus we should strive for this strong normalisation. Personally, when reading (((x + 1) + 2) + 3) + 4) as output my brain thinks, "Why isn't this normalised?"

As an aside, I think it's interesting that we, Formation, ran into two cases where associativity bit us and needing right associativity was the way to go. The first was mapping repeatedly and this was solved by introducing Yoneda (blog post coming to your local internet soon), but probably not solvable at the Dhall level. The second was the one mentioned above and this was solved by explicitly writing the update for the whole record, which could be solved at the Dhall level. I'm not sure if this points to something indicative, but I thought I'd share 😊

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 17, 2018

I think one thing we can do is wait until we have three complete implementations of Dhall before we start adding more simplifications. At that point we'll have a better idea of how cumbersome it is to port the language and how much cost these simplifications add

@FintanH: I agree that the simplifications can greatly improve reasoning about code. However, while the scope of just associative simplifications is well-defined, the scope of what further simplifications we should allow is less well-defined. For example, @MonoidMusician brought up the possibility of more interesting arithmetic simplifications. Another example that Formation brought up was simplifiying (x // { foo = 1 }).foo.

Finally, there's the looming issue that you can't detect all possible equivalence in general in a language that is a superset of System F, meaning that the simplification system will always be necessarily incomplete.

@f-f: The main reason I haven't merged the functionality into the Haskell implementation is because changing the normalization behavior would affect semantic integrity checks for expressions where the simplifications would apply. I could hide the behavior behind a flag, but the Haskell implementation is already starting to be over-customizable to a fault, which is making it more difficult to read and understand the code as a reference implementation.

@FintanH

This comment has been minimized.

Copy link
Collaborator

FintanH commented Nov 17, 2018

So something I'm not understanding is since, "I agree that the simplifications can greatly improve reasoning about code. However, while the scope of just associative simplifications is well-defined", then why did we drop this? 😄 The aim of this PR was to take advantage of our knowledge of associativity and nothing more after that; but then @MonoidMusician mentioned more algebraic laws.

But I suppose the answer to my question is other Dhall implementations?

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 17, 2018

@FintanH: The primary reason is to support getting other implementations off the ground. The secondary (related) reason is that we don't have a clear criterion in general for deciding which simplifications should be added to the language. The reason we want such a criterion is so that people who commit to supporting the standard can anticipate what is the extent of the work they are signing up for.

@FintanH

This comment has been minimized.

Copy link
Collaborator

FintanH commented Nov 18, 2018

@Gabriel439: Cool, thanks for the clarification!

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 18, 2018

@FintanH: You're welcome! 🙂

@FintanH

This comment has been minimized.

Copy link
Collaborator

FintanH commented Nov 18, 2018

Final question actually!

we don't have a clear criterion in general for deciding which simplifications should be added to the language

Shouldn't we start thinking about this? If you haven't already 😄

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 18, 2018

@FintanH: I have, and the conclusion I came to when I thought about it was to not add any new simplifications until Dhall is mainstream.

The reason why is (again) inspired by the book Crossing the Chasm which says that in order to displace the market leader (YAML in this case) you need to focus your limited resources on being better at the things that the existing users care about. In this case, the target audience of people who use YAML and are looking for a better alternative care about:

  • Having a sane standard
  • Not having quirks
  • Being widely supported
  • Not being repetitive
  • Being easy for humans to edit and maintain
  • JSON-compatible

These people don't really care that much about slick simplifications and while these simplifications will create nice demos they won't drive adoption. That doesn't mean that we shouldn't add simplifications but it should not come at the expense of delivering on the features that matter or making it harder to port the language in its infancy.

@FintanH

This comment has been minimized.

Copy link
Collaborator

FintanH commented Nov 18, 2018

And thank you again! Understandable :)

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Nov 18, 2018

@f-f: You're welcome, again! 🙂

@Gabriel439 Gabriel439 mentioned this pull request Jul 23, 2019
0 of 1 task complete
@MonoidMusician

This comment has been minimized.

Copy link
Collaborator

MonoidMusician commented Jul 24, 2019

I feel bad because my comment sparked further discussion which seemed to shut down the issue, which wasn't my intention …

I just want to clarify that FWIW I'm certainly in favor of simplifying based on associativity. Especially because you've made a point to keep the operators associative, which I appreciate :) And also because it seems we are seeing performance issues because of associativity misses – in particular, the idiom of r // { … } is widespread and often appears with the association that prevents it from being normalized further. I don't think that associativity is a difficult one to standardize or implement. So those are the reasons I see to support normalizing associativity at least.

Now, it does irk my mathematical brain slightly that expressions like 3 + x + 9 don't get normalized more, but I can deal with that bugbear :D I agree that there's a value cost for adding more (or just lots) of normalization cases, regarding ease of implementation and clarity in the standard, and just how much Dhall is supposed to do, as a language. I think there might be some elegant solutions to some of these things. But I understand the implementation burden, and I didn't mean for any of that to shut down discussion on these proposed changes. Speaking of which, I should get back to work on my implementation …

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

4 participants
You can’t perform that action at this time.