It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 6
- Green Mathematics 1
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Statistical methods 2
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 0
- Strategy 111
- Azimuth Project 1.1K

Options

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.`