I’m trying to figure out why function equality is considered hard (or undecidable).
Is it because of an overly aggressive definition of equality? For example, I can understand why it would be difficult to determine that two implementations of a function were identical without comparing the generated code or ASTs or whatever and that this would become even worse (impossible) in the presence of commutative and associative operations, etc. After all, the halting problem is essentially asking whether a particular function is equivalent to the function that fails to halt.
But this seems like an overly aggressive definition of equality in a programming context even in a context with referential transparency. It seems like all a language with referential transparency needs to provide is:
A set of “primitive” values for which equality is defined. For example, equality for integers is numerical equality for integers.
Equality needs to be reflexive, symmetric, and transitive.
A guarantee that if fn1 “equals” fn2 and arg1 “equals” arg2, then fn1 arg1 “equals” fn2 arg2. In other words, enough to make substitution work since function application is our only method of combining items.
Now, think of functions in terms of “templates” and “instantiations”. A function template includes its code and its references to other global values. A function template essentially corresponds to a particular piece of source code and gains its identity for equality purposes from that relationship. A function instance is created from a function template by binding any lexically-scoped free variables not tied to globals (those having been handled at the template level). Given this construction, just like other data structures we now have a DAG terminating in primitive values at the leaves. Function templates are primitives and we don’t attempt to identify them as equal beyond source code identity. Function instances reference templates and lexically bound values which have to exist before the instance is created and hence cannot create cycles.
Am I missing something? I can understand where Elm’s actual implementation of functions might make this harder to check. I also see where it might be desirable to have a more expansive definition of equality that would recognize more values as equal to one another, but I would then ask about the reasoning that drives that trade off in terms of issues like performance and inability to test function equality.
I believe the root issue is how to implement this in Javascript. I believe === in js works by identity, which is useless for Elm, especially when you consider curried functions. I also don’t think JS gives you the possibility to inspect two functions for structural equality (might be wrong).
Say that forall x it is true that f x == g x using simple structural equality on the return values. Should f == g? (Q1)
Seems reasonable, but then you have to prove arbitrary function equality. So you can choose “no” for technical reasons, but shouldn’t (\x -> x + 1) equal (\x -> 1 + x)? (Q2)
It seems like those are equal, but for technical reasons, one would need to argue that these are definitely not equal.
Point is, you can choose “only syntactic equality counts” but I personally don’t think it’s a better design. It can be implemented, but I think (\x -> x + 1) is equal to (\x -> 1 + x) and would not be comfortable saying otherwise.
Anyway, hopefully Q1 and Q2 are helpful to your inquiry into function equality more generally. I know equality is a topic of debate/discussion in dependently typed languages, so I bet there are Coq resources that might give a more complete analysis of different concepts of equality.
To add on top of @evancz said, @MarkHamburg, the main term you might want to search for to get more details on this is “intensional equality for functions,” which is the name for the general class of equality proposals like yours.
I personally think that intensional equality is not the right tradeoff for Elm as it stands right now. In particular, by allowing programmers to “open up a function” so to speak, intensional equality damages some otherwise pretty ironclad guarantees that are very useful for refactoring in Elm at the moment.
Equational reasoning. When refactoring in Elm, we can generally treat = as completely equivalent rewrite rules in either direction. Any instance of the left-hand side or right-hand can replaced with the other without affecting the behavior of an Elm program. Not only does this allow things like elm-review to provide automatic fixes for a lot of its rules, it also is generally just very very helpful informally when a programmer reasons about how to refactor a pre-existing codebase.
Function output is the only thing that matters. This is closely related to equational reasoning and depending on your perspective you could say this is a simple consequence of it, but similarly today when we refactor an Elm function, we only need to consider whether it reproduces the same value as it did before. Alongside unit tests and property tests that only need to check function outputs, this gives us great confidence that our refactors don’t go wrong.
You lose these with intensional equality, because all of a sudden runtime behavior can be changed by function implementation. identity becomes a bit scarier of a function to introduce willy-nilly because f /= identity >> f.
In return you don’t get much back in Elm as it currently stands. Any place where you would want to store a function in a data structure, which is then compared for equality, can always be replaced instead with storing a single piece of data in the data structure which is then converted to a function on the fly. And because in Elm there is no eval function, this approach is always sufficient since the program that generates the function and the program that executes the function is always the same (eval would allow for a runtime user to generate the function instead of the program, I address the other end in the next paragraph).
The main place I can see where you would really want something that ends up implying intensional equality is function serialization for distributed systems, that is an environment where you can pass arbitrary functions to arbitrary compute nodes which may or may not share the same programming context as your coordinating node. But absent that kind of functionality on Elm’s roadmap, I would argue that intensional equality is not the way to go in Elm.
I raise the issue because it feels like function equality tests fall into an awkward category of runtime error in Elm. Stack overflow is essentially the halting problem and can’t be solved. Cyclic dependencies aren’t caught at compile time but happen reliably at module load time and hence should not escape into production. Function equality checks only generate runtime exceptions when the comparison is performed and the functions being compared are not referentially equal. That means it can lurk unseen. What’s more as we’ve seen in other questions and reports, people can be surprised that something like a decoder contains a function inside and hence a structure containing a decoder cannot be checked for equality even though there are no functions in immediate sight.
Evan’s desire to have an aggressive definition of equality more or less establishes that the only way to address the runtime error issue is to have another type-class like concept to handle equality. It’s Evan’s language, so he can pick the definition he wants, but it might be nice then to get the compile-time checks.
My sketch of a proposal takes a more conservative view of what it means for things to be equal within a programming language in that it allows for more things to be reported as not being equal to each other. For example, if we define fn1 x = x and fn2 x = x, then I am prepared to say “these are separate textual definitions and are not equal”. This is not as beautiful mathematically but it’s arguably more beautiful than potentially crashing in production and it remains useful in practice for the same sort of cases as lazy Html. Furthermore, note that while I believe Elm goes beyond structural equality for dictionaries, data structures not implemented in the core only get structural equality even if the available APIs would make them appear equal, so this departure from mathematical ideals is not without precedent.
At the same time, my proposal does seek to maintain referential transparency. If we apply “equal” functions to “equal” arguments, we get “equal” results. For example if we define:
adder n = \x -> x + n
then adder 3 == adder 3 which would not happen with simple referential equality.
@yosteden Thanks for pointing me to the term “intensional”. The answer is that what I’m suggesting is roughly related but since “intensional equality” is only roughly defined, that’s as good as one will get.
The more interesting point (from my standpoint) that you raised is the behavior of the >> operator. Referential transparency would not need to have fn == identity >> fn. That’s a separate property that says that identity is the identity element for >>. Similarly, referential transparency does not depend on >> being associative. One response is to make sure that the implementation of >> works “properly” with the implementation of equality. For example, it can certainly special-case identity as the identity element even if it does not recognize that \x -> x is also effectively an identity element. The set of valid program transformations then need to account for what the definition of equality within the language provides. This isn’t a new situation if mathematics guides you to reason about floating-point numbers as if they are reals. A lot of transformations that are valid for reals are invalid for floating-point numbers if the goal is to maintain equality. So, any set of valid transformations really needs to take into account representational concerns and what promises the language actually makes.
Regarding Q2, I think not. There is no a priori guarantee that forall f, a, b: f a b == f b a, hence one wouldn’t expect the compiler to in general be able to prove that. This is particularly the case if one takes (very reasonably for a practical programming language) performance characteristics into account. For instance longList ++ [] == [] ++ longList, but the runtime might be entirely different. In that sense they are absolutely not the same function.
My only gripe is that Elm chooses neither. It doesn’t commit to solving “structural function equality” (whatever that would look like), and it doesn’t commit to syntactic equality either.
Instead we get “function equality works but only sometimes because of how equality short-circuits on reference equality but other times it just runtime crashes.” Elm already compromises on its “no runtime error” guarantee with function equality, I’d rather it compromised on =='s integrity and just said all functions are false unless referentially equal.
You can think of my proposal as being structure equality. Each function in the source code — nested functions count separately — defines a constructor case in a big hidden custom type of all (defined) functions and the lexical values bound for the function are the constructor parameters.
Interesting. I would have reversed those choices. The first is two different function definitions that happen to compute the same thing. The second is two bindings of the first parameter of the plus function to the value 1.
You’ve missed my point. Elm does none of this and instead breaks your program. My suggestion isn’t a solution to function equality its a bandaid to stop programs breaking in production because of unreliable equality semantics.
Same reason our programs don’t runtime error by diving by 0.
Or the compiler could give an error when equality is applied to functions, since it should always be able to know this from the type? But I agree, a wrong answer is also a better solution than a runtime error.
The two paragraphs below are perhaps false because over-simplified.
Elm is a language for doing computations. It is not a language for proving statements. Proof assistants (such as Coq and LEAN) can be used to prove statements.
There do not exist general methods for proving that two functions are equal. If we had such a method, we’d have a general method for proving statements. But there’s the halting problem.
I have a question for @MarkHamburg. If Elm supported function equality, how would you use it to build a better web page?
Example: Being able to test function equality makes it easier to do certain forms of caching which makes it easier to build more performant web pages. Elm’s built-in support for lazy HTML is an example of such a thing but it isn’t the only such thing.
More broadly for better web pages, function equality crashes slip too easily into production and it would be nice to either see them supported or prohibited by the compiler. (See message 5 in this thread.) Prohibition by the compiler would be pretty disruptive to existing code since any type parameters with values tested for equality would presumably need to be revised along the lines of comparable. So, I was looking for an implementation of function equality that maintained referential transparency.
@MarkHamburg claims two benefits for function equality being part of Elm’s run-time, quicker pages and fewer crashes. I’m not convinced.
(Sorry for the long message - I think the detail helps. Disclaimer: I’m an Elm beginner, with much experience in pure mathematics and logic.)
Quicker web pages
I don’t see how it’s possible that being able to test for function equality will make it significantly easier to build web pages that run quicker.
If function equality means syntactic equality, then why can’t you use Html.lazy. (Just use a master function which branches on a flag / key kept in the arguments to the master function.)
If function equality means more than syntactic equality, then you’re asking for an expensive calculation to take place at run time. That will harm performance, in an unpredictable way.
Since functions are objects in JS perhaps we could assign an id property to a function and take a page out of cryptographies book and hash the arguments and function id into a unique string for equality check?
But personally I would rather we avoid that performance overhead and do like Roc Lang and just compile time crash on function equality checks instead of runtime. Runtime crash just makes it look like Elm lied when it said no runtime errors. It’s a bad look
I think this would be a more practical trade-off. Using reference equality in this one case seems less surprising and less likely to cause production problems to me.
The thing that makes me more scared about the function equality strategy is that, unlike JS – where I’m the metal defining functions myself and I know they have the references I expect – when I’m in Elm I have no idea how my definitions (lazy? auto-curried?) will turn into actual javascript functions, if there will be some optimizations that makes my superficial understanding different from what is actually happening under the hood.
This would create the problem of a “lack of runtime expections” but for the wrong reasons since things would be working in a possibly buggy behavior without the possibility of realising it.
Maybe this is just my lack of understanding about how it works tho.
I think there is one place where function equality is commonly useful: Occasionally, one wants to create (or use) semi-generic data structures that require more information about the values of a given type than equality. For example, a Dict needs an order on the keys and a HashSet would need a hash function on the potential values. Now, Elm generates some instances of comparable, but custom types are left out. There is no hashable at all.
If one wants to use custom types in these data structures, there are the following options, none of which I find particularly good:
Replace a custom type that happens to be used as a key in a Dict by ints, strings and tuples of those two everywhere. This loses type safety in all other parts of the app.
Create a toKey function from your type to a type that can serve as a key, and insert this function whenever the type is used as a key. This is quite verbose and not in a way that increases code clarity, in my opinion.
Create a new module containing a copy of (parts of) Dict’s API, only with all the toKey calls already included. This is also busywork and it requires the reader of the code to keep an additional type in their head. Also, it increases the size of the compiled product.
A solution to this problem are AnyDict implementations that store the toKey function with the data structure (so you only need to supply it when creating a new instance, not on every operation). They currently work reasonably well: If you always supply the same global toKey function on instantiation, you can even compare them for equality, as references to the exact same function can be compared for equality and are considered equal. If you mess up and supply different functions, you run into a runtime error. (But in particular, always using a top-level toKey is a good heuristic to ensure that only one copy of the function exists.)
If other goal is to remove the runtime error, there should be a solution to the generic data structure problem of some form. Replacing the runtime error by False would do that, though I’m not convinced that replacing errors by default values is not more dangerous than the error (you might corrupt data because you work under false assumptions). Introducing an equatable constraint to exclude function from == altogether does not. Making more types comparable in exchange would help with the case of Dict but not with other situations (e.g., a potential HashSet).
