It's an interesting coincidence seeing this paper and talks about data flow, because I'm interested in applying typing to logic programming for a practical syst

It's an interesting coincidence seeing this paper and talks about data flow, because I'm interested in applying typing to logic programming for a practical system and also came to the conclusion that my type system needs to be aware of data flow. This is because variables in logic programming are usually individually bidirectional, but may not support all combinations. For instance, consider the logic relation "half(a, b) -> a = b/2 or b = 2a". If you pass in "a,_" it fills in the blank for "b" with the number which "a" is half of. If you pass in "_,b" it fills in the blank for "a" with the number that is half of "b". So, individually each "argument" to the relation is an input and an output. (What in C# would be called a "ref" arg, as opposed to an "out" arg or undecorated in arg.) However calling "half( _ , _ )" is not a valid use of this relation, and we would like the type checker to complain if it is used in this way. (What would one expect if both arguments are unset? Should it produce all pairs (n, 2n) in Z? Or perhaps all pairs ((float)0.5 n, (int)n)? An uncountably infinite set of pairs of Reals?) Clearly just marking individual arguments as "in" or "out" is not enough. The typing has to be more like "if I have this data I can get to that data" and "if I have this other data I can get to something else." I can't figure out a way to represent this in static types, but I believe it could be typed checked with dependent types. The examples with "select" near the beginning of the paper are not exactly the same thing, but are a similar problem and solution: data flow and the direction of the arrows matters.