[Haskell-cafe] Haskell function composition commutivity?
Viktor Dukhovni
ietf-dane at dukhovni.org
Tue Apr 13 17:06:41 UTC 2021
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.
More information about the Haskell-Cafe
mailing list