|
| |||
|
|
Почему и когда теорiя категорiй полезна для программированiя (Развернутая версiя комментарiевъ здѣсь https://www.dreamwidth.org/go?redir_type=t 1. Разсмотримъ какой-либо языкъ программированiя, гдѣ есть "типы данныхъ" (Int, Float, String, Boolean, Array of String, ...) и они провѣряются при компиляцiи, чтобы функцiи никогда не могли быть вызваны съ аргументомъ неправильнаго типа. 2. Каждому такому языку программированiя сопоставимъ категорiю, опредѣляемую слѣдующимъ образом. Объекты - это всѣ типы данныхъ, поддерживаемыхъ языкомъ программированiя. Т.е. въ этой категорiи будетъ объект Int, объектъ String, объектъ Boolean, объектъ "Array of String", и т.д. Морфизмы - это всѣ функцiи однаго аргумента, которыя можно запрограммировать на данномъ языкѣ программированiя. Морфизмъ между объектами A и B это какая-либо функцiя съ аргументомъ типа A и возвращающая значенiе типа B. Напримѣръ, какiе есть морфизмы между объектами Boolean и Int? Это функцiи съ булевымъ аргументомъ и цѣлымъ числомъ въ качествѣ результата. Такихъ функцiй столько же, сколько паръ цѣлыхъ чиселъ. Вотъ, значитъ, получаемъ довольно много всякихъ морфизмовъ. Аксiомы категорiи выполнены, потому что (1) всегда существуетъ тождественный морфизмъ A -> A, т.е. функцiя, берущая аргументъ типа А и возвращающая это же значенiе. На любомъ языкѣ легко написать кодъ для тождественной функцiи: function(x) { return x } или что-то въ этомъ родѣ. (2) Функцiи подходящихъ типовъ можно примѣнять одну за другой къ аргументу, и получится композицiя морфизмовъ. Сначала примѣнить функцiю A -> B къ аргументу типа А, получить значенiе типа В. Потомъ примѣнить функцiю B -> C, получится значенiе типа С. Значитъ, получилась функцiя A -> C. Кодъ для этой функцiи можно легко написать, значитъ этотъ морфизмъ существуетъ. (3) Композицiя функцiй ассоцiативна и тождественная функцiя работаетъ правильно въ композицiи. Вотъ и все, категорiю мы опредѣлили. Теперь будемъ съ ней работать, намъ почти никогда не понадобятся какiя-либо другiя категорiи. Можемъ на основѣ этой категорiи опредѣлить другiя вспомогательныя категорiи, напримѣръ обратную къ данной, или категорное произведенiе двухъ копiй данной категорiи. Или категорiю эндофункторовъ этой категорiи. Но всегда главной явлется именно категорiя "типы / функцiи", которую мы опредѣлили. 3. Что такое эндофункторъ въ такой категорiи? Это отображенiе типовъ и одновременно отображенiе морфизмовъ. Хорошiй примѣръ эндофунктора - это типъ данныхъ "Array". Въ нѣкоторыхъ языкахъ программированiя можно обобщить такой типъ на "Array of Х", гдѣ Х - произвольный типъ данныхъ. Тогда "Array" можно понимать какъ отображенiе изъ типовъ въ типы. Изъ Boolean -> въ Array of Boolean, изъ Array of String -> въ Array of Array of String, и т.д. Для эндофунктора, кромѣ отображенiя объектовъ, еще нужно отображенiе морфизмовъ. По опредѣленiю, нужно для любого морфизма f: A -> B какъ-то получить морфизмъ g: Array of A -> Array of B. Какъ мы можемъ написать программный кодъ для морфизма g? Надо написать циклъ по массиву "Array of A", примѣнить функцiю f къ каждому элементу массива, получить результаты (значенiя типа B) и положить всѣ эти результаты въ томъ-же порядкѣ въ новый массивъ. Получится значенiе типа Array of B, т.е. мы написали кодъ для морфизма g: Array of A -> Array of B. Дальше, можно провѣрить, что необходимыя свойства эндофунктора будутъ тогда выполнены. Преобразованiе изъ f въ g называется "fmap" на Haskell и "map" на языкѣ Scala. То есть, программисту достаточно написать функцiю "fmap" съ аргументомъ типа (A -> B) и возвращаемымъ значенiемъ типа "функцiя изъ Array of A въ Array of B". Тогда g = fmap(f). Это реализуетъ кодъ для эндофунктора "Array". Въ практической работѣ это оказалось жутко полезной вещью. Оказалось, что очень много типовъ данныхъ можно обобщить и сдѣлать изъ нихъ эндофункторы. И потомъ писать очень короткiй кодъ, въ которомъ вездѣ только map(), map(), map(). И ни одного цикла руками не надо больше писать! А свойства эндофунктора, оказывается, это то же самое, что математическая формулировка интуитивнаго пониманiя программиста о томъ, что значитъ "примѣнить функцiю f къ каждому элементу набора данныхъ, оставивъ порядокъ элементовъ такимъ-же". Поскольку математическiя свойства эндофунктора Array (и другихъ эндофункторовъ) гарантируются, программистъ можетъ смѣло полагаться на свою интуицiю и кодъ становится легко писать, читать и понимать. Гораздо легче, чѣмъ кодъ съ циклами. 4. Что такое естественное преобразованiе? Это отображенiе между эндофункторами, которое реализуется программнымъ кодомъ, не зависящимъ отъ типа данныхъ подъ эндофункторомъ. Напримѣръ, "переставить задомъ напередъ порядокъ элементовъ массива" это естественное преобразованiе Array -> Array. Компонента этого естественнаго преобразованiя для объекта А есть морфизмъ Array of A -> Array of A. Поскольку морфизмы нашей категорiи - это функцiи, значитъ, программистъ долженъ для каждаго типа А написать кодъ функцiи съ аргументомъ типа "Array of A" и результатомъ того же типа. Во многихъ языкахъ программированiя можно легко написать одинъ разъ кодъ этой функцiи, который будетъ переставлять задомъ напередъ порядокъ элементовъ массива и будетъ работать одинаковымъ образомъ для любого типа А (т.е. это будетъ кодъ, "параметризованный" типомъ А). Свойства естественнаго преобразованiя тогда будутъ выполняться автоматически для такого кода. (Это называется "parametricity theorem".) Вотъ поэтому оказалось, что въ языкахъ съ поддержкой параметровъ типа (т.е. можно писать кодъ сразу для всѣхъ типовъ А), теорiя категорiй полезна. Свойства естественнаго преобразованiя оказались математической формулировкой интуицiи программиста о томъ, что это значитъ, когда "кодъ написанъ одинъ разъ и работаетъ одинаковымъ образомъ съ любыми типами данныхъ". 5. Мы опредѣлили морфизмы между объектами А и В какъ функцiи одного аргумента (типа А). Но в языкахъ программированiя бываютъ и функцiи многихъ аргументовъ. Что дѣлать съ ними? Запрѣтить ихъ, оставить только функцiи одного аргумента. А вмѣсто функцiй многихъ аргументовъ, есть 2 варiанта, чѣмъ ихъ замѣнить. Первый варiантъ - въ языкѣ должны быть "records" или "tuples" (по-русски "кортежи"), т.е. наборы изъ нѣсколькихъ значенiй разныхъ типовъ. Напримѣръ, кортежъ (Int, Int, String) состоитъ изъ 3 частей - два цѣлыхъ числа и одна строка. Пусть у насъ есть функцiя f(x, y, z), которая возвращаетъ Boolean, а аргументы x: Int, y: Int, z: String. Надо помѣстить всѣ аргументы въ одинъ кортежъ (Int, Int, String). Получится функцiя формально одного аргумента. (Int, Int, String) -> Boolean Второй варiантъ - сдѣлать функцiю отъ перваго аргумента, которая въ качествѣ значенiя возвращаетъ функцiю отъ второго аргумента, которая въ качествѣ значенiя возвращаетъ функцiю третьяго аргумента, которая уже возвращаетъ Boolean. Int -> (Int -> (String -> Boolean)) Это работаетъ, если въ категорiи существуютъ экспоненты (т.е. String -> Boolean является въ языкѣ программированiя допустимымъ типомъ, и значенiе такого типа можно возвратить изъ функцiи или взять въ качествѣ аргумента функцiи). Гдѣ-то между 2010 и 2015 годами, экспоненты (т.е. возможность возвратить функцiю или взять функцiю въ качествѣ аргумента) были добавлены практически во всѣ языки программированiя, потому что люди наконецъ поняли, гдѣ счастье. 6. Каждый языкъ программированiя будетъ давать свою какую-то категорiю. Чѣмъ эта категорiя богаче свойствами, тѣмъ для программированiя лучше. Напримѣръ, очень полезно, чтобы были терминальный объект и иницiальный объектъ (initial object, terminal object - не знаю, какъ по-русски). Очень полезно, чтобы были произведенiя (это кортежи) и ко-произведенiя (это дизъюнктивные типы, называемые также "варiанты" или "помѣченныя суммы"). И чтобы объекты-экспоненты тоже были. Поэтому, создатели новыхъ языковъ программированiя это учитываютъ и создаютъ соотвѣтствующiе языки. Въ языкахъ С++, Java, Python, ... нету ни initial object / terminal object, ни ко-произведенiй, и это дѣлаетъ кодъ уродливымъ для цѣлаго ряда задачъ. Новые языки (Swift, Rust) учитываютъ это. А вотъ Гуглъ сдѣлалъ языки Dart и Go, которые ничего этого не учитываютъ. Потому что тупыыыыые. И у этого есть цѣна - они теперь будутъ писать миллiоны строкъ кода съ ошибками, вмѣсто десятковъ тысячъ строкъ кода безъ ошибокъ. 7. Теперь важный вопрос - а что даетъ теорiя категорiй программисту, который не хочетъ создавать новый языкъ, а хочетъ написать конкретную программу? Программистъ можетъ легко научиться работать съ Array of X, и съ функцiей map, ничего не зная объ эндофункторахъ. И это правильно - не нужно усложнять работу безъ надобности. Теорiя категорiй нужна лишь въ очень ограниченномъ объемѣ и лишь для опредѣленнаго круга задачъ программированiя. А именно, знанiе нѣкоторыхъ понятiй теорiи категорiй (и лемма Йонеды) помогаютъ въ созданiи библiотекъ опредѣленнаго вида, гдѣ важна абстракцiя на уровнѣ типовъ и эндофункторовъ. Напримѣръ, можно написать общую библiотеку для работы съ эндофункторами. Тамъ будутъ функцiи для произведенiя и ко-произведенiя эндофункторовъ, или, скажемъ, функцiи для того, чтобы создать эндофункторъ-монаду, свободно порожденную любымъ даннымъ эндофункторомъ, и потомъ работать съ этой свободной монадой (скажемъ, автоматически находить естественное преобразованiе въ другую монаду). Кодъ, получающiйся изъ этого, сегодня широко используется въ узкихъ кругахъ для написанiя Индустрiальныхъ Программъ Для Большого Бизнеса (тм). У такого кода есть важныя преимущества, - онъ практически гарантируетъ отсутствiе глупыхъ баговъ типа "вездѣ мы сдѣлали записи о найденныхъ ошибкахъ, а вотъ здѣсь забыли вписать этотъ кодъ". Если свободная монада дѣлаетъ записи о найденныхъ ошибкахъ, то она всегда ихъ дѣлаетъ правильно, потому что кодъ для этого написанъ одинъ разъ и онъ очень общiй. Есть библiотеки, которыя сегодня широко используются опять-таки въ узкихъ кругахъ, гдѣ есть функцiя для автоматическаго разложенiя полиномiальнаго эндофунктора на произведенiя и ко-произведенiя, и исходя изъ этого, производится автоматическое написанiе правильнаго программнаго кода (функцiи map) для любого полиномiальнаго эндофунктора, заданнаго лишь своимъ типомъ. Знанiе такихъ библiотекъ позволяетъ сократить кодъ программъ и уменьшить вѣроятность ошибокъ въ кодѣ. А знанiе необходимыхъ математическихъ свойствъ (мотивированныхъ теорiей категорiй) направляетъ программиста въ правильную сторону при написанiи кода этихъ библiотекъ. Однако, если программисту не нужны функцiи, работающiя сразу съ любыми эндофункторами, если онъ не пишетъ такiя библiотеки и не пользуется ими, то теорiя категорiй ему тоже не нужна. 8. Для практическаго программированiя еще оказалось необходимымъ разработать рядъ конструкцiй, которыя обычно мало освѣщаются въ математической литературѣ по теорiи категорiй. Напримѣръ, кромѣ эндофункторовъ (операцiя "map"), въ функцiональномъ программированiи на практикѣ много используются эндофункторы съ операцiями "filter", "zip", "traverse", "fold", а также эндофункторы-монады, одновременно иногда имѣющiя и "filter", "traverse", "fold". Математическая формулировка этихъ свойствъ и написанiе кода, который правильно отражаетъ эти свойства, необходимы для написанiя правильно работающихъ библiотекъ. Эти свойства можно сформулировать въ общемъ видѣ для произвольной категорiи съ какими-то дополнительными структурами, однако, онѣ малоинтересны для математиковъ, поэтому вы не найдете опредѣленiй "filterable functor", "traversable functor", "foldable functor" въ математической литературѣ. Но эндофункторы съ такими операцiями какъ разъ очень важны для программированiя. Теорiя категорiй даетъ, во-первыхъ, удобный языкъ для описанiя этихъ конструкцiй (эндофункторы, естественныя преобразованiя, коммутативныя дiаграммы), и во-вторыхъ, даетъ интуицiю о томъ, какiе предположенiя разумно дѣлать о математическихъ свойствахъ всѣхъ этихъ штукъ (и слѣдовательно, какъ правильно написать кодъ для соотвѣтствующихъ морфизмовъ). Напримѣръ, если нѣчто является функторомъ, то у него два свойства - тождественный морфизмъ переходитъ въ тождественный, а композицiя морфизмовъ переходитъ въ композицiю. Если нѣчто является моноидомъ, то у него три свойства - лѣвое тождественное, правое тождественное, и ассоцiативность. Если нѣчто является естественнымъ преобразованiемъ, то такая-то извѣстная дiаграмма должна быть коммутативна. Теперь, если мы (программисты) нашли конструкцiю, о которой математики не упоминаютъ (скажемъ, эндофункторъ съ операцiей filter), и намъ удалось показать, что она эквивалентна какому-то функтору, - то значитъ, мы ожидаемъ имѣть два извѣстныхъ свойства, не больше и не меньше. Это даетъ намъ увѣренность, что мы правильно угадали свойства этой конструкцiи и, стало быть, правильно написали кодъ для тѣхъ или иныхъ функцiй-морфизмовъ. 9. Въ чемъ польза именно отъ языка категорiй, а не просто отъ изслѣдованiя "на колѣнкѣ" разныхъ свойствъ функцiи map, функцiи filter, и т.д.? Въ общемъ, какъ я сказалъ въ пунктѣ 7, пользы нѣтъ до тѣхъ поръ, пока мы не начнемъ использовать функцiи, которыя должны одинаково работать съ любыми эндофункторами или болѣе общо съ любыми функторами между данными двумя категорiями (какъ-то нами построенными изъ исходной категорiи объектовъ-типовъ и морфизмовъ-функцiй). Примѣръ такой функцiи - построенiе свободной монады, порожденной заданнымъ эндофункторомъ. Это одинаково работаетъ для любого эндофунктора. Гдѣ-то между 2012 и 2016 годами, такая штука стала использоваться программистами довольно существенно. Объяснить, почему это такъ и въ чемъ польза для программиста отъ свободной монады, - это длинная исторiя. 10. Въ чемъ разница между "дѣлай одно и то же со всѣми элементами массива" и "повторяй до тѣхъ поръ, пока..."? Это какъ разъ хорошiй примѣръ, почему при изслѣдованiи программированiя возникаетъ категорный языкъ. Только надо сначала сформулировать "до тѣхъ поръ, пока" въ видѣ функцiи, такъ же, какъ мы раньше сформулировали "дѣлай для всѣхъ элементовъ" въ видѣ функцiи. Разъ нужна функцiя, то надо возвращать значенiе какого-то опредѣленнаго типа. Пусть это будетъ Array of X. Мы скопируемъ элементы массива одинъ за другимъ въ новый массивъ, пока выполняется какое-то условiе. Новый массивъ можетъ оказаться короче исходнаго. (Эта операцiя равносильна "до тѣхъ поръ, пока".) "примѣни функцiю f: X -> Y ко всѣмъ элементамъ массива" это функцiя fmap(f): Array[X] -> Array[Y] взятая отъ эндофунктора Array. Въ математикѣ это обозначается Array(f), т.е. "поднятiе" морфизма f функторомъ Array. "копируй каждый элементъ x, пока p(x) = true" это функцiя Array[X] -> Array[X], которая обозначается takeWhile(p). Здѣсь p должна быть функцiя X -> Boolean, т.е. "предикатъ". Примѣры использованiя: Haskell: fmap ( \ x -> x + 1 ) [100, 200, 300] даетъ массивъ [101, 201, 301] takeWhile ( \x -> x < 250 ) [100, 200, 300] даетъ массивъ [100, 200] Scala: Array(100, 200, 300).map(x => x + 1) даетъ массивъ Array(101, 201, 301) Array(100, 200, 300).takeWhile(x => x < 250) даетъ массивъ Array(100, 200) Теперь мы начинаемъ спрашивать, а какiя свойства желательно имѣть для этихъ функцiй. Для fmap это стандартныя свойства эндофунктора, fmap(id)=id, fmap(f o g) = fmap(f) o fmap(g). А для takeWhile математическiя книги почему-то умалчиваютъ. Поэтому программисты, стиснувъ зубы, сами доказываютъ про это теоремы. Напримѣръ, у takeWhile есть такое важное свойство - если примѣнить два takeWhile подрядъ съ разными предикатами p1, p2, то должно быть то же самое, какъ если мы примѣнимъ takeWhile съ предикатомъ булевой конъюнкцiи p1 и p2, т.е. \x -> p1(x) && p2(x). Это называется "законъ композицiи" (composition law). Если примѣнить takeWhile съ предикатомъ, который тождественно true, то это не должно вообще мѣнять массивъ. Это "законъ тождественности" (identity law). Напрягшись (и задавъ вопросъ - что будетъ, если примѣнить сначала fmap, потомъ takeWhile или наоборотъ), можно еще найти два закона "естественности". Потомъ дальше напрягшись, можно построить нѣкую аналогiю между fmap и takeWhile: и тамъ, и тамъ есть identity law и composition law, и ихъ можно свести къ стандартнымъ законамъ для нѣкоего вспомогательнаго функтора, о которомъ я сейчасъ не буду пытаться объяснять. Но можно и не сводить, а такъ и оставить, но тогда непонятно, откуда эти законы взялись. Пройдя еще черезъ пять-шесть примѣровъ такого сорта (программная задача - переходъ къ функцiямъ - переходъ къ произвольнымъ типамъ X, Y - написанiе законовъ или свойствъ, желательныхъ для программиста), убѣждаемся, что почему-то всегда получаются законы функтора или законы моноида или законы естественныхъ преобразованiй. Программисту надо какъ-то эти законы запоминать и про нихъ какъ-то думать. Либо въ каждомъ случаѣ будутъ какiе-то свои, свалившiеся съ неба законы, которые будетъ трудно запомнить. Либо программистъ выучитъ опредѣленiя моноида, категорiи, функтора, естественнаго преобразованiя и выучитъ, какiя для нихъ есть аксiомы, и тогда больше уже ничего запоминать наизусть не потребуется. Простой циклъ замѣняется на функцiю map. Это законы нѣкоего эндофунктора. "до тѣхъ поръ, пока" это takeWhile, разновидность фильтра (filter). У filter и takeWhile одинаковые законы, это законы нѣкоего функтора. Т.е. фильтры это обобщенiе цикловъ съ условiями. Вложенный циклъ замѣняется на функцiю bind (въ языкѣ Scala, эта функцiя называется flatMap). Это "монады", у нихъ законы моноида. Т.е. монады это обобщенiе вложенныхъ цикловъ. Операцiя монады - замѣна композицiи эндофункторовъ на одинъ эндофункторъ, это для цикловъ то же самое, что замѣна вложенныхъ цикловъ на одинъ, никуда не вложенный циклъ. Параллельныя вычисленiя замѣняются на функцiю zip, это тоже законы моноида. (Моноидальный функторъ.) Всевозможныя суммированiя по массиву и свертки заменяются на fold и traverse. (Законы функтора.) Установивъ это, можно сдѣлать общую библiотеку для такихъ функцiй. Становится понятно, какъ обобщать дальше, а куда идти нельзя. (Напримѣръ, не получится сдѣлать монаду изъ контраварiантнаго функтора.) Теорiя категорiй даетъ хорошiе орiентиры для такой работы. 11. Двѣ большiя разницы - программировать въ стилѣ "дѣлай разъ, дѣлай два, повтори", или въ стилѣ "функцiя f примѣняется къ аргументу x". Важно, что мы не "повторяемъ то-то и то-то для каждаго элемента массива", а "примѣняемъ функцiю f къ каждому элементу массива и собираемъ результаты въ новый массивъ". Получается опять функцiя изъ массива въ массивъ, а не просто наборъ "дѣйствiй". Это позволяетъ думать о программѣ какъ о математической функцiи или формулѣ. Оказалось очень полезно перейти къ математическому стилю программированiя. Въ математикѣ нѣтъ "дѣйствiй", а есть значенiя функцiй, примѣняемыхъ къ аргументу. Въ математическихъ книгахъ никогда не пишутъ "а теперь замѣните x на x + 1, установите z = 0, если раньше z былъ больше 10, и повторяйте чтенiе данной главы начиная съ формулы (3.12), пока x не станетъ равнымъ 100." То-есть, не используются циклы и не переопрѣделяется все время перемѣнная x на x + 1 въ циклѣ. Однако, почему-то, это въ математикѣ никому не мѣшаетъ, а только помогаетъ. Вотъ и въ программированiи оказалось, что помогаетъ. Но надо разрабатывать новые прiемы программированiя, напримѣръ, map, filter, zip, fold. И вотъ когда стали ихъ разрабатывать, выяснилось, что языкъ категорiй естественно возникаетъ. |
||||||||||||||