Function equality

The plan is to add an equatable constrained type var. I thought people knew this from the error:

Error: Trying to use `(==)` on functions.
There is no way to know if functions are "the same" in the Elm sense.
Read more about this at:
https://package.elm-lang.org/packages/elm/core/latest/Basics#==
which describes why it is this way and what the better version will look like.

Following that link gives the following message:

Note: Do not use (==) with functions, JSON values from elm/json , or regular expressions from elm/regex . It does not work. It will crash if possible. With JSON values, decode to Elm values before doing any equality checks!

Why is it like this? Equality in the Elm sense can be difficult or impossible to compute. Proving that functions are the same is undecidable, and JSON values can come in through ports and have functions, cycles, and new JS data types that interact weirdly with our equality implementation. In a future release, the compiler will detect when (==) is used with problematic types and provide a helpful error message at compile time. This will require some pretty serious infrastructure work, so the stopgap is to crash as quickly as possible.

I also mention this in the roadmap:

add a constrained type variable eq to get rid of the runtime error for (==) on functions

To give some extra context, the current behavior is under the theory that, in the absence of the compile-time check, it’s still best to fail as soon as possible. That way type error can be corrected. I think this is better than having behavior like “it’s always false” or “use reference equality” or “use syntactic equality” or whatever which would (1) prolong the life of such code, (2) still be extremely surprising to some large subset of people, and (3) make the eventual introduction of an equatable type even more disruptive.

I appreciate that not everyone agrees with this reasoning, but I hope this clears up that aspect of this discussion. I also appreciate that people in the conversation may not have seen the error message recently / may not remember the exact details of it, so no worries. I just want to add these details in!

Nonetheless, I’m sorry I did not mention that this was the plan in my initial comment. I thought the poster was just asking, “the current behavior/plan makes sense, but what if (==) could be defined on functions in a good way that would work as a long-term solution?” That is an interesting theoretical question.

In languages with dependent types like Coq, you can prove things quite like this! For example, I had a compilers course where we wrote a simple evaluate : AST -> Value function and then proved that it had the same behavior for all inputs as a compilation pipeline that introduced optimizations. That way you can have a proof that your compiler (and all of your optimizations) preserve the language semantics. These proofs cannot be inferred, and I personally found it extremely difficult to create the proofs myself, but it is still quite interesting to think about.

I thought the discussion was going to be mostly about that kind of thing.

19 Likes