[m-rev.] for post-commit review: check for terms containing distinct vars in one place

[Zoltan Somogyi]

On 2024-05-10 14:45 +10:00 AEST, "Peter Wang" <novalazy at gmail.com> wrote:
>> @@ -7828,6 +7828,12 @@ However, variables which are in the range of a functional dependency
>>  need not appear in the signature,
>>  since it is known that their bindings will be determined
>>  from the bindings of the variables in the domain.
>> + at c XXX What about a class with two fundeps: A -> B, and B -> A.
>> + at c Both A and B are in the range of a fundep.
>> + at c The above text seems to imply that it is ok for *neither* to appear
>> + at c in the signature.
>> + at c Should we replace "since it is known that their bindings will be determined"
>> + at c with "provided that their bindings are determined"?
>>  
> 
> How about:
> 
>     Without any functional dependencies, all variables in constraints
>     must appear in the signature of the predicate or function being
>     declared.
>     However, a variable [that appears] in the range of a functional
>     dependency does not need appear in the signature *if* the variables
>     in the domain of that functional dependency do appear in the
>     signature.

I don't think that is quite right. Given functional dependencies
A->B and B->C, it is ok for only A to appear in the signature.
C does not have to appear there, even though B is not in the signature either,
because B is nevertheless determined by a type var, A, that *is* in the
signature.

We need to avoid being both too strict (ruling out the chained application of
more than one fundep, even though it is allowed, as with the {A->B, B->C} example
above) and too loose (allowing circular reasoning of the form "assuming
we know A, we can prove we know A", as with the {A->B, B->A} example
in the original text). It is difficult to thread the needle between these two issues.
I can't think of a way to do that using simple and short text, because I think
that what we need to describe is forward chaining: starting with a given set of type vars
from the signature, and adding to that set  by applying fundeps *whose domain
is already in that set*.

I thought we can describe things using dags, along the lines of

(1) every fundep with N type vars in its domain and M in its range defines N*M directed edges.
with each one pointing from a var in the domain to one in the range, and (2) every var that
is not in the signature must be reachable from the vars that are in the signature.

But I can't come up with a correctness argument for this description, because I have the
nagging feeling that treating a fundep such as P,Q->R as two *independent* edges,
P->R and Q->R, loses significant information. In reality, fundeps are not really
collections of edges, they are *hyperedges*. But if we use that terminology, we lose
at least 95% of our audience.

Zoltan.