I had just implemented type inference when I got smashed over the brain by Prolog. So now the Python code is in limbo because the Prolog implementation of Joy is blindingly elegant.
In Prolog, the Joy interpreter is also the Joy type inferencer.
The compiler (from Joy expressions to new Prolog rules) is five lines long.
Yes, there's a real connection between concatinative languages and logic languages. In some sense you can think of a concatinative logic language as Joy with the ability to push "unknown" values onto the stack, as well as a few constraint manipulatives. That's somewhat orthogonal, but it makes sense an interpreter for Joy would be quite compact in prolog.
Thanks for the links, I'll review your work later!
You might also like: http://conal.net/papers/compiling-to-categories/
He transforms Haskell to a point-free form that's suspiciously like Joy... ;-)