Options

Introduction - 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

Comments

  • 1.

    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.

    Comment Source: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.
  • 2.

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

    Comment Source:Hi, Ryan! I've "announced" your self-introduction to make it more visible. I'll also mention it in our computer science discussion group.
  • 3.
    edited June 10

    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.

    Comment Source: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.
  • 4.

    Thanks Robert, I just commented over there.

    Comment Source:Thanks Robert, I just commented over there.
Sign In or Register to comment.