What does = mean? Equality of terms, I now get. Equality of types still scares me.
Conversation
This Tweet was deleted by the Tweet author. Learn more
Thanks for bringing up the “definitional equality is quite bad for software development” thing too - it's something I've been pondering too. Attempted to talk about it here, for instance:
Quote Tweet
Replying to @taktoa1 and @andrasKovacs6
Yeah, I mentioned how changing the function definition of + can break client code, even if the type signature does not change. This is a pretty weird default behaviour for most programmers!
1
2
It's a double-edged sword – definitional equality being automatic means that you *can* refactor the definition of +, for example by using a recursion combinator rather than pattern-matching.
2
This Tweet was deleted by the Tweet author. Learn more
Trick is, though, if we had more ways of producing definitional equalities, it'd again become easier to preserve all of the equalities during refactoring. For example, if + satisfied the monoid laws definitionally, then any other reasonable implementation would too.
2
1
There’s actually a way to do this!
Jesper cockx has a cute paper a few years back about order independent pattern matching. So you just need to prove locally that for a given function, the clauses are equal on overlapping compatible inputs! This is one path to unstick defn eq!
1
3
What is the paper?
1
Probably this: jesper.sikanda.be/files/overlapp
1
1