Add operator for dividing interval by an interval

Hi,

I've open-coded $subject many times. I wonder if we should add at least a
restricted version of it.

I did find one past discussion of it on the list:
https://www.postgresql.org/message-id/24948.1259797531%40sss.pgh.pa.us

We have workarounds for it on the wiki:
https://wiki.postgresql.org/wiki/Working_with_Dates_and_Times_in_PostgreSQL#4._Multiplication_and_division_of_INTERVALS_is_under_development_and_discussion_at_this_time

There are plenty of search results with various, often quite wrong,
workarounds.

Of course, it's true that there are plenty intervals where division would not
result in clearly determinable result. E.g. '1 month'::interval / '1 day'::interval.

I think there's no clear result whenever the month component is non-zero,
although possibly there are some cases of using months that could be made work
(e.g. '12 months' / '1 month').

In the cases I have wanted interval division, I typically dealt with intervals
without the month component - typically the intervals are the result of
subtracting timestamps or such.

One typical usecase for me is to divide the total runtime of a benchmark by
the time taken for some portion of that (e.g. time spent waiting for IO).

What about an interval / interval -> double operator that errors out whenever
month is non-zero? As far as I can tell that would always be deterministic.

Greetings,

Andres Freund