Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The second Functor law is redundant is not proper #35

Closed
HuStmpHrrr opened this issue Feb 25, 2016 · 3 comments
Closed

The second Functor law is redundant is not proper #35

HuStmpHrrr opened this issue Feb 25, 2016 · 3 comments

Comments

@HuStmpHrrr
Copy link

in the article,

  fmap f . fmap g
= fmap id . fmap (f . g) <-- how this one comes?
= id . fmap (f . g)      -- by the first functor law
= fmap (f . g)

the derivation is problematic and therefore it derives a improper conclusion.

also,

This means that any function f of type [a] -> [a] commutes with map

are you sure this one is true?

let g = (2*)
let f = filter (>10)

apparently map g . f /= f. map g.

@roboguy13
Copy link

Regarding your second point, f doesn't have the type [a] -> [a], it has the type (Num a, Ord a) => [a] -> [a]. All functions with the type forall a. [a] -> [a] have the stated property.

The reason this property holds is that a function with the type forall a. [a] -> [a] cannot examine the items in the list (it must work for all types a). As a result, the list it gives back can only contain items from the list given to it (although the list structure can be different, it cannot have different items or make choices about the list structure based on the specific properties of any of the items).

That property of map is the free theorem of map. The breakthrough paper on free theorems is Philip Wadler's Theorems for free! (although it uses somewhat outdated notation by today's standards). This particular property of map is described in the first part of the introduction and section 3.5 elaborates on the usefulness of using that property to think about map.

@roboguy13
Copy link

For the first point, we can use the free theorem (this is a key part of the proof):

        f .      g =      p .      q
=> fmap f . fmap g = fmap p . fmap q

This lets us turn any equation of the form f . g = p . q into an equation fmap f . fmap g = fmap p . fmap q.

For the precondition in that implication, first we note that this equation holds

        f .      g =      (f . g) .      id

Then we let p = (f . g) and q = id, plug this into the free theorem and end up with

        f .      g =      (f . g) .      id
=> fmap f . fmap g = fmap (f . g) . fmap id

This can be simplified, using fmap id = id to

   fmap f . fmap g = fmap (f . g) . id

and simplified again using the identity law h . id = h, to

   fmap f . fmap g = fmap (f . g)

(This is the same proof as the one in the article, worded in a slightly different way.)

@quchen
Copy link
Owner

quchen commented Feb 27, 2016

Thanks @roboguy13 for answering :-)

5dd82fe adds a short remark in order to clarify the first question.

@quchen quchen closed this as completed Aug 10, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants