Introduction - Ryan Wisnesky

Ryan Wisnesky

Hi all,

My name is Ryan Wisnesky, and I worked as David Spivak's postdoc to create both a company and open source project that implements the 'schemas as categories' idea in working software, called AQL. Seeing as how the seven sketches course is now reaching the database portion, I wanted to say hi and also solicit community involvement in the CI and CatData projects - see below.

---

Categorical Informatics (CI) (http://catinf.com), a data modeling/integration/migration company pioneering a new approach to data based on category theory, is looking to recruit an initial technical staff as it moves from grant-based to angel-based funding. CI was spun out of the MIT math department in 2015 by David Spivak (http://math.mit.edu/~dspivak/) and Ryan Wisnesky (http://wisnesky.net) and maintains an open-source data integration tool, AQL, available at http://catinf.com/download.php .

In CI's approach to data, a database schema is a finitely presented category C and a database instance on C is a set-valued functor C -> Set. The instances on C form a category (indeed, a topos), C-Inst, a functor F from C to another finitely presented category D (so F : C -> D) induces three adjoint data migration functors: Delta_F : D-Inst -> C-Inst, Pi_F : C-Inst -> D-Inst, and Sigma_F : C-Inst -> D-Inst. These data migration functors provide an alternative basis of operations for querying data (compared to SQL) and migration/integrating data (compared to the chase algorithm). At a high level, the objects of C correspond to entities (e.g., Employee, Department, etc), the generating morphisms of C correspond to foreign keys / functions (e.g., worksIn : Employee -> Department, manager : Department -> Employee), and the generating equations of C correspond to data integrity constraints (e.g., manager ; worksIn = id)

The connections to functional programming and database theory are significant and are discussed in a series of papers available at http://categoricaldata.net/fql.html . For example, the query language obtained from delta/sigma/pi can be written using 'SQL-ish' notation, and reasoning about schemas and functors requires use of automated theorem proving methods (e.g., Knuth-Bendix completion).

CI is interested in talking with people who have backgrounds in - category theory - type theory / functional programming - automated theorem proving - database internals / SQL at scale

Please send inquiries to ryan@catinf.com

MatthewDoty

Hey Ryan,

Welcome to the forums!

Categorical Informatics looks really cool. Hopefully either I or someone else around here can find a few spare cycles to collaborate with you on AQL.

John Baez

Hi, Ryan! I've "announced" your self-introduction to make it more visible. I'll also mention it in our computer science discussion group.

Robert Figura

Someone has just tried to mention you in the "History of Databases" thread:

https://forum.azimuthproject.org/discussion/2227/history-of-databases

I'm bugging you here, because mentions are broken with everybody having spaces in their names. It's meant as a notification just as if the mentions were working. Feel free to not respond, at least now you know we're there.

I understand that categorical representations for SQL might help getting types to work to help get better programs in the end. I would love to hear a bit about motivations and lessons from applying these more modern approaches in practice, and I think the others might have more questions.

The discussion is currently drifting towards the practical side, which that may or may not be a good thing.

Ryan Wisnesky

Thanks Robert, I just commented over there.