Побочные результаты

[deniok]

В ходе трудов над статьёй для журнала Практика функционального программирования (по материалам этого поста) и параллельных размышлений над постом beroal'а обнаружил следующий факт. Равенство

(f .) . (. h) = (. h) . (f .)

вылезшее в этом комментарии из преобразований

f (g (h x)) = (f . (g . h)) x = ((f .) ((. h) g)) x = ((f .) . (. h)) g x
f (g (h x)) = ((f . g) . h) x = ((. h) ((f .) g)) x = ((. h) . (f .)) g x

имеет явную категорийную интерпретацию. А именно, указанное равенство выражает (в категории Hask) факт естественной связи Hom-функторов: ковариантного Hom(A,–) и контравариантного Hom(–,B), задаваемой коммутативной диаграммой



(UPD: В комментах велели добавить f : B → B′, h : A′ → A, g ↦ f . g . h. Добавляю.)

В категории Hask ковариантным Hom-функтором является левое сечение композиции (f .), а контравариантным - правое (. h). Соответственно указанное равенство описывает на другом языке коммутативность диаграммы.

Думаю скрыть этот факт от читателей статьи в журнале, но с читателями блога не могу не поделиться.

Comments

[kurilka.livejournal.com]

Я может глупость спрошу, но где на диаграмме Hom(A, -) ну и Hom(-, B)?
Читал вики, ничо не понял...

[deni-ok.livejournal.com]

На диаграмме они инстанцинированны на произвольной паре стрелок f : B → B′ и h : A′ → A. Ну это как в Хаскелле - мы можем рассуждать о map :: (a → b) → ([a] → [b]), а можем о map f :: [a] → [b] для произвольного f :: a → b. В первом случае мы могли бы написать (map -) используя категорийную терминологию.

[kurilka.livejournal.com]

Т.е. "-" - это такой специальный плейсхолдер в ТК чтоли?

[deni-ok.livejournal.com]

ага, типа _ в Хаскелле

[nivanych.livejournal.com]

_ в хаскеле означает независимость от аргумента.
В Hom(A,-) чёрточка, как раз, означает аргумент.

[deni-ok.livejournal.com]

Да, согласен, аналогия плохая, слишком приблизительная

[beroal.livejournal.com]

Я предпочитаю запись с помощью лямбда-абстракции:

Hom(A,−)	λB. Hom(A,B)
Hom(−,B)	λA. Hom(A,B)

[nivanych.livejournal.com]

С одной стороны, не могу не согласиться
с тем, что такая запись выглядит чётче,
но с другой стороны, запись Hom(A,-)
весьма и весьма устоявшаяся.

[kurilka.livejournal.com]

ну да, прочерки как-то совсем неинтуитивны, да и вообще первый раз вижу (правда в ТК я всё в первой половине книжек застреваю)