deniok: (typed lambda)
[personal profile] deniok
В ходе трудов над статьёй для журнала Практика функционального программирования (по материалам этого поста) и параллельных размышлений над постом [livejournal.com profile] 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). Соответственно указанное равенство описывает на другом языке коммутативность диаграммы.

Думаю скрыть этот факт от читателей статьи в журнале, но с читателями блога не могу не поделиться.
This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 17th, 2025 03:14 pm
Powered by Dreamwidth Studios