Remove = sugar for propositional Equality

[andrevidela]

• I have read CONTRIBUTING.md.
• I have checked that there is no existing PR/issue about my proposal.

Summary

Currently, to use built-in propositional equality, we can use the = symbol between two expression to stand for either homogenous equality (===) to heterogenous equality (~=~). The proposal is to provide and upgrade path towards the removal of =.

Motivation

= as a symbol for propositional equality has the benefit of being easy to type and easy to read for newcomers. However, the benefits stop here. Because it overloads both ~=~ and === it can create situations where an error occurs because the compiler disambiguates into heterogenous equality, when homogenous equality was needed. What is more, the presence of this symbol makes the syntax quite a lot more difficult to parse since it has to be disambiguated from = as a clause.

The proposal

The main proposal is actually not about removing special syntax for = but to provide an upgrade path for existing packages making use of = so that we can avoid breakage. The traditional way to achieve this is to emit a warning for the deprecated feature, and to change this warning into an error in a subsequent version. This would be perfect if not for the fact that most users (and build systems) simply ignore warnings.

To remedy this, I suggest we selectively update the content of a compiled file to insert the correct operator, either ~=~ or ===. There are multiple strategies to do that, what I suggest is that we introduce a editor-action to replace the content of an expression by its compiled-tree version, so that users can easily desugar = into either === or ~=~¹. Once we have this, we can automatically replace the content of a file, when it's compiled, to the desugared form of =. Because we do not want this to interfere with interactive editing, it should not be run every time we typecheck the file. However, if we can compile a file with --build, run the code-action on every instance of = and compile the file again, in a way that we obtain the same typechecked tree, we could simply replace the file in-place with the new syntax.

Alternatives considered

Realistically there is only one alternative: Do nothing. Which is what we've been doing this entire time! Arguably, there is not much urgency for this proposal, but it would be a good academic exercise to deploy, at scale, our code-synthesis tools.

Conclusion

If we agree that we do need to remove =, all this work is more of an academic exercise, rather than an absolute necessity. This proposal is also quite brute force, and there might be better ways to do this, but for such a frivolous project, perfect is the enemy of good. And placing more sophisticated expectations on a translation solution might be enough to ensure it never gets done.

Footnotes

1. This feature has potentially other uses when exposed to the user(desugar if_then_else, desugar lambda case, desugar with), but I do not wish to examine them further in this document, nor is it the goal of this project. ↩

[buzden]

What I always liked about = comparing to === is that it has a presedence lower than even infix 0, hence the clean look for function signatures that serve as properties of equality. Current infix 6 is okay for === meaning an alternative comparison function to ==, but propositional equality type plays a different role.

= as a symbol for propositional equality has the benefit of being easy to type and easy to read for newcomers

I don't feel myself a newcomer, but I personally still find = much easier to read than === in most of the cases.

---

Another downside of === being the only standard operator for propositional equality is that === operator is used not only for the propositional equality, for instance it is used for equality-based checks in propety-based testing libraries.

---

You considered the only alternative of doing nothing. In the motivation section (along with unique presedence of =, which I really like) you mention ambiguity problem. I can propose an alternative solution alternative to yours one: instead of removing = in favor of explicit ~=~ and ===, we can consider removing only ambuguous semantics of =, say, sticking it to ===, since this is the most used case for it.

[andrevidela]

What I always liked about = comparing to === is that it has a precedence lower than even infix 0

I also like this, and experimented with the compiler to make = a proper operator with precedence -1 and that seemed to work. I think it would be a reasonable change to make (===) have a compiler-only precedence (like -1), but I wasn't sure if that was something that the people really want, or need. I'd love for more people to chime in on that topic.

Another downside of === being the only standard operator for propositional equality is that === operator is used not only for the propositional equality, for instance it is used for equality-based checks in propety-based testing libraries.

Not a problem with the new fixity namespace features. The compiler can detect if there is a conflicting fixity and generate the appropriate program if necessary. In this instance it would mean hiding the built-in fixity for (===) and calling equality in application position (Builtin.(===) a b).

I can propose an alternative solution alternative to yours one: instead of removing = in favor of explicit = and ===

I think that's a great idea, however it does not really address the upgrade path problem which is the main body of this proposal. We would still need to provide a way to upgrade without breaking existing code-bases. Like mentionned at the end: we don't really have to, but that's the essence of this proposal, to do something nice while learning something on the way there. I know we have a lot of issues right know with code synthesis and this would be a great time to review the infrastructure around it.

[mattpolzin]

I can propose an alternative solution alternative to yours one: instead of removing = in favor of explicit = and ===

I think that's a great idea, however it does not really address the upgrade path problem

I can see it as being a drop-in idea for the end-goal with your proposed solution for migration still being applicable. I think I like the idea of = remaining equivalent to === (possibly modulo precedence, though I didn't know they had different precedence and I am not sure I think that specific point is a benefit). I also like the idea of offering code actions that desugar various kinds of things.

The desugar code action initially seemed of arguable use to me outside of this very specific migration need, but the more I think on it the more I can imagine situations where lifting a with block into a standalone helper function could indeed be desirable.

I saved this for last because it is a bit "sunk-cost-ty" but I'm in favor of past work that served to differentiate e.g. assignment from equality by introducing := so we have in some areas already begun to narrow in on = being used for equality; this would seem to make those distinctions unnecessary and a bit of a bummer from the perspective of wanting = to be useful for something. Of course, = would still be used for function clauses, but regardless I don't think we have ambiguity problems between the equals of function clauses and the equals of an equality.