public inbox for [email protected]  

help / color / mirror / Atom feed

From: Tom Lane <[email protected]>
To: James Coleman <[email protected]>
Cc: pgsql-hackers <[email protected]>
Subject: Re: Teach predtest about IS [NOT] <boolean> proofs
Date: Thu, 14 Dec 2023 16:38:17 -0500
Message-ID: <[email protected]> (raw)
In-Reply-To: <CAAaqYe-CGx7sEm1QRNaY=Pfti4KinLOPtgVr4LKoXY6wLa68Ag@mail.gmail.com>
References: <CAAaqYe8Bo4bf_i6qKj8KBsmHMYXhe3Xt6vOe3OBQnOaf3_XBWg@mail.gmail.com>
	<[email protected]>
	<CAAaqYe-CGx7sEm1QRNaY=Pfti4KinLOPtgVr4LKoXY6wLa68Ag@mail.gmail.com>

James Coleman <[email protected]> writes:
> On Wed, Dec 13, 2023 at 1:36 PM Tom Lane <[email protected]> wrote:
>> I don't have an objection in principle to adding more smarts to
>> predtest.c.  However, we should be wary of slowing down cases where
>> no BooleanTests are present to be optimized.  I wonder if it could
>> help to use a switch on nodeTag rather than a series of if(IsA())
>> tests.  (I'd be inclined to rewrite the inner if-then-else chains
>> as switches too, really.  You get some benefit from the compiler
>> noticing whether you've covered all the enum values.)

> I think I could take this on; would you prefer it as a patch in this
> series? Or as a new patch thread?

No, keep it in the same thread (and make a CF entry, if you didn't
already).  It might be best to make a series of 2 patches, first
just refactoring what's there per this discussion, and then a
second one to add BooleanTest logic.

>> I note you've actively broken the function's ability to cope with
>> NULL input pointers.  Maybe we don't need it to, but I'm not going
>> to accept a patch that just side-swipes that case without any
>> justification.

> [ all callers have previously used predicate_classify ]

OK, fair enough.  The checks for nulls are probably from ancient
habit, but I agree we could remove 'em here.

>> Perhaps, rather than hoping people will notice comments that are
>> potentially offscreen from what they're modifying, we should relocate
>> those comment paras to be adjacent to the relevant parts of the
>> function?

> Splitting up that block comment makes sense to me.

Done, let's make it so.

>> I've not gone through the patch in detail to see whether I believe
>> the proposed proof rules.  It would help to have more comments
>> justifying them.

> Most of them are sufficiently simple -- e.g., X IS TRUE implies X --
> that I don't think there's a lot to say in justification. In some
> cases I've noted the cases that force only strong or weak implication.

Yeah, it's the strong-vs-weak distinction that makes me cautious here.
One's high-school-algebra instinct for what's obviously true tends to
not think about NULL/UNKNOWN, and you do have to consider that.

>>> As noted in a TODO in the patch itself, I think it may be worth refactoring
>>> the test_predtest module to run the "x, y" case as well as the "y, x" case

>> I think that's actively undesirable.  It is not typically the case that
>> a proof rule for A => B also works in the other direction, so this would
>> encourage wasting cycles in the tests.  I fear it might also cause
>> confusion about which direction a proof rule is supposed to work in.

> That makes sense in the general case.

> Boolean expressions seem like a special case in that regard: (subject
> to what it looks like) would you be OK with a wrapping function that
> does both directions (with output that shows which direction is being
> tested) used only for the cases where we do want to check both
> directions?

Using a wrapper where appropriate would remove the inefficiency
concern, but I still worry whether it will promote confusion about
which direction we're proving things in.  You'll need to be very clear
about the labeling.

			regards, tom lane

view thread (3+ messages)

reply

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Reply to all the recipients using the --to and --cc options:
  reply via email

  To: [email protected]
  Cc: [email protected], [email protected]
  Subject: Re: Teach predtest about IS [NOT] <boolean> proofs
  In-Reply-To: <[email protected]>

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

This inbox is served by agora; see mirroring instructions
for how to clone and mirror all data and code used for this inbox