Contradiction in Database [3]

MySQL Type Horrors may have been a more appropriate title. Although it is possible to demonstrate the problem in another DB system, I have deliberately chosen MySQL for this article because it literally lends itself to this kind of errors.


A small, but powerful example. Just by looking at this you may guess that this post may have something to do with case sensitivity, but as you will see the problems go much deeper. Here is the MySQL code for the example.

  T { rw integer
    , A  varchar(32)
    , B  blob
KEY {rw}

 T (rw,   A  ,   B  )
 { ( 1, 'ABC', 'ABC')
 , ( 2, 'abc', 'abc')

For the example I have created a fresh instance of MySQL (v 5.6.27) on Amazon RDS, using default settings. Note that the collation is case and accent insensitive.

select @@collation_database as cdb;



Let’s see what equals to what in table T.

select rw from T where A = B;


Therefore I conclude that:

A1 = B1 
A2 = B2

For simplicity, I am using “Excel notation” to refer to values at row-column intersections in the table.

To check for equality in column A, I simply count number of distinct values in the column.

select count(distinct A) as cnt_a from T;


There is only one distinct value in column A, therefore:

A1 = A2

Based on these two conclusions:

B1 = A1 = A2 = B2

How about column B?

select count(distinct B) as cnt_b from T;


Given that there are two distinct values in column B it is obvious that:

B1 <> B2

If I put this together, the following holds:

B1 = A1 = A2 = B2
B1 <> B2

Interestingly, both statements are true in table T. And we have the contradiction again. I can formalize this a bit. Given a proposition P stating that (B1 = B2), the following holds:

X,Y ∈ T
X = (B1 = A1 = A2 = B2)
Y = (B1 <> B2)

P = (B1 = B2)

⊢ X → P  T ⊢ X       ⊢ Y → ¬P  T ⊢ Y
-------------- (e1)  ---------------- (e2)
T ⊢ P                T ⊢ ¬P
------------------------------------- (i1)
T ⊢ (P ∧ ¬P)

A contradiction leads to nonsense — as previously demonstrated — so, a query that includes table T is likely to return a wrong result.

It Gets Worse

Take a good look at these three queries:

Query Result
select rw from T
where A = B;
select rw from T
where upper(A) = upper(B);
select rw from T
where lower(A) = lower(B);

This is a head-scratcher. What happens is weird: upper() and lower() do not work on blob, binary, and varbinary types. Instead of returning an error, they silently return the input value of the function. Duh. To be fair, it is in the manual; but really?


Time to revisit the definition and properties of equality.

Seems that it was Leibniz who rigorously defined equality; these four properties actually became theorems:

Property For any Must be True
Reflexive a a = a
Symmetry a,b if a = b then b = a
Transitive a,b,c if a = b and b = c then a = c
Substitution a,b,f(x) if a = b then f(a) = f(b)

Given the example, how are we doing some 300 years later?

Property Note
Reflexive ok
Symmetry ok
Transitive broken, first example
Substitution broken, second example


Using the small example — one table with three columns and two rows — I have managed to break two out of four properties of equality. A contradiction ensued. Not good, but this is the state of the industry.

Avoid using blobs, binary, and varbinary types for strings. Even if developers and DBAs are certain that they can handle nuances of an implicit type conversion, it is not likely that analysts will be able to do so. As time goes by, databases grow, and people come and go: errors from this kind of problems are inevitable.

Types and Typos in SQL [2]

In the previous post I demonstrated how small typos in SQL become large logical errors, and how a “proper” type system could help in preventing these. This time I explore how PostgreSQL’s enum data type can be leveraged to gain some data safety and prevent logical errors.

PostgreSQL’s ENUM

In PostgreSQL the enum data type offers some type safety, for example:

('1', '2', '3');

('1', '2', '3');

Enumerated values are labels, hence the quotation marks.


-- compare as default type
select '1' = '1' as bool;


-- compare as two same Enum types
select '1'::d1 = '1'::d1 as bool;


-- compare as two different Enum types
select '1'::d1 = '1'::d2 as bool;

ERROR:  operator does not exist: d1 = d2
LINE 1: select '1'::d1 = '1'::d2 as bool;

Again, this is a good error to get. But notice that the following still works:

select '1'::d1 = '1' as bool;


Why did this work? Take a look at this:

select '1' as x;


A label out of the context of an expression is of an unknown type. An implicit type cast (conversion) rule — in the previous example — converted the unknown type to the type d1 based on what was expected in the expression. If I explicitly specify the type of the second label, the error is back.

select '1'::d1 = '1'::text as bool;

ERROR:  operator does not exist: d1 = text
LINE 1: select '1'::d1 = '1'::text as bool;

The equals operator worked fine, as in the Haskell example from the previous post.

Functions and Operators

To make this a bit more realistic, I’ll use country codes for the next example; say cc2 is a domain of county codes.

('AU', 'BE', 'CA', 'FR', 'US');

First, let’s see what happens if I treat country codes as text (characters) and use a string operator, say concatenation.

SELECT 'AU'::char(2) || 'BE'::char(2) as ctr ;


No surprises here, all looks as expected. But, what does it mean to concatenate two country codes? Did these two countries merge? Did they sign some kind of political alliance? Maybe they signed a beer-drinking trade agreement; if so, how do we join?

The bottom line is that — logically — country code is not a string, but a type; hence concatenation does not make sense. In other words, this is a logical error.

However, if I treat country codes as the enum type:

SELECT ('AU'::cc2) || ('CA'::cc2) as ctr;

ERROR:  operator does not exist: cc2 || cc2
LINE 1: SELECT ('AU'::cc2) || ('CA'::cc2) as ctr;

In other words, there is no concatenation operator for this data type; and that is a good thing.
It is important to realise that in this case the type system prevented a logical error. Also, this error would be caught early — by a programmer or analyst while developing a query — and would not propagate into production nor reports.

More Goodies

It gets even better: consider two money-transaction tables, where one defines currency code as a character type, the other one as an enum; both have the same data. Check out the DDL with some data; I will just sketch it here:

currency = {'USD', 'CAD', 'EUR', 'GBP'}

T1 { TX  int  PK
   , AMT decimal(19,2)
   , CUR char(3)  -- <- focus here

T2 { TX  int  PK
   , AMT decimal(19,2)
   , CUR currency -- <- focus here

-- same data for both tables
T_  (TX,  AMT,  CUR )
   {( 1, 10.0, 'USD')
   ,( 2, 13.0, 'CAD')
   ,( 3,  9.0, 'EUR')

Note that in the sketch, the currency type is represented as a set of all possible values: logically a domain.

Now, consider an analyst wanting to count a number of transactions in Euros, but making a typo in the currency name. Two examples: the first one for currency treated as text, and the second one for the enumerated type.

-- T1.CUR defined as a string
SELECT count(1) as cnt
WHERE CUR = 'ERU' ; -- <- typo


-- T2.CUR defined as an enum
SELECT count(1) as cnt
WHERE CUR = 'ERU' ; -- <- typo

ERROR:  invalid input value for enum currency: "ERU"

In the second example the type check results in an error, which is much better than getting a wrong result. You may argue that the first result is OK too, in that case consider this:

-- foolish
SELECT sum(AMT) as amt_
     , max(CUR) as cur_
WHERE CUR like '%D' ;

amt_   cur_
23.00  USD

So, it added amounts of US and Canadian dollars, and reported the total in USD. Although this is the result of the foolish query, consider what happens when I try it on the table T2:

-- foolish
SELECT sum(AMT) as amt_
     , max(CUR) as cur_
WHERE CUR like '%D' ;

ERROR:  operator does not exist: currency ~~ unknown
LINE 4: WHERE CUR like '%D' ;

Much better, saved by the type system.


My argument is that some type safety is better than none. Hence, whenever there is a finite list of standardised codes, it is a good candidate for an enumerated type.

Unfortunately, all this reasoning does not apply to MySQL: although it does have data type enum, the scope is a singe-table column and its primary purpose is compact data storage.

Further Reading

By now it should be obvious that a type system has something to do with logic; after all, as seen in previous examples, it prevents logical errors.

Take a good look at this:

Γ ⊢ B → A   Δ ⊢ B 
----------------- (e1)
Γ,Δ ⊢ A

Γ ⊢ t:B → A   Δ ⊢ u:B 
--------------------- (e2)
Γ,Δ ⊢ t(u):A

The first rule (e1) is modus ponens in Gentzen's natural deduction; the second rule (e2) is function application in typed lambda calculus.

From this point on I can only "point a finger to the Moon" and recommend two -- nicely written and readable -- papers by P. Wadler: [Wad00] and [Wad14].

Have fun.

Types and Typos in SQL [1]

Almost anyone who has spent time working with SQL made — or had to fix — this kind of bug:

-- two tables (sketch)
users {id, user_name}

trans {id, amt, cur, tx_time, user_id}
-- query with a typo
SELECT user_name
     , tx_time
     , amt
     , cur
 FROM users as u
 JOIN trans as t ON = -- <- typo !!
WHERE user_name = 'jack' ;

Try the query, here is the DDL with some data; note the wrong result.

The naming convention uses a generic id propagated from the application's OO model and the default data type is usually integer. The typo joins transaction table on id, instead of user_id; very easy mistake to make and not so easy to catch.

When it does happen that the bug propagates to a production system, the usual response is to first blame a developer, then argue that the pair programming (or peer review) process is not working, then blame QA for not catching it, and eventually discuss naming conventions.

Although it is true that naming attributes user_id, tran_id instead of the generic id would help -- because the predicate would read u.user_id = t.user_id -- the problem is deeper. As it is often with SQL, the problem is not in users nor developers, but in the SQL itself; namely = is both: a type error and a logical error.

In order to demonstrate the concept I have to use something with a "proper" type system.

Haskell to the Rescue

Haskell's type system is based on Hindley-Milner type system, and if you have never heard of it, don't worry. All you have to know about it right now are just two things: 1) it is a beautiful thing, and 2) you want one.

Let's start with the definition of two new types, one for users and one for transactions. I am typing into Haskell's interactive environment, so "λ" is just a terminal prompt.

New Type

λ  newtype User = MkUser Int deriving (Eq, Show)

λ  newtype Tran = MkTran Int deriving (Eq, Show)

The type system can infer types, hence I can ask for types of constructors: MkUser and MkTran.

λ  :type MkUser 
MkUser :: Int -> User

λ  :type MkTran
MkTran :: Int -> Tran

MkUser is a function which takes an Int and returns a User; MkTran is a function which takes an Int and returns a Tran (transaction).

The deriving (Eq, Show) -- in new type definitions -- simply means to derive rules for equality and string-display from the underlying integer type. And right here -- at the very moment of a new type definition -- a question arises:

What does it mean for two instances of a type to be equal?

The answer seems simple, but in general it requires more thought.


Create two variables: u for a user, and t for a transaction; note that for both of them the value of the underlying integer type is 1.

λ  let u = MkUser 1

λ  let t = MkTran 1

Let's test for equality, first between terms of the same type.

λ  1 == 1

λ  u == u

λ  t == t

λ  MkUser 1 == MkUser 1

λ  MkUser 1 == MkUser 2

λ  MkTran 4 == MkTran 4

λ  MkTran 5 == MkTran 4

However, when different types -- user and transaction -- are compared, an error is raised.

λ  u == t

Couldn't match expected type `User' with actual type `Tran'

This is a good error to get. A user and a transaction are two different things hence can not be compared, regardless of the fact that both have the underlying integer value of 1.

Contrast this thinking to the previous SQL example, which was happy to join a user on a transaction just because 1=1. An error would be much better.

Functions & Operators

What about the type of the equals operator (==) ?

λ :type (==)
(==) :: Eq a => a -> a -> Bool

Equals is a function which takes two arguments of a same type a and returns Boolean, given that definition of equality for that type exists. In Haskell speak, the type a must be a member of the Eq class, but this is not about Haskell: it is the principle that matters.

How about addition? What will happen if I try to sum two users, or a user and a transaction, since both have an integer as the underlying data type?

Let's see the type of the addition operator.

λ :type (+)
(+) :: Num a => a -> a -> a

The addition is a function which takes two arguments of a numeric type a and returns a result of the type a.

By now it should be easy to understand what happens here:

λ u + u

No instance for (Num User) arising from a use of `+'

λ t + t

No instance for (Num Tran) arising from a use of `+'

λ t + u

Couldn't match expected type `Tran' with actual type `User'

Note that the error in the third example is different from errors in the first two examples. The last one complains about different types, while the first two essentially state that types User and Tran are not numeric.


If all this type-reasoning looks too complicated, consider the query:

SELECT (( +^3) - 22 as x
 FROM  users as u
 JOIN  trans as t ON = ( + 2)
WHERE = 1 ;


Take user number one, add transaction number three, raise the result to the power of three, subtract 22; and the result is: the meaning of life.

Hmm, so there may be a logical mistake somewhere in that query. Wouldn't it be nice to have a type system that prevents mistakes like this? Although SQL dialects do not offer much in terms of type safety, PostgreSQL's enum data type does.

Next time: PostgreSQL's enum and type safety.