Implementing category theory

Several computational implementation of category theory use some form of dependent types. Rather than “full” dependent types, first-order logic with dependent types and generalized algebraic theories may be considered as “fragments” of a full dependent type theory and thus more amenable to computational implementation.

First-order logic with dependent types (FOLDS)
Generalized algebraic theories (GAT)
Categories with families (CwF)

Makkai asserts the similarity between GAT and FOLDS, but claims that both FOLDS has a simpler syntax, but more importantly can be used to implement “generalized invariance”.

Palmgren classifies FOLDS as a “logic-enriched type theory” and develops the relationship between FOLDS and categories with families by developing a hyperdoctrine over CwF.

Since Catlab implements generalized algebraic theories, this should be my starting place.

FOLDS is used by Schulman in his papers looking at various models of set theory.

FOLDS also seems interesting for categorical semiotics, since it takes the notion of dependency as primitive, which seems consistent with Peirce’s analysis of triadic relation.

There is a family resemblance between the wiring diagram syntax proposed by Patterson in Catlab and the dependent type syntax in FOLDS. Wiring diagrams give a syntax to monoidal categories and operads over these categories. FOLDS can be used to specify a language of monoidal categories. Catlab also gives a syntax of monoidal categories in Catlab, presumably used in the wiring diagram implementation. Is there a meaningful difference between GAT and FOLDS in this implementation?

Since the dependent types form a category (Makkai and Shulman differ on what to call this - Makkai calls it a one-way category, Shulman an inverse category), the Catlab implementation of C-Sets should be able to be used to implement FOLDS. Relations would correspond to tables, variables to rows, and the dependency structure to foreign keys. Could the foreign keys be used to automatically populate the relevant databases? For example, declaring a variable x for a set A should automatically insert A into Set, x into El(A,x), a_x into Arr(A,x,x), and i_x into I(A,a_x), e_x into Eq(A,a_x,a_x) and t_x into Tri(A,a_x,a_x,a_x). The variable names would be implemented by Catlab automatically - perhaps an attribute for each variable name should also be implemented.

Github update

It appears that I cannot push using ssh from within the firewall, so setting up the https alternative appears to have been worth it.

Logic in color

Was thinking about logic programming, did a Google search on “logic-programming type-theory”, found Christian Williams blog post on Native Type Theory, looked him up on Twitter, and found this talk. He develops the Poincare dual for two-categories, using colors to indicate types. He proposes to develop the simplest language using relations.

Williams develops string diagrams for 2-categories using the concrete example of the bicategory of relations.

The emphasis of this talk on double categories reminds me of the use of double categories in databases (Patterson’s recent talk on double categories in databases), earlier work by Wiskesky on algebraic databases, and the blog entry at Algebraic Julia on attributed C-Sets. Jaz Myers uses double categories in his categorical systems theory, and previously published work on “logic in color” for proarrow equipments (as an undergrad!). It also reminds me of the “operations/relations” discussion in Makkai’s work, where he contrasts “pure FOLDS” (without operations) and generalized algebraic theories (which include both operations and relations).

Category theory for energy modeling

Most of the pieces have been built, but they need to be integrated. Data integration through algebraic databases. This would expand Greg Shively’s work in a more general direction. EIA could also be interested. Both capacity expansion and “production cost modeling” require stochastic optimization and decision-making. Catlab has wiring diagrams and operads - another example of categorical systems theory? Aggregation and disaggregation should be automated in a similar manner to integration routines, where more difficult, rapidly changing areas get greater attention.

Could the central idea be using “double categories?” This project could be built on Christain William’s “graphical editor”. Bryce Clarke put together a nice discussion of lenses in double categories - could this be generalized to more general optics? Would this be necessary?

Bryce Clarke says that certain? optics form double categories - cites a talk by Bruno.