Breaking only the second Functor law

david-christiansen · October 11, 2022, 5:55pm

In Haskell, instances of Functor are expected to satisfy two laws:

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

It occurred to me last night that I can’t think of a ready example of a Functor instance that violates the second law, but not the first one. There are plenty of ways to violated the first, like:

instance Functor [] where
  fmap f _ = []

instance Functor [] where
  fmap f xs = map f (reverse xs)

instance Functor [] where
  fmap f [] = []
  fmap f (x : xs) = f x : f x : map f xs

But I was unable to come up with a functor instance for a datatype that satisfies the identity law but not the composition law. I suspect that I’m just insufficiently devious, but does anyone have a good example?

Bodigrim · October 11, 2022, 6:08pm

github.com

quchen/articles/blob/master/second_functor_law.md

The second `Functor` law is redundant
=====================================

Basic Haskell teaches that instances of `Functor` should satisfy

```haskell
fmap id = id                   -- fmap preserves identity
fmap f . fmap g = fmap (f . g) -- fmap distributes over composition
```

However, Haskell's type system is special in a way that makes the second law
follow from the first one. The values of *every* type follow a certain law;
this law is called the free theorem of that type. For example, the free theorem
of `f :: [a] -> [a]` is

```haskell
map g . f  = f . map g
```

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

This file has been truncated. show original

david-christiansen · October 11, 2022, 6:10pm

This is just what I was looking for, and it explains why I had a hard time finding an example. Thank you!

EdmundsEcho · October 12, 2022, 3:59pm

I might not add much to the formal expression of the situation, but a less formal way I intuited the “power” of Functor was by thinking about “what information” the implementation of Functor requires (said, differently, how does the information encoded in the implementation of Functor augment the system).

The quick answer is that it doesn’t. The type is a Functor regardless of whether a programmer chose to implement the type class. In other words, it’s an inherent property of a subset of types “out there”. It’s an interpretation that requires a little blurring of the eyes. Notwithstanding, I hold to this view because when given that a type can be known by it’s constructor, a generic truth in a few computing contexts, it so happens to be precisely what is required to implement Functor. The “subset” nature of Functor comes from the fact that is is not just any old constructor, but a type constructor.

The programmatic “job” of implementing a Functor requires the information required to both deconstruct and reconstruct the value. An implementation of Functor must host the type constructor logic that is what makes a type a Functor; one in the same. That “promise” to deconstruct and re-construct the value without distorting the payload, is accomplished with the first law.

I suspect the statement:

… lies in the fact that in the “computing” context and in any language where the type aligns with the its constructor (so where there can only be one constructor for a given value), we get the second law for free.

Does that mean the only context in which we need to demonstrate the second law is one in which the interaction between the type constructor and the value of the payload is not “linear”/constant?