Standard library of ACT applications

[jpfairbanks]

When we talked about a standard library of prebuilt functionality for Catlab, we talked about a module for linear algebra (#65). I think this issue could serve as a collection point for what to put in that standard library. Here are some of the examples that make sense to me:

1. LinAlg: describing linear relations with graphical linear algebra
2. MarkovProcesses and Circuits: anything in CS that you can represent with graphs probably forms a category of decorated cospans https://aip.scitation.org/doi/pdf/10.1063/1.4941578?class=pdf
3. Relational Ologs: describe arbitrary knowledge with FreeBicatRel
4. Process Planning: objects are physical objects and morphisms are arbitrary processes (https://doi.org/10.1016/j.compind.2019.103124) (ex. kitchen processes)

I guess for each component of the library we should have a doctrine, an instance, some examples, and a function that computes something interesting about a morphism functorially.

1. LinAlg: solve systems of equations by computing matvec functorially
2. MarkovProcesses: solve for equilibrium (stationary distribution)
3. RelationalOlog: generate a DB schema / knowledge graph to represent information
4. Process Planning: compute plan refinements with pushouts

@epatters do you see any other good examples?

[epatters]

Regarding the linear algebra module, in addition to graphical linear algebra (monoidal product = direct sum), I'd also like to support tensor networks (monoidal product = tensor product).

We could interface with ITensor.jl and possibly other tensor libs. The ITensor book says that ITensor is "inspired by diagrammatic notation for tensor networks" but AFAIK it does not actually support diagrammatics. It would be fun to remedy this! It would also give me a good excuse to learn more about tensor algorithms.

Another new Julia package for tensors is YaoTensorNetwork.jl.

[jpfairbanks]

Another useful example would be unitful computations. We could implement a @theory for dimensional analysis like

@theory Dimensions(Ob, Hom) begin
    Unitless()::Ob
    Product(A::Ob, B::Ob)::Ob
    @op (*) := Product
    Inv(A::Ob)::Ob
    constant(A::Ob)::(munit→A)

    sum(A)::(A⊗A→A)              ⊣ (A::Ob)
    product(A,B)::(A⊗B→(A*B))    ⊣ (A::Ob, B::Ob)
    ratio(A,B)::(A⊗B→(A*Inv(B))) ⊣ (A::Ob, B::Ob)
    square(A)::(A→A*A)           ⊣ (A::Ob)

    # axioms
    # commutativity of product
    Product(A::Ob, B::Ob) = Product(B, A)
    # Inv(A)*A is Unitless
    Product(A::Ob, B::Inv(A)) = Unitless()
    # A*Unitless == A
    Product(A::Ob, B::Unitless()) = A
    # Associativity of the Product on Objects
    Product(A, B::Product(B,C)) = Product(Product(A, B), C) ⊣ (A::Ob, B::Ob, C::Ob)
end

Then as an instance we can use https://github.com/PainterQubits/Unitful.jl. In this way we can build an ahead of time unit checker for unitful computations