idris-ct
idris-ct copied to clipboard
statebox
free strict symmetric monoidal category
@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?
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.
@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
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.