[TYPES/announce] Categorical Informatics positions

[Ryan Wisnesky]

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 at catinf.com