Prolog Instantiation Modes (and Python exit contexts)

I wrote a piece of Python code that does a funny little transform on the syntax tree of a function, and creates a new function that returns all the local variables defined at the exit point of the original function. When I explain this to someone, they ask "Why?" and I don't have a good answer, but usually I say that it's related to predicates in Prolog that have multiple calling modes. Which I'm going to try explaining here:

So, Prolog doesn't have functions, but it has something called "predicates" which are just as good. Predicates don't return a value, but any argument to a predicate can be an "output" variable, like a C reference parameter. Unlike C though, Prolog predicates often treat all of their parameters as outputs. For example, the function append can be used in (no less than) three different ways.

/* Appending, mode = input,input,output */
?- append([1,2,3],[4,5], X).
X = [1,2,3,4,5]

/* Trimming off a shared starting sequence, mode = input,output,input */
?- append([1,2,3],X,[1,2,3,4,5]).
X = [4,5]

/* Trimming off a shared ending sequence, mode = output,input,input */
?- append(X,[4,5],[1,2,3,4,5]).
X = [1,2,3]

Through these three operations seem very different from the perspective of an imperative language, in Prolog append can be defined in two simple lines. The intuition about Prolog is that the runtime doesn't think of variables so much as inputs and outputs, but as "things I already know" and "thinks I don't know yet".

We can translate Prolog's append into Python (at some loss of conciseness and functionality), and then use the Python macro mentioned above to check that the variable bindings at the end of the function maintain the invariant that we expect:

context = append_exit_context(None,[4,5],[1,2,3,4,5])
assert context['head'] + context['tail'] == context['result']

So, this is pretty cool, we can pretend that we're writing a predicate instead of a function, assigning computed values to variables when we're able to discover them, and then examine those bindings after running the predicate.

Of course, Prolog's append can also be called with the first two arguments uninstantiated, but that sort of magic is much harder to fit into Python.