unification environment

[kowey]

OK, it doesn't have to be a monad. But I want to have some sort of abstraction that guarantees that when I do unification on something, the results from previous unification will be automatically propagated to that thing. Seems like it should be fairly straightforward. You could just model this as a state monad for example, and have the unification function get/put the substitutions state.

What may be annoying is having to write a monad transformer and slip it into our current MT stack.

The goal is to have something that makes our code easier to write, and less error-prone, while also staying cheap (we shouldn't be doing any needless traversals).

[kowey]

Imported from trac issue 18. Created by kowey on 1970-01-01T01:20:48, last modified: 1970-01-01T01:20:48

[kowey]

Renamed from monad to environment. I don't care how it's implemented, I just want a less error-prone way to do unification. The standard approach of unification variables pointing into a common environment might be better.

[kowey]

Phew, the way we're doing unification really is dreadful. And an environment doesn't sound so hard either.

[kowey]

OK, have a rough idea what to do maybe.

So problem is bugs caused by forgetting to replace, or not replacing on parent structure

Possible solution: anything with unification variables must have an environment (Var to Value). Let's call it U a. Unifying is U a -> U a -> U a

That is rather than running the replacements, you just have to swap the environments out. But forgetting to swap the environments can still be bad. Maybe this is where something like monads or something could be good? If you have some

data BigThing = BigThing
      { small :: SmallThing
      , etc :: Etc }

When you do unification on the SmallThing, one way or another we need to make sure the rest of BigThing receives the right values. So nebulous idea is that you would do unify :: U SmallThing -> U SmallThing -> U SmallThing and somehow go from there to U BigThing. How do we ensure the right environment?