Algebraic Databases

This month, our speaker will be Ryan Wisnesky. He spoke at Boston Haskell some time ago (video available here (https://www.youtube.com/watch?v=Q0m8baqBrk4)) about categorical databases, which allow thinking about database schemas and queries in ways that are similar to functional programming. He's returning to give an overview of the advances that have been made in these query langauges in the last few years.

Abstract

In this talk we describe a new approach to expressive database query languages that is a conceptual dual to LINQ. We formalize database schemas as algebraic (multi-sorted equational) theories obeying certain restrictions. Hence, a schema can be thought of as a type theory, and morphisms of schemas are morphisms of type theories. We also formalize database instances as equational theories, whose meaning is their initial term model. Schemas form a category, and the database instances on a schema S form a category, S-Inst. Associated with a schema morphism F : S -> T are three functors, Sigma_F : S-Inst -> T-Inst (corresponding to substitution), along with a right adjoint, Delta_F : T-Inst -> S-Inst, which in turn has a right adjoint, Pi_F : S-Inst -> T-Inst. These operations form an alternative basis for both database query (where we compare them to relational algebra) and database integration (where we compare them to embedded implicational dependencies). We say that our approach is a dual to LINQ because we embed programs (in the guise of equational theories) into schemas, rather than embed schemas (in the guise of types) into programs as LINQ does. We demonstrate a prototype information integration tool AQL based on our approach.

If there's time, we describe how the database schemas in our work form a cartesian closed category (model of the simply typed lambda calculus), and how the instances on each schema form a topos (model of higher order logic).

There are two-preprints associated with this topic as well as a project website:

http://arxiv.org/abs/1602.03501

http://arxiv.org/abs/1503.03571

http://categoricaldata.net/fql.html

Joint work with Patrick Schultz (MIT), David Spivak (MIT), and Christina Vasilakopoulou (MIT).

Bio

Ryan Wisnesky obtained B.S. and M.S. degrees in mathematics and computer science from Stanford University and a Ph.D. in computer science from Harvard University, where he studied the design and implementation of provably correct software systems (in e.g., Coq). Previously, he was a postdoctoral associate in the Department of Mathematics at MIT, where he developed a functorial query language, FQL. He currently leads FQL-related commercialization activities at Categorical Informatics, Inc. He maintains an active collaboration with the information-integration department of IBM Research, where he contributed to the Clio, Orchid, and HIL projects.

Logistics

The meetup will be at the Thoughtbot location in downtown Boston. The scheduled start is at 6:30PM. Food should arrive around then and the talk will begin some time after that.

Food and beverages will be provided by Thoughtbot.