I’ve been playing/learning/working with Conal Elliott. During that time I’ve mainly used his category theory library: Felix. However it had a lot of Haskell influence and I’ve run into some troubles with it. Mainly due to the heavy use of instance arguments. Updating Agda was a pain, and I’ve run into instance resolution problems a lot.
Trying out agda-categories
I was motivated to use agda-categories to mitigate problems that I’ve run into using Felix. However its bundling categories properties (structure, or laws in Felix terms) with its operations (signatures, or Raw records in Felix). I think this is the most common convention right now in Agda. It was problematic because for my use case I am able to derive properties automatically. So this put some additional work (filling in the properties) that was discarded in the end.
In order to mitigate it I was hoping to just introduce Raw variants of
the category records. This is similar to some of the helper records
from agda-categories. Unfortunately the amount of additional code was
quite substantial, basically like separate category theory library.
This didn’t mitigate another problem with the fact that agda-categories structures are Setoid-enriched. This is similar problem to properties being entangled with categories records. Often times I’m able to derive the Equivalence relation automatically. If there is another one bundled with the category structure I was forced to discard one at times in order for stuff to work out.
Significant shift in my thinking came from James McKinna comment on Agda Zulip[fn:1]. In the Zulip message he also links the standard-library github issue which goes into much more detail into this design pattern(?). This set me free to break off the structure from the signatures, which is the thing this library does.
Other common problem is with structure hierarchy dependencies. If some structure depends on two other, and both of them have a common dependency, there is nothing to enforce that this common ancestor is the same in both of the direct dependencies.
Alternative approach is used in the Algebra.Bundles hierarchy of Agda standard library. Where there are no dependencies between records, but instead more powerful one contains all the definitions of it would be dependency. Those more powerful structures then define the would be dependency, so one can access the underlying structure.
Going other way is pretty convenient using building records from module names Agda feature.
I wanted this library to have the same organization and naming convention with agda-categories, when possible, so that perhaps other people will be able to navigate it more easily coming from agda-categories. However this can’t interfere with the goals above.
Cheshire uses nix to manage dependencies. One can get a working development environment, with appropriate version of Agda and required libraries/tools by executing:
nix develop
Development environment artifacts are available via cachix. In order to use them follow these instructions. But it is as simple as running:
cachix use famisoft
If the cachix binary is available.
[fn:1] It’s an amazing thread, I was struggling with this a lot when I’ve started my Agda adventure