On Tue, Apr 13, 2021 at 11:30:10AM -0500, Galaxy Being wrote:
Is there anything universal to be drawn from these anecdotal examples of seeming commutativity? My breakdown of the third equation shows the same type definition for both sides. Is this a way to find equality? All in all, Bird doesn't indicate that there are any underlying truths, just "almost" commutativity.
Yes, but the answer is likely some combination of parametricity and the Yoneda Lemma. - Parametricity: Given two fuctors f and g and some function `foo` with type signature: foo :: forall a. f a -> g a we can conclude that `foo` is a "natural transformation", which means that for all functions `bar`, we have: foo . fmap bar = fmap bar . foo - Yoneda Lemma: Given a functor f and some function `foo` with signature: foo :: forall a. (a -> b) -> f b we can conclude that for all `bar :: a -> b`: foo bar = fmap bar (foo id) It is interesting that you used the word "universal", because that's the right word to describe some of the underlying category theory notions. -- Viktor.