{'fraction_non_alphanumeric': 0.05922489082969432, 'fraction_numerical': 0.010687198345207998, 'mean_word_length': 3.8191194794406758, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 71, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
An Equational Formalism and Design Pattern for Functorial Data Integration

In this paper we present the first truly practical formalism for querying and integrating data using the functorial data model. In our formalism, database schemas and instances are multi-sorted equational theories of a certain form. Schemas denote categories, and instances denote their initial (term) algebras. The instances on a schema S form a category, S-Inst, and a morphism of schemas F : S ->T induces three adjoint data migration functors: Sigma_F : S-Inst ->T-Inst, defined by substitution along F, which has a right adjoint Delta_F : T-Inst ->S-Inst, which in turn has a right adjoint Pi_F : S-Inst ->T-Inst. We present a query language based on for/where/return syntax where each query denotes a sequence of data migration functors, a pushout-based design pattern for performing data integration using our formalism, and describe the implementation of the formalism in a tool we call FQL.


Introduction
In the functorial data model (Spivak, 2012), which originated in the late 1990s (Fleming et al., 2002), a database schema is a finitely presented category (Barr & Wells, 1995) (essentially, a directed multi-graph and path equality constraints) and a database instance on a schema S is a set-valued functor from S (essentially, a set of tables). The database instances on a schema S constitute a category, denoted S-Inst, and a functor (a.k.a schema mapping (Fagin et al., 2005)) F : S → T between schemas S and T induces three adjoint data migration functors: ∆ F : T -Inst → S-Inst, defined as ∆ F (I) := I • F, and the left and right adjoints to ∆ F , respectively: Σ F : S-Inst → T -Inst and Π F : S-Inst → T -Inst.
The Σ, ∆, Π data migration functors provide a category-theoretic alternative to the traditional relational operations for both querying data (relational algebra) and migrating / integrating data (the chase (Fagin et al., 2005)). The relative advantages and disadvantages of the functorial data model and the relational model are still being studied, but see (Spivak, 2012) for a discussion. In this paper we describe what we believe to be the first truly practical formalism for both query and data integration using (an extension of) the functorial data model, and use the formalism to describe a commonly occurring data integration design pattern by way of an example. We have implemented the formalism and the example in a prototype data integration system FQL, available at http://categoricaldata.net.
Hereafter we refer to the data model developed in this paper as "the functorial data model", and refer to the data model of (Fleming et al., 2002) as "the original functorial data model".
The mathematics behind our formalism are worked out in detail in (Schultz et al., 2016) using category theory. In this paper, our goal is to present our formalism and its implementation using only basic concepts from functional programming. In particular, we do not assume readers are familiar with category theory, although we do make "categorical remarks", and proofs are deferred to (Schultz et al., 2016). Our formalism is based entirely on multi-sorted equational logic: database schemas and instances are presented by equational theories of a certain kind. A schema mapping F : C → D is defined as a morphism of equational theories C and D, and the Σ F data migration is defined as substitution along F. The conditions we impose on our equational theories guarantee that Σ F has a right adjoint, ∆ F , which in turn has a right adjoint, Π F . Getting the conditions right is tricky: even slight changes to our conditions result in at least one of Σ, ∆, Π no longer existing, or losing its adjointness property. We can recover the original functorial data model of (Fleming et al., 2002), and the extension of the original model in (Spivak & Wisnesky, 2015), by imposing restrictions on our equational theories. Our query language, which is a generalization of for/where/return queries (Abiteboul et al., 1995), corresponds semantically to combinations of Σ, ∆, Π operations and generalizes the idea from relational database theory that conjunctive queries can be represented as "frozen" instances (Abiteboul et al., 1995). Our design pattern for data integration is based on a categorical construction called a "pushout" (Barr & Wells, 1995).

Related Work
Our motivation for extending the original functorial data model (Fleming et al., 2002) is that the original model is difficult to use for data integration: the original model represents database instances as set-valued functors, but most constructions on set-valued functors are only defined up to unique isomorphism, and in the context of data integration, we must distinguish two kinds of values in a database: atomic values such as strings and integers that must be preserved by morphisms (e.g., Bill), and meaningless identifiers that need not be preserved (e.g., an auto-generated ID). (In contexts outside of data integration, such as relational query, there may not be a need to distinguish two types of values.) For example, the following situation, which holds in the original model, is untenable for data integration: 3 Several approaches to this problem have been proposed, including (Johnson et al., 2002) and (Spivak & Wisnesky, 2015). The latter paper also gives (partial) translations between the ∆, Σ, Π data migration functors and the σ , ×, ∪, π fragment of relational algebra.
Pushouts, the basis of our data integration design pattern, are investigated for data integration purposes in (Alagic & Bernstein, 2001). In that paper, the authors use the theory of institutions (Goguen & Burstall, 1984) to describe a design pattern for data integration. The functorial data model is an institution, but their work differs from ours in key respects. First, they are primarily concerned with the ∆, rather than Σ, data migration functor (they call our ∆ functor "Db" in their paper), because ∆ exists in all institutions. They recognize that pushouts (what they call "schema joins") are a canonical way of obtaining integrated schemas, and that not all institutions have pushouts of schemas (the functorial data model does). Their main theorem is that in any institution (including ours), the ∆ functor can be used to migrate the data on a pushout schema back to the source schemas. Our design pattern uses the Σ functor -the left adjoint to ∆, which exists in the functorial data model but not in all institutions -to go the other way: pushing data from source schemas to the integrated schema. See (Goguen, 2004) for more information about data integration in arbitrary institutions. In the more general setting of algebraic specification, pushouts have received considerable attention as a means to integrate specifications (Blum et al., 1987).

Outline
This paper is divided into four sections. In Section 2 we review multi-sorted equational logic. In Section 3 we describe how we use equational theories to define schemas, instances, and the other artifacts necessary to perform data integration and query. In Section 4 we describe how our formalism is implemented in the FQL tool. In Section 5 we describe our design pattern for functorial data integration and include an extended example. We think of this paper as defining a reference implementation of (Schultz et al., 2016) which a motivated reader could use to re-implement the FQL tool and its library of examples.

Multi-sorted Equational Logic
In this section we review standard material on multi-sorted equational logic, following the exposition in (Mitchell, 1996). Theories in multi-sorted equational logic are also called "algebraic theories", as well as "Lawvere theories" and "product theories". We will use these phrases interchangeably. For a category-theoretic study of such theories, see (Adámek et al., 2011). Reader familiars with equational logic can safely skim or skip this section. To save space, we will use the phrase "theory", rather than "multi-sorted equational theory", in this section.

Syntax
A signature Sig consists of: 1. A set Sorts whose elements are called sorts, 2. A set Symbols of pairs ( f , s 1 × . . . × s k → s) with s 1 , . . . , s k , s ∈ Sorts and no f occurring in two distinct pairs. We write f : X instead of ( f , X) ∈ Symbols. When k = 0, we may call f a constant symbol and write f : s instead of f : → s. Otherwise, we may call f a function symbol.
We assume we have some infinite set V := {v 1 , v 2 , . . . }, whose elements we call variables and which are assumed to be distinct from any sort or symbol we ever consider. A context Γ is defined as a finite set of variable-sort pairs, with no variable given more than one sort: When the sorts s 1 , . . . , s k can be inferred, we may write a context as {v 1 , . . . , v k }. We may write {v 1 : s, . . . , v k : s} as {v 1 , . . . , v k : s}. We may write Γ∪{v : s} as Γ, v : s. We inductively define the set Terms s (Sig, Γ) of terms of sort s over signature Sig and context Γ as: We refer to Terms s (Sig, / 0) as the set of ground terms of sort s. We will write Terms(Sig, Γ) for the set of all terms in context Γ, i.e., s Terms s (Sig, Γ). Substitution of a term t for a variable v in a term e is written as e[v → t] and is recursively defined as usual: We will only make use of substitutions that are sort-preserving; i.e., to consider e[v → t], we require e ∈ Terms(Sig, Γ) for some Γ such that v : s ∈ Γ and t ∈ Terms s (Sig, Γ). We An equation over Sig is a formula ∀Γ. t 1 = t 2 : s with t 1 ,t 2 ∈ Terms s (Sig, Γ); we will omit the : s when it is not relevant. A theory is a pair of a signature and a set of equations over that signature. In this paper, we will make use of the following theory we call Type: Equations := {length(nil) = zero, ∀c : Char, s : String. length(cons(c, s)) = succ(length(s))} We will abbreviate zero as 0 and succ n (zero) as n. We will write e.g. Bill for cons (B, cons(I, cons(L, cons(L, nil))).

Fig. 2. The Multi-sorted Equational Theory Type
Associated with a theory T h is a binary relation between (not necessarily ground) terms, called provable equality. We write T h ∀Γ. t = t : s to indicate that the theory T h proves that terms t,t ∈ Terms s (Sig, Γ) are equal according to the usual rules of multi-sorted equational logic. From these rules it follows that provable equality is the smallest equivalence relation on terms that is a congruence, closed under substitution, closed under adding variables to contexts, and contains the equations of T h. In general, provable equality is semi-decidable (Bachmair et al., 1989). Formally, T h is defined by the inference rules:

Fig. 3. Inference Rules for Multi-sorted Equational Logic
A morphism of signatures F : Sig 1 → Sig 2 consists of: • a function F from sorts in Sig 1 to sorts in Sig 2 , and • a function F from function symbols f : s 1 × . . . × s n → s in Sig 1 to terms in The function F taking function symbols to terms can be extended to take terms to terms: When we are defining the action of a specific F on a specific f : s 1 × . . . × s n → s, we may write F( f ) := ∀v 1 , . . . , v n . φ , where φ may contain v 1 , . . . , v n , to make clear the variables we are using. A morphism of theories F : T h 1 → T h 2 is a morphism of signatures that preserves provable equality of terms: T h 1 ∀v 1 : s 1 , . . . v n : s n . t 1 = t 2 : s ⇒ T h 2 ∀v 1 : F(s 1 ), . . . , v n : F(s n ). F(t 1 ) = F(t 2 ) : F(s) In the theory Type (Figure 2), any permutation of A, B, . . . Z induces a morphism Type → Type, for example. Although morphisms of signatures are commonly used in the categorical approach to logic (Adámek et al., 2011), such morphisms do not appear to be as commonly used in the traditional set-theoretic approach to logic. Checking that a morphism of signatures is a morphism of theories reduces to checking provable equality of terms and hence is semi-decidable.
Remark. Multi-sorted equational logic differs from single-sorted logic by allowing empty sorts (sorts that have no ground terms). Empty sorts are necessary to formalize the functorial data model. For the theoretical development, this difference between multisorted and single-sorted logic can be safely ignored. But the fact that many algorithms are based on single-sorted logic means that care is required when implementing our formalism. For example, certain theorem proving methods based on Knuth-Bendix completion (Knuth & Bendix, 1970) ostensibly require a ground term of every sort.
Categorical Remark. From a theory T h we form a cartesian multi-category (Barr & Wells, 1995) T h as follows. The objects of T h are the sorts of T h. The elements of the hom-set s 1 , . . . , s k → s of T h are equivalence classes of terms of sort s in context {v 1 : s 1 , . . . , v : s k }, modulo the provable equality relation T h . Composition is defined by substitution. A morphism of theories F : T h 1 → T h 2 denotes a functor F : T h 1 → T h 2 . Although cartesian multi-categories are the most direct categorical semantics for theories, it many cases it is technically more convenient to work with product categories instead. Every cartesian multi-category is equivalent to a product category, so in our categorical remarks we may conflate product categories and cartesian multi-categories depending on which is more convenient. For details, see (Schultz et al., 2016).

Semantics
An algebra A over a signature Sig consists of: • a set of carriers A(s) for each sort s, and Let Γ := {v 1 : s 1 , . . . , v n : s n } be a context. An A-environment η for Γ associates each v i with an element of A(s i ). The meaning of a term in Terms(Sig, Γ) relative to A-environment η for Γ is recursively defined as: An algebra A over a signature Sig is a model of a theory T h on Sig when T h ∀Γ. t = t : s implies A t η = A t η for all terms t,t ∈ Terms s (Sig, Γ) and A-environments η for Γ. Deduction in multi-sorted equational logic is sound and complete: two terms t,t are provably equal in a theory T h if and only if t and t denote the same element in every model of T h. One model of the theory Type ( Figure 2) has carriers consisting of the natural numbers, the 26 character English alphabet, and all strings over the English alphabet. Another model of Type uses natural numbers modulo four as the carrier for Nat. From a signature Sig we form its term algebra Sig , a process called saturation, as follows. The carrier set Sig (s) is defined as the set of ground terms of sort s. The function Sig ( f ) for f : s 1 × . . . s k → s is defined as the function t 1 , . . .t n → f (t 1 , . . . ,t n ). From a theory T h on Sig we define its term model T h to be the quotient of Sig by the equivalence relation T h . In other words, the carrier set T h (s) is defined as the set of equivalence classes of ground terms of sort s that are provably equal under T h. The function T h ( f ) is Sig ( f ) lifted to operate on equivalence classes of terms. To represent T h on a computer, or to write down T h succinctly, we must choose a representative for each equivalence class of terms; this detail can be safely ignored for now, but we will return to it in the implementation section 4. When we must choose representatives for T h , we will write n f T h (e) to indicate the unique e ∈ T h such that T h e = e (i.e., the normal form for e in T h). For example, the term model of the algebraic theory Type (Figure 2  A morphism of algebras (also called a homomorphism (Mitchell, 1996)) h : A → B on a signature Sig is a family of functions h(s) : A(s) → B(s) indexed by sorts s such that: h(s)(A( f )(a 1 , . . . , a n )) = B( f )(h(s 1 )(a 1 ), . . . , h(s n )(a n )) for every symbol f : s 1 × . . . × s n → s and a i ∈ A(s i ). We may abbreviate h(s)(a) as h(a) when s can be inferred. The term algebras for a signature Sig are initial among all Sigalgebras: there is a unique morphism from the term algebra to any other Sig-algebra. Similarly, the term models are initial among all models. It is because of initiality that in many applications of equational logic to functional programming, such as algebraic datatypes (Mitchell, 1996), the intended meaning of a theory is its term model.
Categorical Remark. Models of a theory T h correspond to functors T h → Set, and the term model construction yields a set-valued functor. That is, an algebraic theory T h denotes a cartesian multi-category, T h , and the term model construction yields functor T h → Set. At the risk of confusion, we will write also write T h for the functor T h → Set; hence, we have T h : T h → Set. Morphisms between models correspond to natural transformations. A morphism of theories F : T h 1 → T h 2 induces a functor, F : T h 1 → T h 2 between the cartesian multi-categories T h 1 and T h 2 , as well as a natural transformation between the set-valued functors T h 1 and T h 2 .

An Equational Formalism for Functorial Data Migration
In this section we describe how to use multi-sorted equational theories for functorial data migration. To summarize, we proceed as follows; each of these steps is described in detail in this section. First, we fix an arbitrary multi-sorted equational theory Ty to serve as an ambient type-side or "background theory" against which we will develop our formalism. We say that the sorts in Ty are types. For example, we may define Ty to contain a sort Nat; function symbols 0, 1, +×; and equations such as 0 + x = x. A schema S is an equational theory that extends Ty with new sorts (which we call entities), for example Person; unary function symbols between entities (which we call foreign keys) and from entities to types (which we call attributes), for example, f ather : Person → Person and age : Person → Nat; and additional equations. An instance I on S is an equational theory that extends S with 0-ary constant symbols (which we call generators), such as Bill and Bob; as well as additional equations, such as f ather(Bill) = Bob. The intended meaning of I is its term model (i.e., the canonical model built from I-equivalence classes of terms). Morphisms of schemas and instances are defined as mappings of sorts to sorts and function symbols to (open) terms that preserves entailment, that is, h : C → D exactly when C p = q implies D h(p) = h(q). Our query language is based on a generalization of for-where-return notation, and generalizes the idea from relational database theory that conjunctive queries can be represented as "frozen" instances (Abiteboul et al., 1995).

Type-sides, Schemas, Instances, Mappings, and Transforms
Our formalism begins by fixing a specific multi-sorted equational theory Ty which will be called the type-side of the formalism. The sorts in Ty are called types. The type-side is meant to represent the computational context within which our formalism will be de-ployed. For example, a type-side for SQL would contain sorts such as VARCHAR and INTEGER and functions such as LENGTH : VARCHAR → INTEGER; a type-side for SK combinator calculus (a Turing-complete formalism) would contain a sort o, constants S, K : o, a function symbol · : o → o, and equations K · x · y = x and S · x · y · z = x · z · (y · z). Note that simply-typed, first-order functional programs can be expressed using multisorted equational theories; in fact, using a functional program as a type-side is a "best-case scenario" for the automated reasoning required to implement our formalism; see Section 4 for details. We will also abbreviate "multi-sorted equational theory" as "theory" in the remainder of this section.
A schema S (on type-side Ty) is a theory extending Ty. If s is a sort in S but not in Ty, we say that s is an entity; otherwise, that s is a type. S must meet the following conditions: • If ∀Γ. t 1 = t 2 is in S but not in Ty, then Γ = {v : s} where s is an entity.
• If f : s 1 × . . . × s n → s is in S but not Ty, then n = 1 and s 1 is an entity. If s is an entity we say that f is a foreign key; otherwise, we say that f is an attribute.
In other words, every equation in a schema will have one of two forms: ∀v : t. v.p = v.p : t , where t and t are entities and p and p are sequences of foreign keys, or some combination of type-side functions applied to attributes, for example ∀v : t. v.p 1 .att 1 + v.p 2 .att 2 = v.att : t where t is an entity and t is a type. Due to these restrictions, S admits three sub-theories: the type-side (or part) of S, namely, Ty; the entity-side of S, namely, the restriction of S to entities (written S E ); and the attribute side of S, namely, the restriction of S to attributes (written S A ). We can also consider the entities and attributes together (S EA ), and the attributes and type side together (S AT ). A morphism of schemas, or schema mapping, S 1 → S 2 on type-side Ty is a morphism of theories S 1 → S 2 that is the identity on Ty. An example schema Emp on type-side Type ( Figure 2) is in Figure 5 below. We may draw the entity and attribute part of the schema in a graphical notation, with every sort represented as a dot, and the foreign keys and attributes represented as edges. In schema Emp ( Figure 5), Emp and Dept are sorts (entities) of employees and departments, respectively; mgr takes an employee to their manager; sec takes a department to its secretary; and wrk takes an employee to the department they work in. The equations are data integrity constraints saying that managers work in the same department as their employees, that secretaries work for the department they are the secretary for, and that the management hierarchy is two levels deep. The first restriction on schemas rules out products of entities (for example, using a symbol CommonBoss : Emp × Emp → Emp), and the second restriction on schemas rules out the use of types as domains (for example, using a symbol EmpNumber : Nat → Emp). Without these restrictions, the existence and adjointness of the Σ, ∆, Π functors that we will later define cannot be guaranteed.
An instance I on schema S is a theory extending S, meeting the following conditions: • If s is a sort in I, then s is a sort in S.
That is, an instance only adds 0-ary symbols and ground equations. Mirroring a similar practice in relational database theory, we use the phrase skolem term to refer a term in an instance that is not provably equal to a term entirely from the type-side, but whose sort is a type. Although skolem terms are very natural in database theory, skolem terms wreak havoc in the theory of algebraic datatypes, where their existence typically implies an error in a datatype specification that causes computation to get "stuck" (Mitchell, 1996).
Similarly to how schemas admit sub-theories for entity, attribute, and type-sides, an instance I contains sub-theories for entities (I E ), attributes (I A ), and types (I T ). Note that I T may not be the ambient type side Ty, because I can declare new constant symbols whose sorts are types (so-called skolem variables), as well as additional equations; for example, infinity : Nat and succ(infinity) = infinity. A morphism of instances, or transform, h : I 1 → I 2 is a morphism of theories I 1 → I 2 that is the identity on S. (The requirement of identity on S rules out the "attribute problem" from figure 1).
The intended meaning of an instance I is its term model, I . In practice, the term model I will often have an infinite type side, but I EA will be finite. Therefore, our implementation computes I EA , as well as an instance talg(I) called the type-algebra 1 for I. The type-algebra talg(I) is an instance on the empty schema over I T . For every attribute att : s → t in S, and every term e ∈ I E (s), the type-algebra contains a generator e.att : t. We call these generators observables because they correspond to type-valued observations one can make about an entity. Observables have the form e. f k 1 . . . . . f k n .att; i.e., have a 0ary constant symbol as a head, followed by a possibly empty list of foreign keys, followed by an attribute. We define the function trans : Terms t (I, / 0) → talg(I), for every type (nonentity) sort t, as: Note that talg(I) does not present I T (the restriction of I to types), rather, talg(I) presents I T (i.e., the skolem terms of I and their relationships).
We visually present term models using a set of tables, with one table per entity, with an ID column corresponding to the carrier set. Sometimes, we will present the type-algebra as well. An instance on the Emp schema, and its denotation, is shown in Figure 6.
In many cases, we would like for an instance I to be a conservative extension of its schema S, meaning that for all terms t,t ∈ Terms s (S, Γ), I ∀Γ. t = t : s if and only if S ∀Γ. t = t : s. (Similarly, we may also want schemas to conservatively extend their typesides.) For example, Emp Al = Carl : String, but there is an Emp-instance I for which I Al = Carl : String. In the context of "deductive databases" (Abiteboul et al., 1995) (databases that are represented intensionally, as theories, rather than extensionally, as tables) such as our formalism, non-conservativity is usually regarded as non-desireable (Ghilardi et al., 2006), although nothing in our formalism requires conservativity. Checking for conservativity is decidable for the description logic underlying OWL (Ghilardi et al., 2006), but not decidable for multi-sorted equational logic (and hence our formalism), and not decidable for the formalism of embedded dependencies (Fagin et al., 2005) that underlies much work on relational data integration (conservativity is checked during the chase process). In Section 4.3 we give a simple algorithm that soundly approximates conservativity. Note that the ∆ and Π migration functors preserve the conservative extension property, but Σ does not; hence, one may want to be careful when using Σ. (More pedantically, ∆ and Π preserve type-algebras, but Σ does not.)

Remark.
There is a precise sense in which our definition of transform corresponds to the definition of database homomorphism in relational database theory. Recall (Abiteboul et al., 1995) that in database theory a schema is a triple (dom, null, R), where dom is a set (called the domain), null is a set disjoint from dom, (called the labelled nulls), and R is a set of relation names and arities; an instance I is a set of relations over dom ∪ null, indexed by R, of appropriate arity; and a homomorphism h : I 1 → I 2 is a function h : dom ∪ null → dom ∪ null that is constant on dom and such that (c 1 , . . . , c n ) ∈ I 1 (R) implies (h(c 1 ), . . . , h(c n )) ∈ I 2 (R) for every R of arity n. If we interpret a term model I as a relational instance by considering every skolem term in I to be a labelled null and over non-skolem term to be a domain value, then a transform of instances in our formalism induces a homomorphism of the encoded relational instances. dom is playing the role of a free (equation-less), discrete (function-less) type-side.
Categorical Remark. By forgetting the entity/attribute distinction, we can consider a schema S as a single algebraic theory,Ŝ; the cartesian multi-category Ŝ is called the collage of S. A schema mapping F : S → T is then a functor between collages Ŝ → T that is the identity on Ty. More pedantically, a schema S is a profunctor S : S E op × Ty → Set which preserves products in Ty . The observables from an entity e ∈ S E to type ty ∈ Ty are given by S (e,ty). A schema mapping F : S → T denotes a functor F E :

Functorial Data Migration
We are now in a position to define the data migration functors. We first fix a type-side (multi-sorted equational theory), Ty. The following are proved in (Schultz et al., 2016): • The schemas on Ty and their mappings form a category.
• The instances on a schema S and their transforms form a category, S-Inst.
• The models of S and their homomorphisms obtained by applying to S-Inst form a category, S-Inst , which is equivalent, but not equal to, S-Inst. Although Σ F and ∆ F are canonically defined, their adjoints are only defined up to unique isomorphism. The canonically defined migration functors enjoy properties that the other data migration functors do not, such as Σ F (Σ G (I)) = Σ F•G (I) and ∆ F ( ∆ G (I)) = ∆ F•G (I) (for the other functors, these are not equalities, but unique isomorphisms).

Uber-flower Queries
It is possible to form a query language directly from schema mappings. This is the approach we took in (Spivak & Wisnesky, 2015), where a query is defined to be a triple of schema Suitable conditions on F, G, H guarantee closure under composition, computability using relational algebra, and other properties desirable in a query language. In practice, however, we found this query language to be extremely challenging to program. Having to specify entire schema mappings is onerous; it is difficult to know how to use the data migration functors to accomplish any particular task without a thorough understanding of category theory; and as a kind of "join all", Π is expensive to compute. Hence, in (Schultz et al., 2016) we developed a new syntax, which we call uber-flower syntax, because it is a generalization of flwr (for-let-wherereturn) syntax (a.k.a select-from-where syntax, comprehension syntax). We have found uber-flower syntax to be more concise, easier to program, and easier to implement than the language based on triples of schema mappings in (Spivak & Wisnesky, 2015).
A conjunctive uber-flower Q : S → T , where S and T are schemas on the same type-side, induces a data migration eval(Q) : In fact, all data migrations of the form ∆ • Π can be expressed as the eval of a conjunctive uber-flower, and all migrations of the form ∆ • Σ can be expressed as the coeval of a conjunctive uberflower. In Sections 3.3.4 and 3.3.5 we describe the correspondence between uber-flowers and data migration functors in detail.
A tableau (Abiteboul et al., 1995) over a schema S is a pair of: • a context over S, called the for clause, f r and • a set of equations between terms in Terms(S, f r), called the where clause wh.
Associated with a tableau over S is a canonical S-instance, called the "frozen" instance (Abiteboul et al., 1995). In our formalism, a tableau trivially becomes an instance by a validitypreserving process called Herbrandization (the dual of the satisfiability-preserving Skolemization process) that "freezes" variables into fresh constant symbols. For example, we can consider the tableau ({v 1 : Emp, v 2 : Dept}, v 1 .wrk = v 2 , v 1 .ename = Peter) to be an Empinstance with generators v 1 , v 2 . In this paper, we may silently pass between a tableau and its frozen instance.
A conjunctive uber-flower S → T consists of, for each entity t ∈ T : • a tableau ( f r t , wh t ) and, • for each attribute att : t → t , a term [att] in Terms t (S, f r t ), called the return clause for att, and • for each foreign key f k : t → t , a transform [ f k] from the tableau for t to the tableau for t, called the keys clause for f k, • such that an equality-preservation condition holds. We defer a description of this condition until the end of this section.
We prefer to use f r t , wh t , [att], [ f k] notation when discussing a single uber-flower. When we are discussing many queries Q 1 , . . . , Q n , we will write Q k (t), Q k (att), Q k ( f k) to indicate ( f r t , wh t ), [att], and [ f k], respectively, for Q k .
We require that the for clauses in an uber-flower only bind variables to entities, not to types (e.g., v : Person is allowed, but v : Nat is not). While not strictly necessary, there are two reasons for preferring this restriction. First, in practice, types will almost always be infinite, so the data migrations induced by a non-restricted uber-flower will often return infinite instances. Second, the restriction ensures that the induced data migrations are domain independent (Abiteboul et al., 1995), allowing some evaluations of uber-flowers to be computed using relational algebra (Spivak & Wisnesky, 2015). Semantically, this restriction means that evaluations of conjunctive uber-flowers correspond to migrations of the form ∆ G •Π F , where F is surjective on attributes, a condition described in Section 3.3.4.
An uber-flower is a conjunctive uber-flower which contains multiple for-where-returnkeys clauses per target entity. These uber-flowers induce a single data migration of the form Barr & Wells, 1995), and can be thought of as our formalism's equivalent of "unions of conjunctive queries". For simplicity, we will stick to exposition involving conjunctive uber-flowers, and in the rest of this paper, we may use the word "query" to mean "conjunctive uber-flower". We now present in Figure 10 an example query, from our Emp schema to our Emp schema ( Figure 5), that when evaluated makes each employee their own boss and appends their old boss's name to their name. Note that in this query, Dept is copied over unchanged; only Emp changes.  Remark. Because boolean algebra can be equationally axiomatized, our conjunctive uber-flowers can express queries that might not be considered conjunctive in certain relational settings. For example, when our type side contains boolean algebra (Figure 11), our conjunctive uber-flowers can express queries such as Q(R) := {x ∈ R | P(x) ∨ ¬P(x) = }. Because instances may contain skolem terms of type Bool, i.e., terms which are not provably equal to or ⊥, in general Q(R) need not equal R. Similarly, our conjunctive uber-flowers can express non-computable queries whenever a type side contains an equational theory that is Turing-complete. In such cases, the type side will not have a decidable equality relation and the theorem proving methods employed by the implementation (Section 4) may diverge.
Categorical Remark. Let Q : S → T be a conjunctive uber-flower over type-side Ty. Then Q denotes a bimodule (Schultz et al., 2016), i.e., a functor Q : Ŝ op → S-Inst such that Q (t) = y(t) for every t ∈ Ty , where y : Ŝ op → S-Inst is the yoneda embedding.

Verification Conditions for Query Well-formedness
Let Q : S → T be a conjunctive uber-flower. A path in T , p : t 0 → t n := f k 1 . . . . . f k n is a sequence of foreign keys, f k n : t n−1 → t n , and we write [p] to indicate the substitution [ f k 1 ] • . . . • [ f k n ] taking each v : s ∈ f r t n to some term in Terms s (S, f r t 0 ) (when n = 0 this is the identity substitution on f r t 0 ). To verify that Q is well-formed, for every equation in T we must verify an induced set of equations on S. There are two kinds of equations in T that we must consider. One kind of equation is equality at entities of paths with a shared head variable in a singleton entity context: For each variable u : s ∈ f r t , we must verify the following: The other kind of equation is equality at types of arbitrary terms where paths share head variables in a singleton entity context, for example: Here we must check, for example: In Figure 10, φ ψ means that equation φ ∈ T generates verification condition ψ. Generating verification conditions for a (not necessarily conjunctive) uber-flower is a slight generalization of the process described above.

Morphisms of Queries
Let Q 1 , Q 2 : S → T be conjunctive uber-flowers. For every foreign key f k : such that for every foreign key f k : t → t , and every v ∈ f r 1 t , and for every attribute att : t → t , h induces a transform eval(h) : eval(Q 2 )(I) → eval(Q 1 )(I) for each S-instance I (in this way, our conjunctive uber-flowers are similar to relational conjunctive queries) and a transform coeval(h) : coeval(Q 1 )(J) → coeval(Q 2 )(J) for each T -instance J.

Composing Queries
Let Q 1 : A → B and Q 2 : B → C be conjunctive uber-flowers on the same type-side. We define the uber-flower Q 2 • Q 1 : A → C as follows. For every entity c ∈ C, • We define (the frozen A-instance of) the for and where clause at c of Q 2 • Q 1 to be the frozen A-instance that is obtained by applying coeval(Q 1 ) : B-Inst → A-Inst to the frozen B-instance for c in Q 2 : • Similarly, the transform associated with a foreign key f k : c → c ∈ C is: • To define the term associated with an attribute att : c → c ∈ C we first define the instance y(c ) (a so-called "representable" (Barr & Wells, 1995) instance) to be the Binstance with a single generator v : c . We then define a transform / substitution from y(c ) to the frozen B-instance for c in Q 2 , namely, h : y(c ) → Q 2 (c) := v → Q 2 (att). Finally, we define: (Not necessarily conjunctive) uber-flowers also compose (in a way similar to how polynomial functors compose), but describing their composition is significantly harder, and we omit a description here.

Converting Data Migrations to Queries
Let F : S → T be a schema mapping on a type side Ty. In this section we define two conjunctive uber-flowers, Q F : S → T and Q F : T → S such that: We now describe Q F and Q F : • The frozen instance (for/where clause) for Q F : S → T at entity t ∈ T is defined to be ∆ F (y(t)), where y(t) is the instance with a single generator {v t : t}. For each foreign key f k : t → t ∈ T , we define the transform Q F ( f k) : . For each attribute att : t → t ∈ T , v t .att ∈ Terms t (T, {v t : t}) and trans(v t .att) ∈ talg({v t : t}). Since ∆ preserves type algebras, we have trans(v t .att) ∈ talg(∆ F ({v t : t})), and hence we can define Q F (att) to be trans(v t .att). For example, the Q F that corresponds to Figure 8 is (note that we write 'x' to indicate an x ∈ talg(y(N))): For Q F to be an uber-flower that obeys the restriction that variables in for clauses only bind entities and not types, F must be surjective on attributes. This semi-decidable condition implies that for every I, there will be no skolem terms in talg(∆ F (I)), i.e., talg(∆ F (I)) ∼ = Ty. Formally, F is surjective on attributes when for every attribute att : t → t ∈ T , there exists an entity s ∈ S such that F(s) = t and there exists an e ∈ Terms t (T, {v : s}) such that T ∀v : F(s). F(e) = v.att.

Converting Queries to Data Migrations
A conjunctive uber-flower Q : S → T , where S and T are schemas on the same type-side Ty, induces a data migration eval(Q) : S-Inst → T -Inst ∼ = ∆ G • Π F and adjoint data migration coeval(Q) : T -Inst → S-Inst ∼ = ∆ F • Σ G for some X, F : S → X, G : T → X. In this section, we construct X, F, and G. First, we define a schema X such that S ⊆ X and we define F : S → X to be the inclusion mapping. We start with: Then, for each entity t ∈ T and each v : s in f r t (the frozen instance for t in Q), we add a foreign key to X: For each equation e = e ∈ wh t we add an equation to X: ∀x : t. eσ x = e σ x ∈ Eq(X) and for each foreign key f k : t → t and for each v : s ∈ f r t , we add an equation to X: This completes the schema X. Finally, we define G : T → X to be the identity on entities and foreign keys, and on attributes we define: For example, the schema X for the query Promote ( Figure 10) is shown in Figure 12.

Implementation
We have implemented the formalism defined in this paper in the FQL tool, which can be downloaded at http://categoricaldata.net/fql.html. In this section we discuss certain implementation issues that arise in negotiating between syntax and semantics, and provide algorithms for key parts of the implementation: deciding equality in equational theories, saturating theories into term models, checking conservativity of equational theories, (co-)evaluating queries, and (co-)pivoting (converting instances into schemas).

Deciding Equality in Equational Theories
Many, but not all, constructions involving equational theories, including query evaluation, depend crucially on having a decision procedure for provable equality in the theory. A decidable equational theory is said to have a decidable word problem. The word problem is obviously semi-decidable: to prove if two terms (words) p and q are equal under equations E, we can systematically enumerate all of the (usually infinite) consequences of E until we find p = q. However, if p and q are not equal, then this enumeration will never stop. In practice, not only is enumeration computationally infeasible, but for query evaluation, we require a true decision procedure: an algorithm which, when given p and q as input, will always terminate with "equal" or "not equal" 3 . Hence, we must look to efficient, but incomplete, automated theorem proving techniques to decide word problems.
The FQL tool provides a built-in theorem prover based on Knuth-Bendix completion (Knuth & Bendix, 1970): from a set of equations E, it attempts to construct a system of re-write rules (oriented equations), R, such that p and q are equal under E if and only if p and q re-write to syntactically equal terms (so-called normal forms) under R. We demonstrate this with an example. Consider the equational theory of groups, on the left, below. Knuth-Bendix completion yields the re-write system on the right in Figure 14. To see how these re-write rules are used to decide the word problem, consider the two terms (a −1 * a) * (b * b −1 ) and b * ((a * b) −1 * a). Both of these terms re-write to 1 under the above re-write rules; hence, we conclude that they are provably equal. In contrast, the two terms 1 * (a * b) and b * (1 * a) re-write to a * b and b * a, respectively, which are not syntactically the same; hence, we conclude that they are not provably equal (which is different than saying they are provably not equal).

Fig. 14. Knuth-Bendix Completion for Group Theory
The details of how the Knuth-Bendix algorithm works are beyond the scope of this paper. However, we make several remarks. First, Knuth and Bendix's original algorithm (Knuth & Bendix, 1970) can fail even when a re-write system to decide a word problem exists; for this reason, we use the more modern, "unfailing" variant of Knuth-Bendix completion (Bachmair et al., 1989). Second, first-order, simply-typed functional programs are equational theories that are already complete in the sense of Knuth-Bendix. Third, specialized Knuth-Bendix algorithms (Kapur & Narendran, 1985) exist for theories where all function symbols are unary, such as for the entity and attribute parts of our schemas.

Saturating Theories into Term Models
Many, but not all, constructions involving equational theories, including query evaluation, depend crucially on having a procedure, called saturation, for constructing finite term models from theories. This process is semi-computable: there are algorithms that will construct a finite term model if it exists, but diverge if no finite term model exists. The FQL tool has two different methods for saturating theories: theories where all function symbols are unary can be saturated using an algorithm for computing Left-Kan extensions (Carmody et al., 1995) (Bush et al., 2003), and arbitrary theories can be saturated by using a decision procedure for the theory's word problem. Let T h be an algebraic theory. We construct T h in stages: first, we find all not provably equal terms of size 0 in T h; 4 call this T h 0 . Then, we add to T h 0 all not provably equal terms of size 1 that are not provably equal to a term in T h 0 ; call this T h 1 . We iterate this procedure, obtaining a sequence T h 0 , T h 1 , . . .. If T h is indeed finite, then there will exist some n such that T h n = T h n+1 = T h and we can stop. Otherwise, our attempt to construct T h will run forever: it is not decidable whether a given theory T h generates a finite term model. Note that the model T h computed using this procedure is technically not the canonical term model for the theory; rather, we have constructed a model that is isomorphic to the canonical term model by choosing representatives for equivalence classes of terms under the provable equality relation. Depending on how we enumerate terms, we can end up with different models. As a reminder, we write n f T h (e) to indicate the unique e ∈ T h such that T h e = e ; i.e., e is the normal form for e in T h .
Saturation is used for constructing tables from instances to display to the user, and for (co-)evaluating queries on instances. In general, the type side Ty of an instance I will be infinite, so we cannot saturate the equational theory of the instance directly (i.e., I is often infinite). For example, if the type-side of I is the free group on one generator a, then I will contain a, a * a, a * a * a, and so on. Hence, as described in section 3, the FQL tool computes the term model for only the entity and attribute part of I (namely, I EA ), along with an instance (equational theory) called the type-algebra of I (namely, talg(I)). The pair ( I EA ,talg(I)) is sufficient for all of FQL's purposes. The FQL tool supports an experimental feature that we call "computational type-sides". The mathematics behind this feature have not been fully worked out, but it provides a mechanism to connect FQL to other programming languages. An L -valued model of talg(I) is similar to a (set-valued) model of talg(I), except that instead of providing a carrier set for each sort in talg(I), an L -valued model provides a type in L , and instead of providing a function for each symbol in talg(I), an L -valued model provides an expression in L . For example, if L = Java, then we can interpret String as java.lang.String, Nat as java.lang.Integer, + : String → String as java.lang.String.append, etc. (Note that our L -models are on talg(I), not Ty; so an L -model must provide a meaning for the skolem terms in talg(I), which can be tricky.) Given an L -model M, we can take the image of I EA under M by replacing each term talg(t) t ∈ I EA with the value of t in M. We write this as M( I EA ). The pair (M( I EA ), M) can be used by the FQL tool in many situations where ( I EA ,talg(A)) is expected; for example, in displaying tables to users (see Figure 15), and when (co-)evaluating queries. We have used type-side computation to connect the FQL tool to a number of 3rd party libraries, including a machine-learning library, and formalizing computational type-sides is an important area for future work.

Deciding that a Theory Conservatively Extends Another
As described in Section 3, we may want instances to conservatively extend their schemas, where a theory T h 2 conservatively extends T h 1 when T h 1 ∀Γ. t = t : s iff T h 2 ∀Γ. t = t : s for all t,t ∈ Terms s (T h 1 , Γ) for every Γ. Conservativity in equational logic is not decidable, and the only system we are aware of that automates conservativity checks in a language at least as expressive as equational logic is the system (Lüth et al., 2005). In this section, we give a simple algorithm that soundly but incompletely checks that a theory T h 2 conservatively extends a theory T h 1 by showing that T h 2 freely extends T h 1 .
Let T h 1 be a equational theory, and let T h 2 extend T h 1 with new sorts, symbols, and equations. We will simplify the presentation of T h 2 by repeatedly looking for equations of the form g = t, where g is a generator (0-ary symbol) of T h 2 but not of T h 1 , and t does not contain g; we then substitute g → t in T h 2 . If after no more substitutions are possible, all equations in T h 2 are either reflexive or provable in T h 1 , then T h 2 is conservative (actually, free) over T h 1 . For example, we can show that the theory: {infinity : Nat, undef : Nat, infinity = 0, undef = 1, infinity = undef} is not conservative over Type (Figure 2), because the simplification process yields the nonreflexive equation 0 = 1, which is not provable in Type. However, the algorithm is far from complete. The theory: {+ : Nat × Nat → Nat, infinity : Nat, undef : Nat, infinity+1 = undef+1} does not pass our check, even though it is a conservative extension of Type. Developing a better conservativity checker is an important area for future work, lest we inadvertently "damage our ontologies" (Ghilardi et al., 2006). The process of repeatedly substituting g → t, where g is a generator in an instance's type-algebra and t is a type-side term is also used by the FQL tool to simplify the display of tables by biasing the tables to display e.g., 45 instead of e.g. age.bill when 45 and age.bill are provably equal.

Evaluating Queries
Although it is possible to evaluate a conjunctive uber-flower query by translation into a data migration of the form ∆ • Π, we have found that in practice it is faster to evaluate such queries directly, using an algorithm that extends relational query evaluation. Let Q : S → T be a conjunctive uber-flower and let I be an S-instance. We now describe how to compute the instance (theory) eval(Q)(I). First, we copy the generators and equations of the type-algebra talg(I) into eval(Q)(I). Then, for every target entity t ∈ T , we perform the following: • We define the generators of entity t in eval(Q)(I) to be those I EA environments for f r t that satisfy wh t . Formally, we represent these environments as ground substitutions f r t → Terms(S, / 0) and define, where f r t := { −−→ v i : s i }: , ∀eq ∈ wh t , ∀e i ∈ I EA (s i )} • For each attribute att : t → t ∈ T , we have a term [att] ∈ Terms t (S, f r t ) from the return clause for t. For every substitution σ ∈ eval(Q)(t), we have [att]σ ∈ Terms t (S, / 0), and we add: The reason that trans([att]σ ) ∈ Terms t (eval(Q)(I), / 0) is because trans([att]σ ) ∈ Terms t (talg(I), / 0) and talg(I) ⊆ eval(Q)(I). See 3.1 for the definition of trans. • For each foreign key f k : t → t ∈ T , we have a transform from the frozen instance for t to the frozen instance for t from the keys clause for t, which can be thought of as a substitution [ f k] : f r t → Terms(S, f r t ). For every substitution σ : f r t → Terms(S, / 0) ∈ eval(Q)(t), we add the equation: is a transform, not an arbitrary substitution.
Note that in order to build the instance eval(Q)(I), we have effectively constructed the term model eval(Q)(I) EA , and then "de-saturated" the term model into an equational theory. Evaluation of uber-flowers is similar, except that there are multiple tableau associated with each target entity, so the results for each tableau associated with target entity t must be disjointly-unioned together to populate eval(Q)(I)(t).
To make the above description concrete, we will now evaluate the conjunctive uberflower Promote : Emp → Emp from figure 10 on the instance Inst from figure 6, which in turn is on the schema Emp from figure 5 on the type-side Type from figure 2. Our goal is to compute the instance (equational theory) eval(Promote, Inst). We start by copying talg(Inst) into eval(Promote, Inst). Next, we process the tableau. We start with target entity Dept ∈ T . The from and where clauses give us a    each target entity t ∈ T , consider the generators in eval(Q)(I)(t): they will be the ground substitutions f r t → Terms(S, / 0) satisfying wh t . We will map each such substitution to a substitution (generator) in eval(Q)(J)(t). Given such a substitution σ := [v 0 : s 0 → e 0 , . . . , v n : s n → e n ], where e i ∈ Terms s i (S, / 0), we define: In general, h(e i ) need not appear in J E , so we must use the normal for h(e i ) in J E . Evaluation of (non-conjunctive) uber-flowers on transforms is similar.

Evaluating Morphisms of Queries
If Q 1 , Q 2 : S → T are conjunctive uber-flowers, a morphism h : Q 1 → Q 2 is, for each entity

Co-Evaluating Queries
Although it is possible to co-evaluate a conjunctive 5 uber-flower query by translation into a data migration of the form ∆ • Π, we have implemented co-evaluation directly. Let Q : S → T be a conjunctive uber-flower and let J be a T -instance. We are not aware of any algorithm in relational database theory that is similar to coeval(Q); intuitively, coeval(Q)(J) products the frozen instances of Q with the input instance J and equates the resulting pairs based on either the frozen part or the input part. We now describe how to compute the S-instance (theory) coeval(Q)(J). First, we copy the generators and equations of the type-algebra talg(J) into coeval(Q)(J). We define coeval(Q)(I) to be the smallest theory such that, for every target entity t ∈ T , where f r t := {v 1 : s 1 , . . . , v n : s n }, • ∀(v : s) ∈ f r t , and ∀ j ∈ J (t), (v, j) : s ∈ coeval(Q)(J) • ∀e = e ∈ wh t , and ∀ j ∈ J (t), recall that [att] ∈ Terms t (S, f r t ) is the return clause for attribute att and trans : Terms t (J, / 0) → talg(J) is defined in Section 3.1. • ∀ f k : t → t ∈ T, and ∀ j ∈ J (t), and ∀(v : s ) ∈ f r t , recall that the substitution [ f k] : f r t → Terms(S, f r t ) is the keys clause for foreignkey f k.
The co-evaluation the conjunctive uber-flower Promote : Emp → Emp from figure 10 on the instance Inst from figure 6 is in fact isomorphic to the evaluation of promote ( Figure 16); the reason is that evaluation and co-evaluation of Promote are semantically both projections (∆-only operations).

Co-Evaluating Queries on Transforms
Let Q : S → T be a conjunctive uber-flower and let h : I → J be a transform of T -instances I and J. Our goal is to define the transform coeval(Q)(h) : coeval(Q)(I) → coeval(Q)(J). For each entity t ∈ T , and for every ∀(v : s) ∈ f r t , and for every j ∈ J E (t), we define: As was the case for evaluation of uber-flowers on transforms, we must use n f to find appropriate normal forms.

Co-Evaluating Morphisms of Queries
If Q 1 , Q 2 : S → T are conjunctive uber-flowers, a morphism h : Q 1 → Q 2 is, for each entity t ∈ T , a morphism from the frozen instance for t in Q 1 to the frozen instance for t in Q 2 , and it induces a transform coeval(h) : coeval(Q 1 )(J) → coeval(Q 2 )(J) for every T -instance J; in this section, we show how to compute [h]. Let t ∈ T be an entity The generators of coeval(Q 1 )(J) are pairs (v, j) with v : s ∈ f r Q 2 t and j ∈ J E (t). Define:

The Unit and Co-Unit of the Co-Eval Eval Adjunction
Let Q : S → T . Then coeval(Q) is left adjoint to eval(Q), i.e., coeval(Q) eval(Q). This means that the set of morphisms coeval(Q)(I) → J is isomorphic to the set of morphisms I → eval(Q)(J) for every I, J. The unit and co-unit of the adjunction, defined here, describe this isomorphism. Let I be a S-instance. The component at I of the co-unit transform ε I : coeval(Q)(eval(Q)(I)) → I is defined as:

Pivot (Instance → Schema)
Let S be a schema on type-side Ty and let I be an S-instance. The pivot of I is defined to be a schema S on Ty, a mapping F : I → S, and a I-instance J, such that Σ F (J) = I, defined as follows. First, we copy talg(I) into J. Then for every entity s ∈ S, and every i ∈ I E (s), we have: i : s ∈ I F(i) := s i : s ∈ J and for every attribute att : s → s ∈ S, where trans is defined in Section 3.1, and for every foreign key f k : s → s ∈ S, In addition, for each generator g := e. f k 1 . . . . . f k n .att in talg(I), we have a term [g] ∈ Terms(J, / 0) defined as: Let S be a schema on type-side Ty and let I be an S-instance. The co-pivot of I is defined to be a schema S on Ty, a mapping F : S → I, and a I-instance J, such that ∆ F (J) ∼ = I, defined as follows. In fact, we obtain an inclusion F : S → I, so J is superfluous. First, we add a single entity to S, and for every generator g : s ∈ talg(I), an attribute g A : ∈ I g A : → s ∈ I Then for every entity s ∈ S, and i ∈ I E (s) we have a foreign key: i E : → s ∈ I F(s) := s and additionally, for every attribute att : s → s , and every foreign key f k : s → s , we have: where trans is defined in Section 3.1. See Figure 18 for an example on type-side Type (Figure 2).

A Pushout Design Pattern for Functorial Data Integration
In this section we describe a design pattern for integrating two databases on two different schemas, relative to an overlap schema and an overlap instance, using the formalism defined in this paper. The overlap schema is meant to capture the schema elements common to the two input schemas (e.g., that Patient and Person should be identified), and the overlap instance is meant to capture the instance data that should be identified (e.g., that Pete and Peter are the same person). Although the Σ, ∆, Π data migration functors are sufficient to express queries and data migrations, as unary operations they are insufficient to express data integrations, which involve many schemas and instances and their relationships (Doan et al., 2012). So, we will need to define additional operations on our formalism as we develop our pattern. In particular, we will define pushouts (Barr & Wells, 1995) of schemas and instances and use pushouts as the basis of our pattern. The idea of using pushouts to integrate data is not new (Goguen, 2004); our goal here is to express this pattern using our formalism. With pushouts defined, we describe our pattern at an abstract level, and then we describe a medical records example that uses the pattern. This example is built into the FQL tool as the "O Integration" example.

Pushouts of Schemas and Instances
Let C be a category and F 1 : S → S 1 and F 2 : S → S 2 be morphisms in C . A pushout of F 1 , F 2 is any pair G 1 : S 1 → T and G 2 : S 2 → T such that G 2 •F 2 = G 1 •F 1 , with the property that for any other pair G 1 : S 1 → T and G 2 : S 2 → T for which G 2 • F 2 = G 1 • F 1 , there exists a unique t : T → T such that G 1 = t • G 1 and G 2 = t • G 2 , as shown in Figure 19.
The pushout schemas and instances defined in this section are canonical, but the price for canonicity is that their underlying equational theories tend to be highly redundant (i.e., have many symbols that are provably equal to each other). The canonical pushout schemas and instances can be simplified, and in fact FQL performs simplification, but the simplification process is necessarily non-canonical. In our extended medical example, we will use a simplified non-canonical pushout schema.

Overview of the Pattern
Given input schemas S 1 , S 2 , an overlap schema S, and mappings F 1 , F 2 as such: we propose to use their pushout: as the integrated schema. Given input S 1 -instance I 1 , S 2 -instance I 2 , overlap S-instance I and transforms h 1 : Σ F 1 (I) → I 1 and h 2 : Σ F 2 (I) → I 2 , we propose the pushout of: as the integrated T -instance.
Because pushouts are initial among the solutions to our design pattern, our integrated instance is the "best possible" solution in the sense that if there is another solution to our pattern, then there will be a unique transform from our solution to the other solution. In functional programming terminology, this means our solution has "no junk" (extra data that should not appear) and "no noise" (missing data that should appear) (Mitchell, 1996). Initial solutions also appear in the theory of relational data integration, where the chase process constructs weakly initial solutions to data integration problems (Fagin et al., 2005).

An Example of the Pattern
As usual for our formalism, we being by fixing a type-side. We choose the Type typeside from Figure 2. Then, given two source schemas S 1 , S 2 , an overlap schema S, and mappings F 1 , F 2 as input, our goal is to construct a pushout schema T and mappings G 1 , G 2 , as shown in figure 20. In that figure's graphical notation, an attribute • A → att • String is rendered as • A − • att . Next, given input S 1 -instance I 1 , S 2 -instance I 2 , overlap S-instance I and morphisms h 1 : Σ F 1 (I) → I 1 and h 2 : Σ F 2 (I) → I 2 , our goal is to construct a pushout T -instance J and morphisms j 1 , j 2 , as shown in Figure 21; note that in this figure, by K → (F,h) L we mean that h : Σ F (K) → L, and that we use variable font for generators, sansserif font for sorts and symbols, and regular font for terms in the type-side.
Intuitively, this example involves integrating two different patient records databases. In S 1 , the "observations" done on a patient have types, such as heart rate and blood pressure. In S 2 , the observations still have types, but via "methods" (e.g., patient self-report, by a nurse, by a doctor, etc; for brevity, we have omitted attributes giving the names of these methods). Another difference between schemas is that S 1 assigns each patient a gender, but S 2 does. Finally, entities with the same meaning in both schemas can have different names (Person vs Patient, for example).
We construct the overlap schema S by thinking about the meaning of S 1 and S 2 ; alternatively schema-matching techniques (Doan et al., 2012) can be used to construct overlap schemas. In this example, it is clear that S 1 and S 2 share a common span P f ← O → g T relating patients, observations, and observation types; in S 1 , this span appears verbatim but in S 2 , the path g corresponds to g 2 • g 1 . This common span defines the action of F 1 and F 2 on entities and foreign keys, so now we must think about the attributes. For purposes of exposition we assume that the names of observation types ("BP", "Weight", etc.) are the same between the instances we are integrating. Hence, we include an attribute for observation type in the overlap schema S. On the other hand, we do not assume that patients have the same names across the instances we are integrating; for example, we will have the same patient named "Pete" in one database and "Peter" in the other database. Hence, we do not include an attribute for patient in S. If we did include an attribute for patient name, then the pushout schema would have a single attribute for patient name, and the integrated instance would include the equation "Pete" = "Peter" : String. We would Fig. 20. Medical Records Schema Integration violate the conservative extension property (see Section 4.3), which is not a desirable situation (Ghilardi et al., 2006). So, our design pattern explicitly recommends that when two entities in S 1 and S 2 are identified in an overlap schema, we should only include those attributes that appear in both S 1 and S 2 for which the actual values of these attributes will correspond in the overlap instance. As another example of this phenomenon, to a first approximation, attributes for globally unique identifiers such as social security numbers can be added to overlap schemas, but attributes for non-standard nomenclatures such as officer titles (CEO vs Chief Executive Officer) should not be added to overlap schemas. With the overlap schema in hand, we now turn toward our input data. We are given two input instances, I 1 on S 1 and I 2 on S 2 . Entity-resolution (ER) techniques (Doan et al., 2012) can be applied to construct an overlap instance I automatically. Certain ER techniques can even be implemented as queries in the FQL tool, as we will describe in a later section. But for the purposes of this example we will construct the overlap instance by hand. We first assume there are no common observations across the instances; for example, perhaps a cardiologist and nephrologist are merging their records. We also assumed that the observation type vocabulary (e.g., "BP" and "Weight") are standard across the input instances, so we put these observation types into our overlap instance. Finally, we see that there is one patient common to both input instances, and he is named Peter in I 1 and Pete in I 2 , so we add one entry for Pete/Peter in our overlap instance. We have thus completed the input to our design pattern.
In the output of our pattern we see that the observations from I 1 and I 2 were disjointly unioned together, as desired; that the observation types were (not disjointly) unioned together, as desired; and that Pete and Peter correspond to the same person in the integrated instance. In addition, we see that one patient, Jane, could not be assigned a gender.

Entity-resolution Using Queries
Let schemas S, S 1 , S 2 , mappings F 1 : S → S 1 , F 2 : S → S 2 , and instances I 1 ∈ S 1 -Inst, I 2 ∈ S 2 -Inst be given. In practice, we anticipate that sophisticated entity-resolution (Doan et al., 2012) techniques will be used to construct the overlap instance I ∈ S-Inst and transforms h 1 : Σ F 1 (I) → I 1 and h 2 : Σ F 2 (I) → I 2 . However, it is possible to perform a particularly simple kind of entity resolution directly using conjunctive uber-flowers.
Technically, the overlap instance used in the pushout problem should not be thought of as containing resolved (unified) entities; rather, it should be thought of as containing the record linkages between entities that will resolve (unify) (Doan et al., 2012). The pushout resolve entities by forming equivalence classes of entities under the equivalence relation induced by the links. As the size of the overlap instance gets larger, the size of the pushout gets smaller, which is the opposite of what would happen if the overlap instance contained the resolved entities themselves, rather than the links between them. For example, let A and B be instances on some schema that contains an entity Person, and let A(Person) := {a 1 , a 2 } and B(Person) := {b 1 , b 2 }. If the overlap instance O has O(Person) := {(a 1 , b 1 ), (a 1 , b 2 ), (a 2 , b 1 ), (a 2 , b 2 )}, then this does not mean that the pushout will have 4 people; rather, the pushout will have one person corresponding to {a 1 , a 2 , b 1 , b 2 }, because these four people are linked. Intuitively, the overlap instance I constructed by the technique in this section is (isomorphic to) a sub-instance of ∆ F 1 (I 1 ) × ∆ F 2 (I 2 ), where × denotes a kind of product of instances which we will not define here. When I is empty, the pushout will be a co-product ("maximally large"), and when I is not a proper subinstance, the pushout will be the pushout of a product, which will be small -perhaps terminal ("maximally small").
Let inc 1 : S 1 → S 1 +S 2 and inc 2 : S 2 → S 1 +S 2 be inclusion schema mappings, and define the S 1 + S 2 instance I := Σ inc 1 (I 1 ) + Σ inc 2 (I 2 ). This instance will contain I 1 and I 2 within it, and will contain nothing else. (Here X +Y means co-product, which is equivalent to the pushout of X and Y over the empty schema or instance).
We construct overlap S-instance I by defining a query Q : S 1 + S 2 → S and evaluating it on the S 1 + S 2 -instance I . For each entity s ∈ S, we choose a set of pairs of attributes from F 1 (s) and F 2 (s) that we desire to be "close". In the medical records example, for P we choose (PatientAtt, PersonAtt) and for T we choose (ObsTypeAtt, TypeAtt); we choose nothing for O. We next choose a way to compare these attributes; for example, we choose a string edit distance of less than two to indicate that the entities match. This comparison function must be added to our type side, e.g., strMatches : String × String → Nat true : Nat true = 1 The function strComp can be defined using equations, although the FQL tool allows such functions to be defined using java code (see Section 4). With the String-comparator in hand, we can now define Q : S 1 + S 2 → S as in Figure 22. The overlap instance I is defined as eval(Q)(I ). To construct h n : Σ F n (I) → I n for n = 1, 2, we define projection queries Q n : S 1 + S 2 → S and inclusion query morphisms q n : Q n → Q as in Figure 22. We start with the induced transforms for q n , then apply Σ F n , then compose with the isomorphism eval(Q n )(I ) ∼ = ∆ F n (I n ), and then compose the co-unit ε of the Σ F n ∆ F n adjunction, to obtain h n as in Figure 22. The result of running Figure 22 on the medical records data I 1 , I 2 from Figure 21 will be the overlap instance I from Figure 21.
To compute the isomorphism eval(Q n )(I ) → ∆ F n (I n ), we note that the generators of eval(Q n )(I ) will be singleton substitutions such as [v n → in j n a n ] where a n is a term in Σ inc n (I n ) and in j n means co-product injection. But inc n is an inclusion, so a n is a term in I 1 . Because we compute ∆ F n by translation into an uber-flower similar to Q n , the generators G G Σ F n (eval(Q n )(I )) ∼ = G G Σ F n (∆ F n (I n )) ε G G I n Fig. 22. Entity-Resolution on Medical Records using Uber-flowers of ∆ F n (I ) will have a similar form: [v n → a n ] which defines the necessary isomorphism.
In the case where all schemas are disjoint and variables are chosen appropriately, the isomorphism can be made an equality.

Further Patterns
Pushouts have a dual, called a pullback, obtained by reversing the arrows in the pushout diagram (see Figure 19). Pushouts can also be generalized to co-limits, which can be thought of as n-ary pushouts (Barr & Wells, 1995). Exploring applications of pullbacks and colimits to data integration, as well as finding other useful design patterns and constructions for functorial data integration, is an important area for future work.

Conclusion
In this paper we have described what we believe to be the first truly practical formalism for the functorial data model, and work continues. In the short term, we aim to formalize our experimental "computational type-sides", and to develop a better conservativity checker. In the long term, we are looking to develop other design patterns for functorial data integration and to study their compositions, and we are developing an equational theorem prover tailored to our needs. In addition to these concrete goals, we believe there is much to be gained from the careful study of the differences between our formalism, with its category-theoretic semantics, and the formalism of embedded dependencies, with its relational semantics (Doan et al., 2012). For example, there seems to be a semantic similarity between our Σ operation and the chase; as another example, so far we have found no relational counterpart to the concept of query "co-evaluation"; and finally, our "uberflower" queries may suggest generalizations of "comprehension syntax" (Grust, 2003).