It looks like you're new here. If you want to get involved, click one of these buttons!
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
Comments
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.
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.
Hi, Ryan! I've "announced" your self-introduction to make it more visible. I'll also mention it in our computer science discussion group.
Hi, Ryan! I've "announced" your self-introduction to make it more visible. I'll also mention it in our computer science discussion group.
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.
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.
Thanks Robert, I just commented over there.
Thanks Robert, I just commented over there.