# Function equality

**URL:** <https://discourse.elm-lang.org/t/function-equality/7538>\
**Category:** Learn\
**Created:** [July 12, 2021, 4:32pm UTC](https://discourse.elm-lang.org/t/function-equality/7538 "2021-07-12T16:32:21Z")\
**Posts on this page:** 1\
**Showing post:** 25

<div class="post-metadata">

**Author:** ![jfine2358](https://yyz1.discourse-cdn.com/flex035/user_avatar/discourse.elm-lang.org/jfine2358/32/3875_2.png) [@jfine2358](https://discourse.elm-lang.org/u/jfine2358)\
**Post date:** [July 20, 2021, 6:07pm UTC](https://discourse.elm-lang.org/t/function-equality/7538/25 "2021-07-20T18:07:42Z")

</div>

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 `equatable` type

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.

---

_[View the full topic](https://discourse.elm-lang.org/t/function-equality/7538)._