Побочные результаты
Jan. 22nd, 2010 04:21 pmВ ходе трудов над статьёй для журнала Практика функционального программирования (по материалам этого поста) и параллельных размышлений над постом
beroal'а обнаружил следующий факт. Равенство

(UPD: В комментах велели добавить f : B → B′, h : A′ → A, g ↦ f . g . h. Добавляю.)
В категории Hask ковариантным Hom-функтором является левое сечение композиции (f .), а контравариантным - правое (. h). Соответственно указанное равенство описывает на другом языке коммутативность диаграммы.
Думаю скрыть этот факт от читателей статьи в журнале, но с читателями блога не могу не поделиться.
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
(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). Соответственно указанное равенство описывает на другом языке коммутативность диаграммы.
Думаю скрыть этот факт от читателей статьи в журнале, но с читателями блога не могу не поделиться.