Replace unification-fd with a custom implementation of unification
#1802
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Replace with modern standard implementations of `Free` and `Fix`.
Now getting weird compile-time errors from some quasiquotes
Now it compiles but almost everything in the test suite is failing =)
Composition of substitutions is not commutative!
Compared to the naive implementation, this brings down the time to run the whole test suite from ~190 to ~140 seconds---though still slower than unification-fd (~120s), which is to be expected.
Co-authored-by: Restyled.io <commits@restyled.io>
…warm into refactor/custom-unification
kostmo
approved these changes
Apr 26, 2024
Comment on lines
+122
to
+123
| -- unification is subtly wrong; fortunately, a single integration test | ||
| -- in the Swarm test suite failed, leading to discovering the bug. |
There was a problem hiding this comment.
It was Challenges/Sliding Puzzles/_sliding-puzzle/solution.sw that failed to typecheck, specifically the getInitialBlankDestination function. Something about the way it involved inferring the type of a higher-order function that took tuple projections as an argument tickled the type inference algorithm in just the right way to trigger the bug. So thanks for writing that code! 😄
Closed
byorgey
added
the
CHANGELOG
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Closes #1661; towards #154.
unification-fdis very powerful, and extremely fast, but it was written a long time ago and its age shows. It was not possible to incorporate it into our effects system in a nice way, necessitating the use of concrete monad transformers in the typechecking code. In addition it is impossible to customize, and we have been contemplating new type system features such as #153 and #154 that turn out to require hooking into the way the unification algorithm works (see #154 (comment) for more details).This PR thus removes the dependency on
unification-fdand implements our own version of unification. It is not quite as fast asunification-fdbut I consider the slowdown acceptable in order to gain e.g. recursive types. And of course there is also room to optimize it.The custom
UTermfromunification-fdis replaced with the standardFree(free monad) construction from thefreepackage, and the customFixfromunification-fdis replaced with the one fromdata-fix.We also get rid of the
unifyCheckfunction, which used to be a quick short-circuiting way to check whether two types definitely did not unify or might unify, allowing us to give better error messages more quickly. Now, the=:=unification operator itself just does this.