Issues regarding relation predicates

[rlaiola]

Some tricky queries.

• Query 1

  -- Should throw an error or at least return an empty relation
  -- (with no schema) but returns R
  { t | ¬R(t) }

• Query 2

  -- Should return S but returns R
  { t | ¬R(t) ∧ S(t) }

• Query 3

  -- Should throw an error but returns R
  { t | ¬R(t) ∧ S(t) ∧ T(t) }

• Query 4

  -- Should return T but throws an error
  -- Error: schemas are not unifiable: types are different or size is different: [R.a : number, R.b : string, R.c : string] and [S.b : string, S.d : number]
  { t | ¬R(t) ∧ ¬S(t) ∧ T(t) }

[KPMGE]

• Query 1

-- Should throw an error or at least return an empty relation
-- (with no schema) but returns R
{ t | ¬R(t) }

Fixed on #11

Yes! In this case the query is unsafe. This case can be handled easily, but it's worth pointing out that there's no way to cover all possible unsafe TRC queries, and it's up to the user to make sure their safety.

[KPMGE]

• Query 2

-- Should return S but returns R
{ t | ¬R(t) ∧ S(t) }

This one should also return an error, as the ~R(t) makes it into an unsafe query, doesn't it?

[KPMGE]

• Query 3

-- Should throw an error but returns R
{ t | ¬R(t) ∧ S(t) ∧ T(t) }

With the fix #11 this query would actually fail, because the negation of a relation predicate makes it unsafe. Arguably though, one may question that setting a relation predicate twice should throw an error. I've implemented that on #12

now a query likes this throws an error:

{ t | S(t) ∧ T(t) }

[KPMGE]

• Query 4

-- Should return T but throws an error
-- Error: schemas are not unifiable: types are different or size is different: [R.a : number, R.b : string, R.c : string] and [S.b : string, S.d : number]
{ t | ¬R(t) ∧ ¬S(t) ∧ T(t) }

Same as in Query 2, this one is already covered after #11

[rlaiola]

• Query 3

-- Should throw an error but returns R
{ t | ¬R(t) ∧ S(t) ∧ T(t) }

With the fix #11 this query would actually fail, because the negation of a relation predicate makes it unsafe. Arguably though, one may question that setting a relation predicate twice should throw an error. I've implemented that on #12

now a query likes this throws an error:

{ t | S(t) ∧ T(t) }

Nice work!

Thinking ahead, perhaps the verification should include one more test: only one relation predicate per tuple variable. For instance, the expression below is valid and it would be a good addition in the near future.

{ t.a, p.d | R(t) ∧ S(p) ∧ t.b = p.b }

[KPMGE]

• Query 3

-- Should throw an error but returns R
{ t | ¬R(t) ∧ S(t) ∧ T(t) }

With the fix #11 this query would actually fail, because the negation of a relation predicate makes it unsafe. Arguably though, one may question that setting a relation predicate twice should throw an error. I've implemented that on #12 now a query likes this throws an error:

{ t | S(t) ∧ T(t) }

Nice work!

Thinking ahead, perhaps the verification should include one more test: only one relation predicate per tuple variable. For instance, the expression below is valid and it would be a good addition in the near future.

{ t.a, p.d | R(t) ∧ S(p) ∧ t.b = p.b }

Indeed! that's a good point, i don't think now it's the correct time to add this check, though. Imo this should be implemented only when support for multiple tuple variables is done.

I'll keep it in mind though, thanks for pointing out.