“пересказал Бродского своими словами”
Кто живёт в разноязычных средах, тому наверняка знакома проблема, когда хочешь поделиться стихами, песней, да хотя бы шуткой на каком-то языке, которым собеседник не владеет, а в переводе уже не то. Да и не только в языке дело, культурный контекст нужен
( Read more... )
Въ качествѣ иллюстрацiи, вотъ у меня такой простой вопросъ. Есть функторы, а есть сильные функторы (strong functors). И вотъ пока что ни разу я не видѣлъ, чтобы на практикѣ, т.е. въ программированiи - насколько я понимаю, другой практики у функторовъ пока нѣтъ, - функторы были бы не сильные. Они всегда и вездѣ сильные. Программисту даже не надо изучать отдѣльно это понятiе, оно никогда не потребуется - просто у всѣхъ функторовъ есть свойство A × F[B] => F[A × B], написать кодъ для этой функцiи - простое упражненiе.
Однако, математики это понятiе формулируютъ и изучаютъ отдѣльно, причемъ въ большой общности (для любыхъ моноидальныхъ категорiй). А въ программированiи встрѣчаются только и исключительно моноидальныя категорiи, и операцiя (×) у нихъ всегда одна и та-же, такъ что изучать эти категорiи отдѣльно не требуется.
И вотъ нѣкiй математикъ придумалъ теорему о тонкихъ различiяхъ между нѣкими сильными и слабыми функторами въ нѣкихъ моноидальныхъ или не очень категорiяхъ. Однако теорема эта никакъ не связана съ реальной практикой, и объяснить ея программисту трудно или даже невозможно. Математикъ воспылалъ энтузiазмомъ по поводу этой теоремы, потому что она показываетъ, что... эээ... (дальше еще длинный потокъ словъ, никакъ не связанныхъ съ практикой). Психологически, математикъ испытываетъ чувство "красоты", но это обманъ, "багъ" мозга. Мозгъ, на своемъ какомъ-то глубоко подсознательномъ уровнѣ, думаетъ, что нашелъ новую вкусную ѣду. На самомъ дѣлѣ, эти теоремы безполезны, онѣ - не ѣда. Онѣ, скорѣе всего, и сегодня никому не нужны, и никогда въ будущемъ не понадобятся. Вѣроятность, конечно, есть, что когерентность или слабыя модельныя категорiи черезъ 50 лѣтъ для чего-то понадобятся, - вотъ, понадобились же (полвѣка спустя) функторы, конструктивная логика, и даже теорiя чиселъ. Но эта вѣроятность очень мала - и сегодня, во всякомъ случаѣ, дорога къ практикѣ совершенно не видна.
Поэтому и нельзя ничего объяснить неспецiалисту. Обычные достаточно умные люди будутъ думать примѣрно такъ, какъ говорилъ Хармсъ, - "[этотъ математикъ] знаетъ очень много, да все ерунду".
Мнѣ только жалко, что математики заняты такими вотъ вещами, а не болѣе важными для практики вопросами. Напримѣръ, монады придумали, а monad transformers такъ и не разобрались, какъ въ общемъ случаѣ дѣлать. А на практикѣ они нужны. Если у "спецiалистовъ" спросить объ этомъ, начинается невнятное бормотанiе про Eilenberg-Moore and Kleisli adjunctions, а четкаго отвѣта - какъ написать кодъ для monad transformer, если извѣстенъ кодъ данной монады, и всегда-ли это возможно - кажется, такъ и нѣтъ.
Другой вопросъ - почему функторъ (пишу на Хаскелѣ)
data P a = Empty | Pair a a
не является монадой, какъ ни старайся написать кодъ для return и join - законы монады не удовлетворяются. Этотъ функторъ - полиномiальный, очень простой, соотвѣтствуетъ полиному P(x) = 1 + x*x. То-же самое относится къ полиному P(x) = 1 + x*x*x. Доказательство тупое и длинное, переборомъ всѣхъ возможныхъ способовъ написать кодъ для return и join. Почему это происходитъ? Какъ понять, является ли данный полиномiальный эндофункторъ монадой? Нѣтъ отвѣта.
Или, скажемъ, parametricity theorem. Придумали сложную, запутанную теорiю, какiя-то relations, semantic frames, а для практическаго использованiя нужны четкiе шаги, какъ находить свойства naturality для данныхъ функцiй. А этого, какъ разъ, нигдѣ не написано.
Такое впечатленiе, что это имъ неинтересно или ниже достоинства витающихъ въ эмпиреяхъ математиковъ - давать четкiе отвѣты на практически важные, но непростые вопросы. Это не даетъ имъ понты въ ихъ частномъ клубѣ элитарныхъ спецiалистовъ-теоретиковъ.
Занялись бы дѣломъ, былъ бы хлѣбъ, и дѣтямъ было бы не стыдно разсказывать. ;)
Reply
Reply
А учебникъ Вашъ (въ любомъ видѣ) можно посмотрѣть? Если не хотите свѣтить ссылку, можно въ личку.
Reply
Reply
Reply
Reply
Если искать статьи про parametricity, то съ каждымъ годомъ онѣ становятся все заумнѣе и заумнѣе, въ то время какъ доказательство главной теоремы для самыхъ простыхъ случаевъ (polymorphic lambda calculus and System F) нигдѣ полностью въ деталяхъ не выписано. Ссылаются на старыя статьи Reynolds'a ("Types, abstraction and parametric polymorphism") и Wadler'a ("Theorems for free"), но тамъ нѣтъ всѣхъ деталей доказательствъ, а также нѣтъ четкаго рецепта, какъ по данной функцiи написать для нея "безплатную теорему".
А какъ насчетъ существованiя и единственности monad transformers? Монады придумали, а трансформеры изучать - уже не надо, что ли? Программисту надо знать, для любой ли монады существуетъ трансформеръ, и если существуетъ, то какъ написать необходимый для него кодъ. Отвѣта нѣтъ.
А какъ насчетъ критерiя о томъ, какой полиномiальный эндофункторъ можетъ быть монадой, а какой нѣтъ? Это чисто математическiй вопросъ, четко и просто поставленный, и при этомъ важный для практики. Почему этимъ никто не занимался никогда? Вѣдь это простѣйшiй, первѣйшiй вопросъ, который долженъ у всякаго спецiалиста возникать - мы только что дали опредѣленiе монады, вотъ теперь предположимъ, нѣкiй эндофункторъ заданъ явной формулой, - какъ я могу выяснить, является ли этотъ эндофункторъ монадой? Нѣтъ отвѣта.
Въ общемъ, возникаетъ ощущенiе, что математики работаютъ только для своихъ какихъ-то понтовъ и междусобойчиковъ. А если задача технически потруднѣе и поскучнѣе, и понтовъ не приноситъ, или если надо немного попотѣть и выписать детали доказательства, чтобы хотя бы кто-то другой могъ это прочитать и понять - то математику такое дѣлать уже неинтересно.
Reply
А в целом математика работает так, что серьёзный прогресс происходит только либо благодаря внутреннематематическим мотивациям, либо когда возникает потребность математически осмыслить новый раздел внешней естественной науки (обычно это двигателем была физика, но пару раз и информатика), а не от того что кто-то садится и начинает думать, чем бы ему таким попрактичнее заняться.
Reply
Reply
data P a = Empty | Pair a a
не можетъ быть сдѣланъ монадой. Это полиномiальный эндофункторъ, соотвѣтствующiй полиному P(x) = 1 + x*x, но для него нельзя опредѣлить функцiи return: a -> P a и join: P(P a) -> P a, удовлетворяющiя законамъ монады.
Доказательства этого были выписаны тутъ, https://stackoverflow.com/questions/49742377/
Reply
data P a = Empty | Pair a a
опредѣлить функцiи
return: a -> P a
join: P (P a) -> P a
удовлетворяющiя необходимымъ законамъ для монады. Этого сдѣлать нельзя. Доказательство пишется путемъ перечисленiя всѣхъ 50 возможныхъ способовъ написать кодъ для функцiй return и join. Это обсуждалось здѣсь, https://stackoverflow.com/questions/49742377/is-data-poe-a-empty-pair-a-a-a-monad и тамъ нѣсколько человѣкъ выписали и провѣрили доказательство.
Reply
Reply
Reply
Reply
Reply
Leave a comment