Haskell Functor подразумеваемый закон

Question

Typeclassopedia говорит:

"Аналогичный аргумент также показывает, что любой экземпляр Functor, удовлетворяющий первому закону (fmap id = id), также автоматически удовлетворяет второму закону. На практике это означает, что нужно проверять только первый закон (обычно очень прямая индукция), чтобы убедиться, что экземпляр Functor действителен. "

Если это так, почему мы вообще упоминаем второй закон функторов?

Law 1: fmap id = id
Law 2: fmap (g . h) = (fmap g) . (fmap h)

Answer 1

Хотя я не могу дать доказательства, я считаю, что это говорит о том, что из-за параметричности система типов обеспечивает исполнение второго закона, пока действует первый закон , Причина для указания обоих правил заключается в том, что в более общей математической настройке у вас может быть некоторая категория C , где вполне возможно определить «отображение» из C для себя (т.е. пара эндофункций на Obj ( C ) и Hom ( C ) соответственно), который подчиняется первому правилу, но не подчиняется второму правилу и, следовательно, не является функтором.

Помните, что Functor s в Haskell являются эндофункторами в категории Hask , и даже все, что математически считается эндофунктором в Hask , может быть выражено в Haskell .. Ограничения параметрического полиморфизма исключают возможность указания функтора, который не ведет себя одинаково для всех объектов (типов), которые он отображает.

Исходя из этой цепочки , общий консенсус, по-видимому, заключается в том, что второй закон следует из первого для экземпляров Haskell Functor. Эдвард Кметт говорит ,

Учитывая fmap id = id, fmap (f . g) = fmap f . fmap g следует из свободного теорема для fmap.

Это было опубликовано в качестве отдельной статьи в газете давным-давно, но я забыл, где.

Answer 2

Используя seq, мы можем написать экземпляр, который удовлетворяет первому правилу, но не второму.

data Foo a = Foo a
    deriving Show

instance Functor Foo where
    fmap f (Foo x) = f `seq` Foo (f x)

Мы можем убедиться, что это удовлетворяет первому закону:

fmap id (Foo x)
= id `seq` Foo (id x)
= Foo (id x)
= Foo x

Однако это нарушает второй закон:

> fmap (const 42 . undefined) $ Foo 3
Foo 42
> fmap (const 42) . fmap undefined $ Foo 3
*** Exception: Prelude.undefined

Тем не менее, мы обычно игнорируем такие патологические случаи.

Answer 3

Я бы сказал, что второй закон упоминается не по причинам действительности, а скорее как важное свойство:

Первый закон гласит, что отображение функции идентификации для каждого элемента в контейнере не имеетэффект.Второй говорит, что сопоставление композиции из двух функций каждому элементу в контейнере такое же, как сначала сопоставление одной функции, а затем сопоставление другой.--- Typeclassopedia

(я не могу понять, почему этот первый закон подразумевает второй закон, но я не опытный Хаскеллер - это, вероятно, очевидно, когда вы знаете, что происходит)

Answer 4

Кажется, совсем недавно осознало, что закон 2 следует из закона 1. Таким образом, когда документация была первоначально написана, она, вероятно, считалась независимым требованием.

(Лично меня не убеждает этот аргумент, но, поскольку у меня не было времени самостоятельно проработать детали, я даю здесь преимущество сомнения.)