Re: Why we allow CHECK constraint contradiction?

On 2018/10/10 16:28, Imai, Yoshikazu wrote:
> On Tue, Oct 9, 2018 at 6:01 PM, Amit Langote wrote:
>> I had wondered about it when developing the partitioning feature about
>> a couple of years ago and this is the response I'd gotten:
>>
>> https://www.postgresql.org/message-id/CA+TgmoaQABrsLQK4ms_4NiyavyJGS
>> -b6ZFkZBBNC+-P5DjJNFA(at)mail(dot)gmail(dot)com
>
> Thanks for tell me one of a discussion about this.
>
>> To summarize, the answer I got was that it's pointless to create defenses
>> against it inside the database. It's on the users to create the
>> constraints (or specify bounds) that are non-contradicting.
>
> I just thought it's kind to tell users whether users mistakenly specify
> bounds.
>
>
>> Interesting quotes from the above email:
>>
>> "If we allow partitioning on expressions, then it quickly becomes
>> altogether impossible to deduce anything useful - unless you can solve
>> the halting problem."
>>
>> "... This patch is supposed to be implementing partitioning, not
>> artificial intelligence."
>
> It takes little more time to completely understand this interesting quotes,
> but I guess I see that point.

The task of developing a contradiction proof module that takes an
arbitrary expression and returns whether it's self-contradictory seems
daunting to me. You may know of predtest.c in the optimizer directory as
one example of such a module, but if you look closely it's scope is fairly
limited; it works only if the input expressions contain variables of
certain types and operators that btree operator classes can handle, and
gives up on producing a proof otherwise.

On the other hand, the syntax of CHECK constraints allows a fairly wide
range of expressions to be specified, with expressions/values of arbitrary
types and operators with arbitrary semantics (not limited to
btree/ordering semantics, for example). It won't be a good enough
solution if it can provide the error for only a certain subset of
user-specified expressions, IMHO.

Thanks,
Amit