verigraph icon indicating copy to clipboard operation
verigraph copied to clipboard

Refactor FinitaryCategory Type Class

Open jsbezerra opened this issue 7 years ago • 9 comments

Refactor the Morphism type class, renaming it to FinitaryCategory to better match its responsabilities.

At the same time, implement @ggazzi's suggestion of using a Context Monad to store important information about the category, such as the type graph of a TGraph and the type graph and NAC strategy of a TSpan.

  • [x] Rename Morphism to FinitaryCategory
  • [ ] Add a "context monad" to the type classes
  • [x] Flip the arguments of compose and add an alias (<&>)
    • [ ] To do the same thing for Data.Relation ?
  • [x] ~~Integrate FindMorphism into FinitaryCategory~~

jsbezerra avatar May 08 '17 00:05 jsbezerra

This will cause a major API change, so we need to discuss this better.

jsbezerra avatar May 08 '17 01:05 jsbezerra

Question: should we also change the order of paramaters in the compose function to reflect exactly the category operator?

jsbezerra avatar May 08 '17 15:05 jsbezerra

In this case it might even make sense to use some sort of operator for morphism composition. Clearly we can't use (.) which is already function composition.

One possibility would be to define an instance of the Semigroup class, so we could use the (<>) operator. I don't think this would fit, though, since some morphisms aren't actually composable so it might violate the laws of the Semigroup class.

Otherwise, we need to find an operator that is not too noisy and doesn't clash with common Haskell libraries.

ggazzi avatar May 08 '17 16:05 ggazzi

It makes sense. We could use <&>

https://www.haskell.org/hoogle/?hoogle=%3C%26%3E

jsbezerra avatar May 08 '17 16:05 jsbezerra

The name FinitaryCategory would be technically more appropriate than FiniteCategory. A finitary category where each object is finite (i.e. has a finite number of subobjects), but the number of objects may be infinite.

ggazzi avatar May 08 '17 19:05 ggazzi

Updated

jsbezerra avatar May 09 '17 04:05 jsbezerra

@lm-rodrigues once suggested to me that FindMorphism might be unnecessary, since all instances of Morphism should also implement FindMorphism. I think this is even more true of FinitaryCategory: since the objects are finite, finding morphisms between them is definitely decidable.

How about we integrate FindMorphism into FinitaryCategory?

ggazzi avatar May 09 '17 13:05 ggazzi

About the integration of FindMorphism and FinitaryCategory:

What would be the case for the Category Graph, which today only implements FinitaryCategory?

Should we also implement FindMorphism for it (even though we do not use it) or should we leave it unimplemented and raise and error accordingly?

jsbezerra avatar May 22 '17 19:05 jsbezerra

Good point. As it stands, I think it would be best to keep these type classes separate, since they do express separate concerns (the "definition" of a finitary category is independent of the algorithms for finding morphisms between its objects).

ggazzi avatar May 22 '17 20:05 ggazzi