I’ve spent some time reading the Elm generated JavaScript and I think in practice the behaviour isn’t surprising, so luckily this potential problem is easy to avoid.
1 Like
I was ready to let this wind down having gotten early on Evan’s definitive view that he would prefer functions be declared equal if they computed the same thing which really is impossible to compute. I just think that then argues for a type system mechanism to prevent such equality checks from sneaking into the code.
But I stirred the hornet’s nest and it seems some of my explanations for why this might matter have lead to more confusion.
First, on crashes, I refer again to message 5 in this thread. Function equality check crashes in Elm fall into a category that is both potentially detectable at compile time (unlike stack overflow) but aren’t caught. They can’t be caught at module load time the way cyclic references are. Instead, you have to actually perform the comparison and not have it short-circuited by referential equality. The net result is that this is a path to what could have been preventable crashes in production. It also leads to incidents like the recent case of someone here being puzzled at why comparing HTTP requests could crash. To understand why, you have to know that Decoders are basically wrappers around functions.
Second, utility and performance. From a performance standpoint, lazy HTML demonstrates the value of caching. What if one wanted to build a caching mechanism for something else? For example layout computations that could not be handled by HTML or queries filtering down a dictionary full of items or subscription computations. But more broadly, the thing that characterizes functional programming languages is that they are much more friendly to building data structures that include functions as a first class component. See, for example, the discussion earlier in this thread about building dictionaries with the comparison function baked into the data structure. But if function equality checks can crash, then these need to be treated as second-class data structures ineligible for equality tests.
Finally, solutions. There seem to be three ways out if one doesn’t just accept the risks inherent in the current state of affairs. One is a type-system mechanism to prohibit function equality tests and hence equality tests of anything containing functions. One is to just use referential equality for functions. In practice, this will work but it does break some ability to reason about programs since it breaks referential transparency. And one is something like the structural equality definition I outlined which has the downside of being harder to compute with Elm’s current JavaScript implementation.
And with that summary, barring any significant new arguments — I really did find the point about >> semantics interesting to consider — I will now just tell myself that I’ve already pointed to all of the key issues.
An improved description of the existing behaviour of Elm would be a useful outcome of this discussion. This would help those who encounter problems with function equality.
I’d like this to state that function equality is an NP-complete problem, as in:
I feel that once the existing behaviour is better explained and understood, we’ll be better able to consider changes to Elm’s behaviour.
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 fromelm/json, or regular expressions fromelm/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
eqto 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
I thank @evancz for explaining why he has implemented (==) as he had. His reasons are practical. I particularly like:
(3) [to avoid disruption due to] the eventual introduction of an
equatabletype
I read this as placing a high value on consistency with the math and logic definition of equality for functions. I think this is a reasonable point of view, even though the original poster describes it as overly aggressive.
If we had a partial implementation of the math-and-logic definition, then I think the development tool-chain would be a good place to use it. It could be used, as evancz says, to prove that optimizations (and refactoring simplifications) preserve the semantics of the code.
By the way, in his Structured programming with goto statements (1974), Don Knuth explores the idea of what he calls an interactive program manipulation system. This seems to be similar to what evancz described. Such a system is perhaps a refactoring assistant, much as Coq and Lean are proof assistants.
1 Like
Would it not be pretty easy to have a “compile time error” for this using elm-review in the meantime? I have not yet written my own rule/looked at the api so would someone with knowledge give their view? (I could not find any existing elm-review rule for it.)
@mika I would recommend reaching out to @jfmengels. He would likely know best and would probably point you in the right direction if you wanted to attempt to write this rule yourself (assuming it’s possible).
I could defend Q1=no and Q2=no with the following logic.
An Elm function doesn’t have to be a naked pairing of inputs to outputs. Alternately it could be treated as a specific definition of code that happens to pair inputs to outputs in a repeatable way. Sort of like an ADT opaque wrapping of a naked pairing of inputs to outputs.
If you think about what coders are after when they test for function equality, it’s not usually “will these two things offer the same output for every input”… which is lucky since that’s literally impossible to prove in a general sense, and since it fails to implementational troubles like confusing reals with IEEE 754 floats, etc.
No, usually a coder wants to know “is what’s in this step the same value I fed into the chain of functions earlier?” Or alternately, “Is the token over here the same as the one this package advertises as a default?”
So instead, let’s think of it like an ADT. Where creating a function (\x → x + 1) is really in a sense creating a wrapped object Func#17 (\x → x + 1) where the wrapper is an arbitrary unique product of where that definition was made.
Now only that object defined in that location can ever equal itself, so even x = (\x → x + 1) and y = (\x → x + 1) would set x and y as not being equal — and that could be justified by having different conceptual function wrappers due to being defined at different locations in the code.
If we do it that way then currying might not be so difficult for the compiler to support as well.
x = {conceptual ADT Func#66} (\x y → x + y)
y = x 3 {conceptually, now y = ( 3 |> Func#66 (\x y → x + y) ) or even just ( Func#66 3 ) internally}
z = x 3
and then it makes sense that y == z or y == (x (2+1)) or whatever because they are all derived from the same function defined at the same location, and then only ever curried together with equal input values.
If we were able to define function equality that way, and allow all functions that do not spring from the same definitions to be unilaterally not equal, then I think I would be comfortable with things on every level:
- I don’t think there are any concrete uses that would be stymied
- We’d shut down that path to runtime exception, obviously
- We would support black box implementations where module developers could swap opaque objects out for things that contain functions without breaking calling code
- We would avoid leaky abstractions where people might expect “mathematical” equality to translate into demonstrable equality.
- And our concept of equality would survive currying, function nesting, and basically every real-life thing I can think of that would actually lead people to care about in what sense any functions are “equal”.
Furthermore, I don’t see how @yosteden’s point about refactoring helps here: currently “f == (identity >> f)” gives a runtime error, and I don’t see why that would be preferable to having a false value.
We shouldn’t write tests comparing functions as a shorthand for all possible input/output pairs anyway, we should just be writing good fuzz tests to directly test said input/output pairs. if g = identity >> f then we can feed as many inputs into f and g that we’d like and test to confirm their outputs match instead of trying to interrogate the function directly in a sense that is literally impossible.
But at least my proposal let’s us do things like compare functions curried from the same source with matching partial inputs, and a fair few other — predictable — transformations as well. 
I decided to give it a go but as most of the times stuff is not as easy at it seems.
My assumption is that we should be able to report error when using a “non applied” function in equality checks. That is assuming this always results in a runtime error. Does there exist cases when that would not give a runtime error?
Here is my attempt if someone wants to help out:
Started out copy pasting some example so yes it is a mess.
It seems doable at least. My plan was: Collect all functions (that takes arguments) and collect all Expression.OperatorApplication by ==. Then compare those in the end.
Elm-review is new to me so I have not managed to store the moduleName for functions etc.
fx x = 1
fy x = 2
ffx x y = 1
ffy x y = 2
t1 = fx == fy
t2 = ffx == ffy
t3 = ffx 1 == ffy 1
The thing collecting Expression.OperatorApplication for == needs to be recursive and handle other expressions i.e. records (with functions) etc. So for above code it collects the functions for t1 and t2 but not for t3.
I am unsure if this would cover all runtime error cases though. Are there cases this would give false positives? Also @jfmengels (ignore my ignorance of how to write elm-review rule) do you have any take on if this is feasible or other input?
You can find a short discussion/proposal on a rule that would do something in the same vein
I think you will have false positives (when you report an error but shouldn’t have) and false negatives (when you don’t report anything while you should have)
I think you need some kind of type inference to be able to detect these.
For instance, if you have
Maybe.withDefault identity maybeFunction == ...
Then you need to infer the type of the expression on the left to understand that it will result in a function. It’s possible, but not something I have been able to have built-in into elm-review at the moment.
Another false negative is that you need to understand when a function will try to compare things.
isEqual = (==)
a = isEqual b c
If b and c are or contain functions, then this should not be allowed. The places where isEqual is used should also be checked, in addition to all the places where == is used. Same thing for any function that does this equality check at any point in their code (directly or indirectly) where the types would allow the comparison of something that contains functions (meaning all functions except where from the type signature you can confirm the inputs won’t contain a function, or when you can determine that one of the == operands is not a function).
A third false negative, is that elm-review doesn’t look at the source code of dependencies, and without doing that, you can’t know whether a custom type (directly or indirectly) from a dependency, or a value from/containing that type, contains a function. We could if we knew whether the type was equatable or not though.
I can’t think of false positives off the top of my head, but I guess that detecting some true positives while never reporting a false positive could already be useful to prevent crashes.
I’m probably forgetting cases, and I haven’t looked at your code too much (don’t have access to a laptop at the moment), but this would be quite a complex rule to create.
This is typically a case where you’d want the type system to take care of this, because we want to make something impossible based on the type of a value, not based on how it’s written.
I’m looking forward to see the equatable type in the language! And I’m very curious to see how the documentation (and docs.json) would display it.
2 Likes
Thanks for the thorough explanation. I understand now why this is complex and seems elm-review is bound by the same restrictions as the compiler I guess. Have made some progress so might continue on it but got a bit uninspired by the fact that elm-review doesn’t check dependencies. Did not know/realize that was the case which makes pursuing this not very worthwhile. I have learned something about writing elm-review rules at least. 
1 Like
The below may be redundant, but anyway, here is an
Example.
Consider first the function below, defined by recursion:
collatz n =
if n == 1 then 1
else if modBy 2 n == 0 then collatz (n // 2)
else collatz (3*n + 1)
One can write a program to show (for example), that collatz n == 1 for all n < 1000.
With this in mind, define the two function f n = collatz n == 1 and g n = True, where f, g : {Integers > 0} -> Bool.
We ask: is f = g? The two functions are not intensionally equal: they are defined differently. As for extensional equality, for all n > 0, f(n) = g(n), nobody (and no computer program) knows. To decide the issue is to prove a theorem. This is the Collatz conjecture.
3 Likes
This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.