Conditional Control is not quite Categorical Control

Abstract

It is often the intent of an algebraic specification of a data structure to include an aspect of control. For example, a stack is either empty or nonempty and one expects to be able to perform different actions based on this test. The question of whether an algebraic specification correctly expresses the intended control is related to a categorical question concerning whether the equalizer completion of the theory is distributive.

A many-sorted algebraic theory T is distributive whenever its (product preserving) equalizer completion, or equivalently the dual of the category of finitely presented algebras, ε(T) = (Set ^T_f )^op is a distributive category. This happens precisely when it has inhabited types and a weak form of “if...then...else” operator satisfying certain Horn clauses.

Of philosophical interest is the observation that if one drops the requirement that the types are inhabited the above correspondence fails. This means that the traditional method of adding control using conditional operators does not in general correspond to the categorical notion of control as given in distributive categories (or even locally predistributive categories).