Бесплатная теорема для fmap

Question

Рассмотрим следующую оболочку:

      newtype F a = Wrap { unwrap :: Int }

Я хочу опровергнуть (в качестве упражнения, чтобы осмыслить этот интересный пост ), что существует законный Functor F экземпляр, который позволяет нам применять функции Int -> Intвведите фактическое содержимое и ~ игнорируйте ~ все другие функции (т.е. fmap nonIntInt = id).

Я считаю, что это должно быть сделано с помощью бесплатной теоремы для fmap: для данного f, g, h а также k, так что g . f = k . h: $map g . fmap f = fmap k . $map h, где $mapэто естественное отображение для данного конструктора.

Что определяет естественную карту? Правильно ли я полагаю, что это простой flip const для ?

Насколько я понимаю: $map f это то, что мы обозначаем как Ffв теории категорий. Таким образом, в категориальном смысле мы просто хотим, чтобы что-то среди строк следующей диаграммы коммутировало:

Пока не знаю, что поставить вместо ???s (то есть какой функтор мы применим, чтобы получить такую ​​диаграмму и как мы обозначим это почти - ?).

Итак, что такое естественная карта в целом и для F? Какая правильная диаграмма для fmapбесплатная теорема?

Answer 1

Итак, мы развлекаем функцию m :: forall a b . (a->b) -> F a -> F b такое, что (среди прочего)

      m (1 +)    (Wrap x) = (Wrap (1+x))
m (show)   (Wrap x) = (Wrap x)

Здесь есть два связанных между собой вопроса.

1. Может ли человек с хорошим поведением это сделать?
2. Может ли это сделать параметрическая функция?

Ответ на оба вопроса - «нет».

Человек с хорошим поведением не может этого сделать, потому что должен подчиняться аксиомам. Независимо от того, является ли наша среда параметрической или нет. Аксиома Functor говорит, что для всех функций a а также b, fmap (a . b) = fmap a . fmap b должен держаться, и это не для a = show а также b = (1 +). Так что нельзя вести себя хорошо.

Параметрическая функция не может этого сделать, потому что это то, что говорит теорема параметричности. При просмотре типов как отношений между терминами связанные функции принимают связанные аргументы для связанных результатов. Легко увидеть, что m не справляется с параметризацией, но на него легче смотреть m': forall a b. (a -> b) -> (Int -> Int)(эти два могут быть тривиально преобразованы друг в друга). связано с, поскольку является полиморфным по своему аргументу, поэтому различные значения аргумента могут быть связаны любым отношением. Функции - это отношения, и существует функция, которая отправляет (1 +) к show. Однако тип результата не имеет переменных типа, поэтому он соответствует постоянному отношению (его значения связаны только сами с собой). Поскольку каждое значение, включая m' относится к самому себе, из этого следует, что все параметрические функции m :: forall a b. (a -> b) -> (Int -> Int) должен подчиняться m f = m g, т.е. они должны игнорировать свой первый аргумент. Что интуитивно очевидно, поскольку не к чему его применять.

Фактически можно вывести первое утверждение из второго, заметив, что хорошее поведение должно быть параметрическим. Таким образом, даже если язык допускает непараметрию, fmap не может использовать его нетривиально.