Interaction between Union downcasting and negation

[langston-barrett]

When updating to Souffle 2, I've encountered an type error that is a little counter-intuitive. Specifically, I'm able to "downcast" to one branch of a union in the body of a rule, but only if the "downcast" is not under a negation.

I can work around this by creating a "copy" rule with a relaxed type signature, and embedding that in the negation. The fact that this workaround works suggests that this isn't a fundamental limitation, perhaps it could be lifted?

The documentation on the type system doesn't really talk about this kind of downcasting, I'm happy to write a bit of documentation with this workaround if that seems helpful.

.type A <: symbol
.type B <: symbol
.type U = A | B

.decl b(x:B)
.decl u(x:U)
.decl r(x:U, y:U)
.decl s(x:B, y:number)

// Get rid of "no rules/facts defined" warning
.input b(IO="file", delimiter="\t", filename="b.csv")
.input r(IO="file", delimiter="\t", filename="r.csv")
.input s(IO="file", delimiter="\t", filename="s.csv")

u(x) :- b(x).  // downcast is fine
u(x) :- s(x, _).  // downcast is fine
u(x) :- r(x, y), s(y, _).  // downcast is fine
u(x) :- r(x, y), !s(y, _).  // Error: Atom's argument type is not a subtype of its declared type

// Try working around this with a "copy" relationship with a relaxed type...
.decl ss(x:U, y:number)
ss(x, y) :- s(x, y).
u(x) :- r(x, y), !ss(y, _).  // Works!

Error: Atom's argument type is not a subtype of its declared type in file type-test.dl at line 18
u(x) :- r(x, y), !s(y, _).  // Error: Atom's argument type is not a subtype of its declared type
--------------------^----------------------------------------------------------------------------
The argument's declared type is B in file type-test.dl at line 8
.decl s(x:B, y:number)
----------^------------
1 errors generated, evaluation aborted

This is with Souffle 2.0.1.

[b-scholz]

This issue has been raised by others as well (e.g. Neville).

We assume that in a rule, there are sources (e.g. positive predicates in the body) that generate information, and sinks (eg. variables in the head predicate, constraints, negation, etc.). Each of the sources / sinks have types associated and the question is whether there is a type clash or not.

Our approach is that (1) we search for the largest compatible sub type, and (2) check whether the sinks are super (or equal) types.

In this example,

.decl r(x:U, y:U)
.decl s(x:B, y:number)

u(x) :- r(x, y), !s(y, _).  // Error: Atom's argument type is not a subtype of its declared type

the source type of variable y is of type U caused by the variable binding r(x,y) in the first predicate. However, the sink type for the negation !s(y,_) is of type B. We have here a type clash because the relationship U <: B does not hold.

The notion of sinks and sources are important so that we avoid the wrong use of values in functors and constraints.

However, there could be one exception - negation.

The problem with negation is that one can argue that the sink type of negations can be in the extreme case unrelated since it checks the non-existence and does not perform any computations with its values. For example, two unrelated types would give a tautology. Let's assume we have the following program:

.type even <: number  // even numbers
.type odd <: number   // odd numbers

.decl e(n:number) 
...

.decl o(n:number)
...

.decl my_even(n:number)
my_even(x) :- e(x), !o(x), x <= 10.

The above code says that we are searching for even numbers that are not odd and are less than or equal to 10.

Our current type system would raise an issue because (1) the source type is even and the sink type is odd, and (2) even is not a subtype of odd, i.e., they are unrelated.

However, we could argue that !o(x) is a tautology because the intersection of even and odd numbers is assumed empty and hence permissible. We could further assume that no values are shared between the two domains, and the negation can be replaced by true.

Coming back to your example, you have an inversion, i.e., the source is a super-type of the sink. As a consequence, you may query values that are out of range in the negated predicate, i.e., the set of values U \ B.

The ultimate question is whether we either make negations more permissible or ask the users to be more precise in their modelling of the relation and its domains.

Instead of copying the relation, you could use a type cast:

u(x) :- r(x, y), !s(as(y, B), _).