free strict symmetric monoidal category

[marcosh]

No description provided.

[fredrikNordvallForsberg]

These postulates makes it possible to prove false:

oops : Void
oops = constructorsDisjoint (freeLeftIdentity [] [] (MkIdFreeMorphism []))
  where
    DistinguishThem : FreeMorphism () [] [] [] -> Type
    DistinguishThem (MkIdFreeMorphism []) = Void
    DistinguishThem _                     = ()
    constructorsDisjoint : MkCompositionFreeMorphism {t = ()} {generatingMorphisms = []} (MkIdFreeMorphism []) (MkIdFreeMorphism []) = (MkIdFreeMorphism []) -> Void
    constructorsDisjoint p = replace {P = DistinguishThem} p ()

What you need to pursue this approach is some form of quotient type, which Idris unfortunately doesn't support.

But maybe there is some clever way to construct the free strict monoidal category explicitly, e.g. the free category on a graph can be constructed as the transitive closure of the edge relation (in other words, a morphism is a list of edges), which gives you the category laws for free, instead of having to quotient by them explicitly.

[FabrizioRomanoGenovese]

This is fucked :( Do you have a reference for building free cats over graphs? Are you referring to the same construction one can find, say, on MacLane?

Also, should it be possible to generalize to monoidal categories by using hypegraphs as generators? :)

[fredrikNordvallForsberg]

I don't have access to MacLane at the moment, but it's probably the same construction. The nlab is quite explicit, and has further references:
https://ncatlab.org/nlab/show/path+category

From a type theory point of view, what is nice with this construction is that it is only involving free concepts (that hence can be implemented by inductive definitions), with no need to quotient. Compare with the construction of the free monoid, which is a very similar situation. I'll have to think about if hypergraphs would work. My immediate concern would be that we now also have to introduce morphisms not only from compositions of previously introduced ones, but also by applying the functoriality of the tensor, which I fear would need something more than just paths of edges.

[WhatisRT]

I've dealt with similar issues a lot in Coq and Agda. I don't know if the path category approach works, but there are several ways to deal with the issue that quotient types don't exist.

In this scenario, I would postulate the existence of the quotient type locally. I.e. keep the type FreeMorphism as it is but rename it to PreFreeMorphism, and then postulate the existence of a new type FreeMorphism together with a map quot : PreFreeMorphism ... -> FreeMorphism ..., such that the type FreeMorphism has exactly the structure that we want (i.e. the map is surjective, and quot x = quot y if and only if they are of the forms as described by the postulates here). This is for example how real numbers are implemented in Coq.

Alternatively, one could deal with setoids, but everytime I did I regretted it big time.

[FabrizioRomanoGenovese]

My gut feeling is that trying to go with what Fred said, but using hypegraphs, is probably worth trying first. If this experience has taught me something it is that postulate is a very dangerous construct to use. So if there's a way of giving definitions which avoids it completely, I'd gladly go for it.

In addition to it, Petri nets can clearly be seen as hypegraphs, where places are vertexes and transitions are hyperedges. Generating a free smc from an hypegraph should basically be exactly what we want (you have to add symmetries but I don't want to think about this right now :) )

[marcosh]

yes, I guess they are practically the same approach. This is just a concrete implementation

[FabrizioRomanoGenovese]

Well then we know that at least two people in the team like this now!
Anyway, if this fixes it, go for it. Nevertheless, I'd consider it more of a momentary fix that a definitive thing: If we can get stuff done in terms of free compositions of other structures I'd feel way better :)

[WhatisRT]

In principle, other than using setoids this is the only solution in Idris, so if you consider this to be only a temporary fix, we either have to make large changes (like switching to a language that supports quotients or using setoids everywhere), or we have to give a quotient type explicitly.

In this scenario, there might actually be a reasonable way to do this. As long as the sets of generators are finite, the set of objects should be countable infinite and the set of morphisms between two objects should be finite (I haven't given much thought to it, maybe it is possible that some are coubtably infinite?). Thus, it should be possible to figure out the size of all the required types, and you would be able to construct something that is isomorphic to the quotient you want, without using postulates. That would be much more work though.

As an alternative, Agda 2.6 supports cubical type theory, so in particular quotient inductive types. Translating Idris code to Agda is reasonably quick and I have already translated everything in the Basic directory. So we could just postulate that the quotients exist in a different file, and then have an Agda copy of that file where we just add the definition of the quotient we want and replace the postulates by theorems there. If it's just a definition of that one quotient, it's unlikely that that will change, so it shouldn't be a maintenance problem.

[FabrizioRomanoGenovese]

Did you read my previous comments in terms of free structures? Why do you think it is not possible to do anything like this? It works for the path category, do you have elements to affirm there is no possible construction of FSSMCS in terms of free structures?

[WhatisRT]

To recap what we've decided in the meeting: It seems best to use postulates right now, to just give us the existence of the type we need. I think the proposal by @marcosh is a great start, but it should be done in such a way that the implementation of FSSMCS is parametrized over the implementation of the quotient. This would mean that whenever we find a good way to construct the type we need without postulates, we can just change a single line of code to switch between the implementation with postulates and any other implementation. Afterwards, we can decide how to tackle the implementation of that type, either via a subtype using normal forms, doing some random stuff with isomorphisms or by getting some of @FabrizioRomanoGenovese's ideas to work.

[marcosh]

@WhatisRT @fredrikNordvallForsberg @FabrizioRomanoGenovese I pushed an update to this, which should solve the issue raised by Fredrik. Could you please take a look at it again and check it this could work?

[WhatisRT]

I think it looks good, but I'm thinking that it might be a good idea to export PreFreeMorphism together with its constructors. There might be things that don't require quotienting, and those might be easier to work with if one has access to the type, including constructors. The important part is that the constructors of FreeMorphism aren't visible.

In case that export would also expose the constructors for FreeMorphism, one could wrap a single (private) constructor around PreFreeMorphism to turn it into a FreeMorphism.

[marcosh]

@WhatisRT I'm not sure exporting PreFreeMorphism and its constructors is a good idea. I thought about it as just an implementation detail which needs to be hidden from the end user.

Do you have in mind any example or use case where it could be useful to actually export it?

In any case we could just postpone this decision and write a comment above the definition which states that, if needed PreFreeMorphism, could be made public

[WhatisRT]

Ok, I've realized that the functions provided already enable writing morphisms in the FSSMC. It might still be a good idea to expose the PreFreeMorphism type, for convenience. Right now, one has to use 5 functions to build a morphism, that aren't really tied together. If PreFreeMorphism is exposed, those 5 functions could be combined into a single quotient map, and then one could build the morphism with just constructors, and apply one quotient map at the end. But maybe this is just me thinking too much.

[WhatisRT]

So this seems to implement a symmetric monoidal category given a category (which can probably be turned into a free functor from categories to symmetric monoidal categories?), but I think if you want to get strictness from that, you need quotients...
To start off from generators and relations, you probably need to turn the generators and relations into a graph, then take the associated category, and then apply this construction.