I like Inverse types! While it's not novel idea, this seems like a very concise implementation of it. Inverse types are also known as negative types (https://legacy.cs.indiana.edu/~sabry/papers/rational.pdf) or holes. This concept is what needed to make a concrete category for computation compact (highly recommend: http://arxiv.org/abs/0903.0340) and make the connection to how our physical universe actually works on a quantum level, with antiparticles performing backward computation. I'm pretty sure this model of computation of filling holes with inference would allow us to understand advantages of quantum computation much better.

Do you have any thoughts on HVM's SupGen for program synthesis? I would love to understand how interaction nets makes the notion of inverse types and filling holes more natural and efficient.