[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