Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: practice: software

Topic: Catlab.jl

Sophie Libkind (May 11 2020 at 20:38):

@James Fairbanks @Evan Patterson I've been playing around with Catlab.js and I was wondering how to instantiate something like a Poset. Would it make sense to define a theory that inherits from Category? Or as an instance of a Category?

James Fairbanks (May 11 2020 at 20:42):

you are thinking of a poset as a category where $Ob(C)$ is the elements of the set and $Hom(a,b)$ is empty unless $a\leq b$ right?

James Fairbanks (May 11 2020 at 20:43):

Here is the version for preorders https://github.com/epatters/Catlab.jl/pull/148/files

Sophie Libkind (May 11 2020 at 20:44):

I'm thinking of a poset as a category with $Hom(a,b) \in Bool$

Sophie Libkind (May 11 2020 at 20:44):

Ah cool! Thanks!

sarahzrf (May 11 2020 at 20:45):

a poset is a category enriched in truth values, not where the hom sets are the set of truth values

sarahzrf (May 11 2020 at 20:45):

so you want an $\in$ up there, not an $=$

Evan Patterson (May 11 2020 at 20:45):

The source file added by that PR is: https://github.com/epatters/Catlab.jl/blob/master/src/doctrines/Preorders.jl

sarahzrf (May 11 2020 at 20:45):

also, it's probably a good idea to distinguish between truth values and booleans if you're doing constructive work!

Evan Patterson (May 11 2020 at 20:46):

So you can see that we have a thin category, which inherits from category, and also a preorder, which does not. From the comment at the end, you can see that we want to say that these are related, but haven't yet implemented that machinery.

James Fairbanks (May 11 2020 at 20:47):

I think you just need to add antisymmetry to go from preorder to poset. so you could inherit from ThinCategory and add an additional axiom for antisymmetry. We don't really have the machinery for enforcing or testing the axioms, right now they are carried around in the relevant data structures

James Fairbanks (May 11 2020 at 20:49):

following the julia approach we leave a lot of the rule following to the user. since you can't actually enforce anything in julia, haven't spent a lot of effort on implementing enforcement.

Sophie Libkind (May 11 2020 at 20:51):

In one experiment, I composed two morphisms $f$ and $g$ where the codomain of $f$ did not match the domain of $g$ and it composed no problem. Is that an example of leaving the rule following to the user?

Evan Patterson (May 11 2020 at 20:52):

That can be enforced. It depends on how the expressions are set up in the @syntax macro.

Evan Patterson (May 11 2020 at 20:53):

When strict=true, like here, it should work. (If it doesn't, it's a bug and please report it.)

James Fairbanks (May 11 2020 at 20:53):

that might be bug i've hit stuff like that before where stuff composes fine and then later you try to convert it to a wiring diagram or something and you get a runtime error in the WD code because it is checking that things match up.

James Fairbanks (May 11 2020 at 20:54):

when strict=true, that means that the syntax system will check for well formedness, right?

Evan Patterson (May 11 2020 at 20:54):

It means that it will check that, e.g., domains and codomains match when composing. More generally, it enforces the equalities implied by the GAT term and type constructors.

Sophie Libkind (May 11 2020 at 20:55):

In this particular experiment, I believe I had defined an @instance macro. What are the use case differences between @instance and @syntax?

James Fairbanks (May 11 2020 at 20:55):

i definitely assumed that strict meant strictification

Evan Patterson (May 11 2020 at 20:55):

OK, maybe we should use a different word.

Evan Patterson (May 11 2020 at 20:56):

The reason that this is even an option, BTW, is that if you have nontrivial equations between your objects, then it may be difficult or impossible to verify that the domain and codomain objects are actually equal before composing.

James Fairbanks (May 11 2020 at 20:57):

so an instance is basically a functor into the "category" of julia types and julia functions. You map every object to a julia type and every morphism to a julia function.

Evan Patterson (May 11 2020 at 20:57):

Sophie, the short version is that @instance is for regular Julia types and @syntax is for symbolic expressions.

James Fairbanks (May 11 2020 at 20:57):

oh yeah that is shorter than my version.

Evan Patterson (May 11 2020 at 20:58):

A long version is here :)

Sophie Libkind (May 11 2020 at 20:58):

Okay! So if I want to work with integers and functions between integers then I use an @instance macro and Julia will do the work of composition etc. for me

James Fairbanks (May 11 2020 at 20:58):

yeah

Sophie Libkind (May 11 2020 at 20:59):

vs. if I was to define a more abstract category then I use the @syntax macro and Catlab will keep track of all my expressions

James Fairbanks (May 11 2020 at 21:00):

yeah and you would often do both, like have a syntax where you express things symbolically and then have an instance where "real" computation happens.

James Fairbanks (May 11 2020 at 21:01):

like in the GLA case you want to use symbolic expressions to describe linear operators as composites of small linear operators and then you want to pick some matrices and solve some equations.

James Fairbanks (May 11 2020 at 21:03):

This file shows you a pretty complex example, https://github.com/epatters/Catlab.jl/blob/master/src/linear_algebra/GLA.jl

James Fairbanks (May 11 2020 at 21:03):

the instance comes from LinearMaps.jl which is like a lazy linear algebra library.

Evan Patterson (May 11 2020 at 21:06):

Another example says that wiring diagrams are an instance of symmetric monoidal categories.