Verites / verigraph

Software specification and verification system based on graph rewriting
https://verites.github.io/verigraph/
Apache License 2.0
37 stars 4 forks source link

Refactor FinitaryCategory Type Class #25

Open jsbezerra opened 7 years ago

jsbezerra commented 7 years ago

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.

jsbezerra commented 7 years ago

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

jsbezerra commented 7 years ago

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

ggazzi commented 7 years ago

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.

jsbezerra commented 7 years ago

It makes sense. We could use <&>

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

ggazzi commented 7 years ago

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.

jsbezerra commented 7 years ago

Updated

ggazzi commented 7 years ago

@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?

jsbezerra commented 7 years ago

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?

ggazzi commented 7 years ago

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).