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). Соответственно указанное равенство описывает на другом языке коммутативность диаграммы.

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

Date: 2010-01-22 02:15 pm (UTC)
From: [identity profile] kodt-rsdn.livejournal.com
Сделай это врезкой в журнале. Типа, "знаете ли вы что" :)

Date: 2010-01-22 02:21 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Я подумаю над этой идеей :)

Date: 2010-01-31 10:08 am (UTC)
From: [identity profile] beroal.livejournal.com
оффтоп: А что, на RSDN ещё OpenID не сделали?

Date: 2010-01-22 02:54 pm (UTC)
From: [identity profile] migmit.vox.com (from livejournal.com)
То бишь, попросту то, что Hom - бифунктор.

Date: 2010-01-22 05:49 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
контравариантный по первому аргументу и ковариантный по второму, ага (если не привлекать двойственных категорий)

Date: 2010-01-23 11:36 am (UTC)
From: [identity profile] nivanych.livejournal.com
Такие бифункторы на nLab называют профункторами.
Реже дифункторами (видимо, по аналогии с диестественным пр-нием).
Но под бифунктором, как правило, насколько я видел,
понимается ковариантный по обоим аргументам.

Date: 2010-01-31 10:22 am (UTC)
From: [identity profile] beroal.livejournal.com
Это тоже не очевидно, а доказательство выльется в ещё один пост. :)

Date: 2010-01-31 11:07 am (UTC)
From: [identity profile] migmit.vox.com (from livejournal.com)
А этого поста будет не достаточно?

Date: 2010-01-22 06:42 pm (UTC)
From: [identity profile] kurilka.livejournal.com
Я может глупость спрошу, но где на диаграмме Hom(A, -) ну и Hom(-, B)?
Читал вики, ничо не понял...

Date: 2010-01-22 06:57 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
На диаграмме они инстанцинированны на произвольной паре стрелок f : B → B′ и h : A′ → A. Ну это как в Хаскелле - мы можем рассуждать о map :: (a → b) → ([a] → [b]), а можем о map f :: [a] → [b] для произвольного f :: a → b. В первом случае мы могли бы написать (map -) используя категорийную терминологию.

Date: 2010-01-22 07:32 pm (UTC)
From: [identity profile] kurilka.livejournal.com
Т.е. "-" - это такой специальный плейсхолдер в ТК чтоли?

Date: 2010-01-22 07:36 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
ага, типа _ в Хаскелле

Date: 2010-01-23 11:33 am (UTC)
From: [identity profile] nivanych.livejournal.com
_ в хаскеле означает независимость от аргумента.
В Hom(A,-) чёрточка, как раз, означает аргумент.

Date: 2010-01-23 12:05 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Да, согласен, аналогия плохая, слишком приблизительная

Date: 2010-01-31 10:18 am (UTC)
From: [identity profile] beroal.livejournal.com
Я предпочитаю запись с помощью лямбда-абстракции:
Hom(A,−)λB. Hom(A,B)
Hom(−,B)λA. Hom(A,B)

Date: 2010-01-31 10:31 am (UTC)
From: [identity profile] nivanych.livejournal.com
С одной стороны, не могу не согласиться
с тем, что такая запись выглядит чётче,
но с другой стороны, запись Hom(A,-)
весьма и весьма устоявшаяся.

Date: 2010-01-31 03:41 pm (UTC)
From: [identity profile] kurilka.livejournal.com
ну да, прочерки как-то совсем неинтуитивны, да и вообще первый раз вижу (правда в ТК я всё в первой половине книжек застреваю)

Date: 2010-01-22 07:07 pm (UTC)
From: [identity profile] ivan-gandhi.livejournal.com
Приятно, конечно, до чего компьютерная наука дошла; но это как бы очевидно для всякого категорщика, и, должно быть, совершенно загадочно для некатегорщика.

Надо поправить диаграмму или довасить комментарий, мол, h:A'->A, f:B->B'.

g |-> f.g.h

Date: 2010-01-22 07:10 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Не, ну что профессиональные категорщики - небожители, это и так понятно; но благожелательным массам-то на примерах тоже полезно пояснять ;-)

Date: 2010-01-24 04:59 am (UTC)
From: [identity profile] ivan-gandhi.livejournal.com
На примерах - это прекрасно; так и надо.
(deleted comment)

Date: 2010-01-22 07:17 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Я сам очень испуган, но уважаемая редакция сама попросила. Попробую не подвести :)

Date: 2010-01-23 06:55 pm (UTC)
From: [identity profile] nivanych.livejournal.com
Строго говоря, это не Hom, а экспонента.
Ну или ещё сопряжённый к лампочке
в моноидально-замкнутой категории
называют internal hom.

Date: 2010-01-31 10:27 am (UTC)
From: [identity profile] beroal.livejournal.com
Но диаграмма верна и для external hom.

Date: 2010-01-31 10:44 am (UTC)
From: [identity profile] nivanych.livejournal.com
Это другой вопрос, щас начнём его обсуждать,
продолжим про обогащённые категории,
и можем уйти в приличные дебри ;-)

Date: 2010-01-31 10:23 am (UTC)
From: [identity profile] beroal.livejournal.com
|→
В Unicode есть такой значок

Date: 2010-01-31 12:27 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
thnx, мне лень искать было, сейчас поправлю

Be ready for that special moment. Day or night.

Date: 2012-08-22 05:07 am (UTC)
From: (Anonymous)
BUY ONLINE! BEST GENERIC! VIAGRA, CIALIS, LEVITRA!!!
Save BIG on genuine Viagra, Cialis, Levitra, plus:

-100% genuine meds - no imitations!
-Discount prices - up to 65% off storewide
-Easy refunds!
-Safe and confidential orders



[b]CLICK HERE - http://mothershare.net/ [/b]


BONUS!!! TODAY ONLY!

http://mothershare.net/

[url=http://mothershare.net/][img]http://pharmshoper.com/images2/generic-pharmacy.jpg[/img][/url]

Profile

deniok: (Default)
deniok

February 2022

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

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 12th, 2025 09:28 am
Powered by Dreamwidth Studios