Haskell function composition commutivity?

newer
Generalized, named, and exportable...

Galaxy Being

13 Apr 2021 13 Apr '21

12:30 p.m.

I'm in chapter 4 of Bird's very interesting *Thinking Functionally with Haskell *and he has a problem at the end of the chapter where he lists these equations map f . take n = take n . map f map f . reverse = reverse . map f map f . sort = sort . map f map f . filter p = map fst . filter snd . map (fork (f,p)) filter (p . g) = map (invertg) . filter p . map g reverse . concat = concat . reverse . map reverse filter p . concat = concat . map (filter p) adding this caveat for the 3rd equation iff x <= y <=> f x <= f y and this for the 4th equation fork (f,g) x = (f x, g x) and for the 5th invertg satisfies invertg . g = id My confusion is over the commutative-ness of most of this but only anecdotally. With the particularly dense map f . filter p = map fst . filter snd . map (fork (f,p)) We have

...

:t (map myF . filter myP) Integral b => [b] -> [b] :t (map fst . filter snd . map (myFork (myF,myP))) Integral b => [b] -> [b]

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

Attachments:

attachment.html (text/html — 2.5 KB)

Show replies by date

Viktor Dukhovni

13 Apr 13 Apr

1:06 p.m.

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.

Viktor Dukhovni

1:29 p.m.

On Tue, Apr 13, 2021 at 01:06:41PM -0400, Viktor Dukhovni wrote:

...

- Yoneda Lemma: Given a functor f and some function `foo` with signature:

foo :: forall a. (a -> b) -> f b

Sorry, typo, should be: foo :: forall b. (a -> b) -> f b -- Viktor.

Tom Smeding

2:02 p.m.

(Viktor: sorry for the duplicate...) Does it make a difference? To me the following function type signatures mean exactly the same thing: foo :: (a -> b) -> f b foo :: forall a. (a -> b) -> f b foo :: forall b. (a -> b) -> f b foo :: forall a b. (a -> b) -> f b This of course changes when the `forall` is put inside the parentheses (though I don't think you meant that -- but I'm not a category theorist), or if ScopedTypeVariables is used nontrivially, or... etc. Although, because of the fact that you omitted 'Functor f =>' and instead chose to write the constraint in prose beforehand, I get the feeling that you may be speaking mathematically, not about Haskell as compiled by GHC. - Tom On 13/04/2021 19:29, Viktor Dukhovni wrote:

...

On Tue, Apr 13, 2021 at 01:06:41PM -0400, Viktor Dukhovni wrote:

...
- Yoneda Lemma: Given a functor f and some function `foo` with signature:

foo :: forall a. (a -> b) -> f b

Sorry, typo, should be:

foo :: forall b. (a -> b) -> f b

-- Viktor. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Viktor Dukhovni

2:14 p.m.

...

On Apr 13, 2021, at 2:02 PM, Tom Smeding wrote:

Although, because of the fact that you omitted 'Functor f =>' and instead chose to write the constraint in prose beforehand, I get the feeling that you may be speaking mathematically, not about Haskell as compiled by GHC.

Yes, mathematically, with Haskell-like syntax. Also the functors in question were intended to stand for specific functors, rather than be universally quantified. So perhaps better: Yoneda (with A some type and F some functor): foo :: forall b. (A -> b) -> F b <=> foo bar = fmap bar (foo (id @A) -- Viktor.

Galaxy Being

3:19 p.m.

Your answers seem to originate outside of normal Haskell tutorials. Where can I start with this higher superset theory? On Tue, Apr 13, 2021 at 1:19 PM Viktor Dukhovni wrote:

...

...
On Apr 13, 2021, at 2:02 PM, Tom Smeding wrote:

Although, because of the fact that you omitted 'Functor f =>' and instead chose to write the constraint in prose beforehand, I get the feeling that you may be speaking mathematically, not about Haskell as compiled by GHC.

Yes, mathematically, with Haskell-like syntax. Also the functors in question were intended to stand for specific functors, rather than be universally quantified.

So perhaps better:

Yoneda (with A some type and F some functor):

foo :: forall b. (A -> b) -> F b

<=> foo bar = fmap bar (foo (id @A)

-- Viktor.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Viktor Dukhovni

5:37 p.m.

On Tue, Apr 13, 2021 at 02:19:46PM -0500, Galaxy Being wrote:

...

Your answers seem to originate outside of normal Haskell tutorials. Where can I start with this higher superset theory?

There's a reason why the tutorials don't cover this, the categorical foundations of Haskell types are not beginner material. It is perhaps best to defer going down this rabbit hole until you're more comfortable with the Haskell generally. You could start with: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-p... https://bartoszmilewski.com/2015/04/07/natural-transformations/ For the Yoneda Lemma specifically, I'd recommend: http://blog.sigfpe.com/2006/11/yoneda-lemma.html Parametricity is covered in "Theorems for free": https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf but it is by no means elementary, though skimming it for the essential facts and skipping the gory details is not too difficult. You could also read "Categories for the Working Mathematician" by Saunders Mac Lane. -- Viktor.

1498

Age (days ago)

1498

Last active (days ago)

List overview

Download

6 comments

3 participants

participants (3)

Galaxy Being
Tom Smeding
Viktor Dukhovni