Semantic difference in division operator (SQLite vs. MySQL)

[wanteatfruit]

@Beliefuture Thank you for your hard work on this impactful project!

I have a quick question about semantic equivalence. If I understand correctly, the sqlite and mysql queries in the source-target query pair are intended to be equivalent?

I noticed a subtle semantic difference in the BIRD example. SQLite defaults to floor (integer) division for the / operator, while MySQL performs an implicit type conversion and returns a decimal, even though the operator is the same.

{
  "norm": "SELECT SUM(identifier) / NULLIF(COUNT(identifier), 0) FROM identifier WHERE SUBSTRING(identifier, 'value', 'value') BETWEEN '''value''' AND '''value'''",
  "sqlite": "SELECT SUM(height) / COUNT(id) FROM Player WHERE SUBSTR(birthday, 1, 4) BETWEEN '1990' AND '1995'",
  "mysql": "SELECT SUM(height) / COUNT(id) FROM Player WHERE SUBSTRING(birthday, 1, 4) BETWEEN '1990' AND '1995'",
  "id": "BIRD"
}

To illustrate, for the following minimal database instance:

CREATE TABLE Player (
    id INT,
    birthday VARCHAR(20),
    height INT
);

INSERT INTO Player (id, birthday, height) VALUES (0, '1995', 150);
INSERT INTO Player (id, birthday, height) VALUES (1, '1990', 151);

SQLite returns 150 while MySQL returns 150.5.

For the queries to be semantically equivalent (matching SQLite's integer division), I believe the MySQL query would need to use the DIV operator: SELECT SUM(height) DIV COUNT(id) FROM ...

Is this behavior intended, or is this a case where the translation could be more precise? Thanks!

[Beliefuture]

@wanteatfruit Hi! Thanks for your interest in our work! This behavior is intended, as the results differ only in precision. We relax the semantic equivalence considering the intrinsic implementations of different database systems, such as ignoring the precision and the displayed order of the returned results. However, I think the problem you pointed out is a promising direction that we keep on working to reflect upon how to ensure more strict and consistent equivalence among different systems.

[wanteatfruit]

@Beliefuture Thank you for the clarification! I'm wondering if this is more than just precision, but rather a difference in logically inequivalent data types? SQLite's query returns an INTEGER (from integer division), while MySQL's returns a DECIMAL (from decimal division). To get a logically equivalent integer type from MySQL, one would need to use DIV, which returns a BIGINT.

To reproduce:

-- SQLite

SELECT SUM(height) / COUNT(id), typeof(SUM(height)/COUNT(id)) FROM Player WHERE SUBSTR(birthday, 1, 4) BETWEEN '1990' AND '1995';

Output:
150|integer

-- MySQL

CREATE TEMPORARY TABLE TempTypeCheck AS
SELECT SUM(height) / COUNT(id) AS average_height
FROM Player 
WHERE SUBSTRING(birthday, 1, 4) BETWEEN '1990' AND '1995';

DESCRIBE TempTypeCheck;

Output:
+----------------+---------------+------+-----+---------+-------+
| Field          | Type          | Null | Key | Default | Extra |
+----------------+---------------+------+-----+---------+-------+
| average_height | decimal(36,4) | YES  |     | NULL    | NULL  |
+----------------+---------------+------+-----+---------+-------+

-- MySQL, using DIV operator

CREATE TEMPORARY TABLE TempTypeCheck AS
SELECT SUM(height) DIV COUNT(id) AS average_height
FROM Player 
WHERE SUBSTRING(birthday, 1, 4) BETWEEN '1990' AND '1995';

DESCRIBE TempTypeCheck;

+----------------+--------+------+-----+---------+-------+
| Field          | Type   | Null | Key | Default | Extra |
+----------------+--------+------+-----+---------+-------+
| average_height | bigint | YES  |     | NULL    | NULL  |
+----------------+--------+------+-----+---------+-------+

[Beliefuture]

Hi, the "precision" and the "data type" should refer to the same thing, as the inconsistency of the involved data types leads to the difference in precision, as you point out. Indeed, it is challenging to maintain a consistent data type due to the implementation differences.