Consolidating Unification with fd-unification

[bladyjoker]

PRIORITY: MEDIUM

There's an opportunity we could use to consolidate and structure our internals in a way that signals the underlying intention more clearly, removes unnecessary code in favor of reusing a well-tested library https://hackage.haskell.org/package/unification-fd-0.10.0.1/docs/Control-Unification.html.

We introduced a separate ad-hoc machinery to work with unifiable terms:

1. https://github.com/mlabs-haskell/lambda-buffers/blob/b36982041bde869f0b6b27d7f98711352521d994/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs#L131
2. https://github.com/mlabs-haskell/lambda-buffers/blob/ce6830ca68ca4b050f3e925d81cdc9757494ff08/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Pat.hs#L1

And as a result of that we have small implementations laying around that perform what is essentially unify, subsumes and freshVar in Control.Unification.

Logic programming requires us to clearly state:

1. What are 'ground' terms,
2. How do you lift 'ground' terms into 'unifiable' terms,
3. What are 'unification variables'.

By using Control.Unification we could have a common module in LambdaBuffers.Compiler.Unification where the necessary ProtoCompat.Types are lifted to their 'unifiable' counterpart and the monad stack is defined with the BindingMonad and Fallible.

This could then be used throughout the Compiler, but it could be also used in Codegen.

[gnumonik]

Repost from slack (so this doesn't get swallowed in the channel):

We're not actually doing unification in the typeclass stuff. Pattern matching is very similar to unification but only works in one direction. If we rewrote match using Control.Unification we'd end up in a situation where a general instance head in a user-defined clause would match a specific rule. Example:

R = rule C (Maybe Int) -- pretend this is an "instance rule" 

I = instance C (Maybe a) -- pretend a user writes this in an instance/deriving clause 

I and R unify because unification is bidirectional. 
I doesn't *match* R because I is more general. 
Matching only goes from general -> specific  

Pattern matching aims to determine whether Y is a substitution instance of X (where we fail if Y is more general than X) whereas unification attempts to determine whether X is a substitution instance of Y OR Y is a substitution instance of X c.f. here & here

We do not want the latter. We want pattern matching.

[gnumonik]

It's true that we could rewrite the typeclass machinery w/ Control.Unification but there are real costs to doing so:

• It forces us to adopt a monad transformer stack where we have simple pure functions
• I believe that it will greatly complicate the logic in solve if we want to replicate the "returns all unsatisfied subgoals" functionality that is necessary for the compiler checks. We'll have to "run" the whatever BindingMonad we choose at very specific points
• That will require one (or more) new kind(s)of internal error that we otherwise do not need
• We lose the ability to insert traces at key points to debug
• It will become a lot harder to maintain or upgrade because of the above points

At any rate, I don't think we're clearly communicating our intention if we use Control.Unification for pattern matching. We could eliminate Pat using one of these first-class-patterns libraries, however I do not really think we gain very much from that.

Edit:

One thing we could do, which might please you, is to rewrite match so that we don't need to convert TyDefs & friends into a Pat to perform the matching. Then we could clearly communicate that patterns are always meant to be general and would only serve to express rules.

[bladyjoker]

This library is used, we haven't achieved consolidation. Probably when we get to spring cleaning internals.