Comments 105
Можно ли вместо того, чтобы бегом отвечать на вопрос, для начала его сформулировать? Тем более, если целевая аудитория — «нематематики».
Поняв монады, теряшь способность их объяснить :) Как по мне, заметка получилась неплохая. В комментах разовьём.
Вывод особенно хорош применять при ревью чужого кода. Не раз ловил себя на мысли "дык это же изоморфно подходящему решению, которое я ожидал увидеть" и спокойно мержил код, зная, что при необходимости код легко выворачивается наизнанку и становится "более подходящим". А раньше я применял строгоя равенство и был более костным. Главное, не подняться до уровня "всё изоморфно всему" ведь все основные языки полны по Тьюрингу
Кроме этого, под кат обычно скрывается то, что необязательно для прочтения. А тут все равно все будут на него кликать, поэтому особого смысла в нем нет – пускай лучше те, кому неинтересно читать код на С#, проскроллят.
Насчет скроллинга — не знаю, как-то скрывать лишнюю информацию приятнее, чем скроллить.
Во всех случаях изоморфизм предлагался между множествами. Другими словами, предлагалась биекция — в каждом конкретном случае разная, разумеется, а не «одна на все случаи жизни».
Не между множествами, а между типами, а изоморфизм здесь — не биекция, а вычислимая ф-я, для которой есть обратная вычислимая. Не любая биекция вычислима.
Будьте корректны.
Биекция это всегда функция. В чем смысл ("вычислимой") — я не знаю. И последнее — любой тип даёт множество, составленное из всех возможных комбинаций этого типа, так что не могу всерьез принять ваши поправки.
В чем смысл ("вычислимой") — я не знаю.
В том, что не любая ф-я является вычислимой, очевидно. Биекция существует между любыми равномощными множествами, но вот вычислимая ф-я (с вычислимой обратной) — далеко не всегда. Множество биекций между двумя счетными множествами несчетно, а вот множество изоморфизмов — не более чем счетно.
И последнее — любой тип даёт множество, составленное из всех возможных комбинаций этого типа, так что не могу всерьез принять ваши поправки.
Любая селедка — рыба, но не любая рыба — селедка.
Как догадались, оба определения выше оказываются изоморфны. Это означает в точности следующее: если мне только одно из них, то в неявном виде мне даны сразу оба: все благодаря изоморфизму — двухстороннему преобразователю одного в другое.
Нет, не догадались… Помимо явно пропущенных слов, это утверждение звучит как «изоморфизм работает благодаря изоморфизму».
И да, не понятно, с чего вдруг простое равенство слишком строгое? И зачем в C# может потребоваться обратное каррирование?
На конкретных примерах на Haskell и C# я не только растолкую теорию для нематематиковПока у вас получилось только продемонстрировать примеры кода для математиков.
Компилятор не даст просто так одно подменить другим, хотя поведение совершенно одинаковое. Считаете, что ООП тут не причем?
Ну вообще, конечно, совершенно ни при чем, потому что "компилятор не дает подменить одно другим" из-за конкретной системы типов, а не ООП.
Нет, этого я не отрицаю. Но ваш пример никак с этим не связан. Если взять F# (который не ОО-язык), там будет все то же самое:
let f1 (a, b) = a + b
let f2 a b = a + b
let mutable t = f1
t <- f2
error FS0001: Type mismatch. Expecting aint * int -> int
but given aint -> int -> int
. The typeint * int
does not match the typeint
Два — думаю, вы согласитесь, что эту задачу можно было бы решить достаточно просто — самый глупый способ, через [Аттрибуты], более умный способ — class'ы Хаскеля. Просто это не очень практично вшивать прям в ядро, хотя в Haskell-сообществе то и дело появляются схожие разговоры.
Есть еще три — точно так же, как с монадой, моноидом, функтором, аппликативным функтором и т.д., ни один компилятор не может удостовериться наверняка, что соответ. законы таки выполняются на всех возможных входных данных. Отсюда вытекает главная причина, почему это не идет в мир, а остается на бумаге и в мыслях условных ученых.
Ну вы же понимаете, что F# — это только синтаксис ФПшный, не более?
Нет, не понимаю.
Два — думаю, вы согласитесь, что эту задачу можно было бы решить достаточно просто
Какую конкретно задачу?
По второму — заставить компилятор принимать изоморфные параметры, пренебрегая в таких случаях строгим равенством.
откройте, что ли, разницу между F# и, например, Haskell.
Это вы так тонко хотите намекнуть, что F# — это ОО-язык?
Не, ну если у вас есть ровно один ФП-язык, и это Хаскель, то с вами сложно спорить, но только не ожидайте, что другие с этим согласятся.
заставить компилятор принимать изоморфные параметры, пренебрегая в таких случаях строгим равенством.
А зачем?
По вопросу «зачем» — ответы могут быть очень разные и это выходит за контекст обсуждаемой темы. Я согласен с тем, что это малопрактично и очень способствует ошибкам, неуловимым. Я просто указал на саму возможность достаточно легко (если разработка компилятора, конечно, может считаться легкой задаче ;)) научить компилятор принимать изоморфизм.
Я говорил, что от ФП в нем только синтаксис.
А теперь попробуйте доказать (или, что то же самое, формально опровергнуть) это утверждение.
А, главное, если F# — это не ОО-язык, то и компилятор его — не ОО-компилятор, и философия его — не ОО-философия. Но при этом он продолжает демонстрировать поведение, которое вы приписываете ОО-философии. Не сходится.
По вопросу «зачем» — ответы могут быть очень разные и это выходит за контекст обсуждаемой темы.
Вот только с этого надо начинать. Потому что можно же просто взять язык с динамической типизацией, и в нем, при определенных подпрыгиваниях, все будет работать. И… что? Зачем мне нужно, чтобы компилятор принимал изоморфизм (даже если оставить за скобками спор о том, являются ли две конкретных функции изоморфными)?
Не вижу ничего таинственного в том, что ФП-синтаксис можно навесить на какие-то устоявшиеся парадигмы ООП-мира, уж систему типов — так точно.
Насчет вашего «зачем». Я бы задался другим «зачем», а именно — зачем вы сводите все к компилятору-то? Я же в выводе ясно написал, что первоочередно — это способ четче и последовательнее мыслить. Я нигде не утверждал, что нужны менять компиляторы. Также никому нигде не навязывал именно ФП языки и для наглядности провел читателя через классический ФП и классический ООП языки.
Давайте не будет «за деревьями не видеть леса»?
Не вижу ничего таинственного в том, что ФП-синтаксис можно навесить на какие-то устоявшиеся парадигмы ООП-мира, уж систему типов
И в каком месте различие функций (a, a) -> a
и a -> a -> a
— это "устоявшаяся парадигма ОО-мира"?
Я бы задался другим «зачем», а именно — зачем вы сводите все к компилятору-то?
Затем, что вы зачем-то приводите пример работы компилятора (в том числе и не-ОО языка) как аргумент в пользу того, что "ООП, особенно строго типизированное, [...] работает на уровне "строгого равенства". И потому [...] часто бывает излишне строгим."
И это далеко не только про компилятор, кстати. Но и про саму философию тоже. В любом случае — с точки зрения выводов и того, что я хотел сказать читателям — наш с вами спор ничего не меняет.
instance Functor ... where ...
… компилятору всего хватает. Другое дело, что можно объявить функтор, который на самом деле не функтор — и будет небедажимая беда у программиста.github.com/idris-lang/Idris-dev/blob/master/libs/base/Control/Isomorphism.idr
github.com/idris-lang/Idris-dev/tree/master/libs/contrib/Control/Isomorphism
А с переходом к гомотопическим типам можно полноценно формализовать и изоморфизмы для функций:
github.com/clayrat/redtt/blob/isos/library/cool/isos.red#L60
эту задачу можно было бы решить достаточно просто — самый глупый способ, через [Аттрибуты], более умный способ — class'ы Хаскеля.Задача «излишне строгий» компилятор сделать «достаточно строгим», я полагаю? В ОО-языках такая задача называется абстрагированием данных, и она успешно решается при помощи реализации и использовании интерфейсов. Тут не понятно почему вы приписываете ОО-парадигме излишнюю строгость.
ни один компилятор не может удостовериться наверняка, что соответ. законы таки выполняются на всех возможных входных данных. Отсюда вытекает главная причина, почему это не идет в мир, а остается на бумаге и в мыслях условных ученых.Да, ладно, а вы знаете про существование таких языков, как Agda, Coq, Idris? Там все законы приведенных вами классов можно спокойно формализовать, доказать и верифицировать при помощи компилятора. Поверьте, невозможность проверить эти законы в хаскеле не является причинной его малой популярности. Вон, посмотрите на языки с динамической типизацией типа Python или JS, там ничего нельзя проверить компилятором, однако данные языки пользуются относительным успехом.
Пока у вас получилось только продемонстрировать примеры кода для математиков.И для математиков получилось не очень — сомневаюсь, что им понравится определение:
все благодаря изоморфизму — двухстороннему преобразователю одного в другое.
Совершенно не понравилось. А как же про сохранение математической структуры?
сам по себе это не математический терминОчень даже математический! ИМХО достаточно:
Изоморфи́зм (от др.-греч. ἴσος — «равный, одинаковый, подобный» и μορφή — «форма») — это очень общее понятие, которое определяется по-разному в различных разделах математики. Изоморфизм определяется для множеств, наделённых некоторой структурой (например, для групп, колец, линейных пространств и т. п.). В общих чертах его можно описать так: обратимое отображение (биекция) между двумя множествами, наделёнными структурой, называется изоморфизмом, если оно сохраняет эту структуру. Если между такими структурами существует изоморфизм, то они называются изоморфными. Изоморфизм всегда задаёт отношение эквивалентности на классе таких структур.Вики.
Кто захочет — пройдет по вики дальше. Можно было и ссылкой на Вики ограничится, но зачем вместо не плохого определения, нпр., из Вики в статье давать негодное?
Два графа изоморфны, если между их множествами вершин существует взаимно однозначное соответсвие, сохраняющее смежностьФ.Харари, Теория графов, М.: УРСС, 2003, С.24.
Понятно, что для неграфов будет другое определение.
с ним я не согласенИмеете право несогласится со всей математикой, но при этом не отказывайте читателю в праве не согласится с Вами :)
Лично я считаю Википедию откровенно плохим источникомВики не источник, она только содержит ссылки на авторитетные источники и их краткий пересказ, иногда цитаты. Понятно, что в одних статьях это м.б. сделано лучше, в других хуже, а в третьих совсем плохо, но вешать ярлык на всю вики, как и на любой большой сборник многих авторов явно не оправданно.
Главный мой посыл не в том, что вы не нашкребете много разных определений изоморфизмов для разных разделов математикик, а в том, что там будет много ненужной конкретики, которую можно считать «деталями реализации», но не сутью, не «интерфейсом». Я же обращаю ваше внимание именно на интерфейс.
Верьте мнеЭто явно не для Хабра. Здесь обычно используется научный метод, а не шаманские заклинания.
Главный мой посыл не в том, что вы не нашкребете много разных определений изоморфизмов для разных разделов математикикЗначит есть много разных определений? А выше Вы утверждали:
Изоморфизм не определяется по-разному в зависимости от раздела математики.И как Вам после этого верить? Какому из утверждений? ;)
там будет много ненужной конкретики, которую можно считать «деталями реализации», но не сутьюИ чтобы избежать конкретики Вы предложили пустое «определение»? ;)
Изоморфизм сохраняет алгебраическую структуру, не ясно какую структуру сохраняют ваши примеры. Судя по всему — никакую, потому что в первом же примере сравнивается бинарная операция сложения и унарная операция отображающая int -> func<int,int>.
Пока я вижу у вас тезисы о том, что есть биекция между функциями определенных сигнатур, а также о том, что нужно уметь абстрагироваться от деталей. Вывод про ООП несостоятелен хотя бы потому, что определения, что такое ООП нет. Вы ищете «гибкости», но не определяете ее строго. В самом деле «потеря желанной гибкости» выражается в уменьшени какой-то метрики или норма вектора «гибкости» уменьшается, может ряды какие-то сходятся медленнее или ещё что-то?
Здорово, что вы поднимаете эти вопросы, но хотелось бы видеть больше строгости в изложении.
Второе — вы даете слишком конкретные примеры, в рамках которых вы правы. А я вот вам дам функцию f: { (a, b) } и функцию g: { (b, a) } и они-таки изоморфны. Углубляться в строгость определений можно бесконечно — но не в статьях такого характера.
Если что — взгляд на фукнцию как на бинарное отношение (т.е. множество в конечном счету, удовлетворяющее как раз определенным взаимоотношениям) — освобождает меня от вашей изначальной претензии. Но опять же — текст нематематический.
Вы так и не объяснили ни разу, что за проблему решаете и как… Кому-то ваши выкладки отозвались знакомыми буквами, но с тем, что изложено в статье, так никто и не согласился…
Может это знак? Может стоит обратить внимание? Может стоит изложить тему так, чтобы её понял хоть кто-то, кроме вас?
но текст-то для нематематиков
Но опять же — текст нематематический.
Этот тест ни для кого. Он — ни о чём. Вы не утруждали себя при написании статьи, не написали ни проблематики, ни объяснений, ни формулировок, ни подведения к выводам. Вы не сделали ни-че-го для того, чтобы эта статья была для кого-то. Может, математики, действительно, прочитали и поняли о чём вы, да и то, судя по комментариям — и они остались в неведении. А остальные и подавно, не поняли ни-че-го.
Даже с самого начала.
«Изоморфизм» — одно из базовых понятий современной математики.
Я безумно рад за вас, и за математику, но раз текст для «нематематиков» и термин Изоморфизм является главным в этой статье, то, будьте добры, потрудитесь и дайте хотя бы своё определение, своё понимание этого термина, чтобы читатель мог хотя бы попытаться понять, что будет дальше.
На конкретных примерах на Haskell и C# я не только растолкую теорию для нематематиков (не используя при этом никаких непонятных математических символов и терминов), но и покажу как этим можно пользоваться в повседневной практике.
Даже не учитывая прошлое замечание, вы не объявили сути — зачем этим пользоваться в повседневной жизни? Какие преимущества оно даст? Какие проблемы решит? Какой обычному читателю толк от использования изоморфизма в своём коде?
Проблема в том, что строгое равенство (например, 2 + 2 = 4) часто оказывается излишне строгим.
Извиняюсь, но я не вижу проблемы. Для меня это не проблема. Я ни разу не сталкивался с этой проблемой напрямую и не понимаю того, что вы пишите. Но, вполне вероятно, что я сталкивался с этой проблемой, но вы не потрудились показать на примерах эту проблему, в чём она выражается и как выглядит и какие проблемы приносит людям в повседневной жизни. И именно поэтому даже, если я сталкивался с ней, то я не смог проассоциировать свой опыт с вашим текстом.
И, даже в выводах вы умудрились напортачить. Ладно бы начали какой-то вывод про изоморфизм, с самого начала, тогда я бы просто не понял его, поскольку в моей голове с самого начала нет понимания проблемы и сути того, зачем вы это пишете.
Вывод? ООП, особенно строго типизированное, (вынужденно) работает на уровне «строгого равенства».
Но вы начали говорить про ООП. И, упоминание ООП в этой статье началось угадайте с какого момента? Именно, с вывода. Иными словами, вы вообще не касались тематики ООП, не связывали свои рассуждения с этой парадигмой, не пытались подвести читателя к этому выводу. Вы просто взяли и в выводе начали говорить про ООП.
Извиняюсь, но какого чёрта?!
В следующий раз, пожалуйста, давайте свои черновики знакомым или хоть кому-то, чтобы они могли скорректировать ваш поток информации, структурировать его и помочь вам сделать что-то более адекватное. В данный же момент, это тотальный провал.
Это все потому, что автор про вычислимость забыл. Изоморфизмом в данном случае являются вычислимые биекции (нам же в рамках программирования неинтересно рассматривать ф-и, которые нельзя реализовать в виде некоторого алгоритма), с-но, тот факт, что они вычислимые — и гарантирует сохранение структуры (вычислимые ф-и можно определить как непрерывные в некоторой специальной топологии, с-но, данная топология и сохраняется).
Я не то, чтобы забыл про это, просто оно не нужно для понимания природы изоморфизма.
Это нужно, как минимум, для того, чтобы текст вашей статьи был корректным текстом, а не бессмысленной белибердой.
Ну и да, для понимания того, что такое изоморфизм, как раз необходим тот факт, что это не просто биекция.
Любая биекция — это изоморфизм.
Спорить не интересно.
Любая биекция — это изоморфизм.
Нет, существуют биекции, которые не являются изоморфизмами. С-но, выше я привел математическое доказательство этого факта.
Я не люблю хамство.
Ваша статья некорректна, а вы — безграмотны в области, о которой рассуждаете. Это не хамство, это констатация факта. Возможно, прежде, чем писать статьи по cs, вам самому следовало приобрести какие-то базовые знания.
Спорить не интересно.
А тут не о чем спорить, это математика. Вы не правы, это математически доказано, конец истории.
The epimorphisms in Set are the surjective maps, the monomorphisms are the injective maps, and the isomorphisms are the bijective maps.
in Set
А при чем тут Set? Вас не смущает то, что в Set есть множества более, чем счетные, а типов таких не бывает?
Успехов!
Да действительно! Ну просто мимо пробегал, вообще не причем.
То есть, вы даже не понимаете, что рассматриваемая вами категория — это не Set.
Как я и сказал — извольте ознакомиться хотя бы с базовой литературой по CS, а потом уже статьи пишите.
И прекращайте свое воинствующее невежество — вас ведь читают другие люди, которые не разбираются в предмете и могут счесть ваши бредни за истину.
* 1 -1 2 -2
1 1 -1 2 -2
-1 -1 1 -2 2
2 2 -2 1 -1
-2 -2 2 -1 1
и
+ 0 1 2 3
0 0 1 2 3
1 1 2 3 0
2 2 3 0 1
3 3 0 1 2
Предлагаю вам найти тут изоморфизм групп. Hint — биекций тут много, но, изоморфизма нет потому что -1*-1 = 1, ничего такого с + сделать не выйдет. В итоге отобразить одно в другое вы можете (биекция), но сохранить свойства группы (изоморфизм) не сможете.
Скажите, пожалуйста, множество действительных чисел (объект в Set) — какому типу соответствует?
В любом случае следующее утверждение истинно: как только речь идет о Set — так сразу изомофримз <=> биекция. Исключений нет.
Но все же — хоть Set и скучна, ее более чем достаточно для плодотворного функционального программирования. Опять же, в сообществе Haskell условная категория Hask это такой плохенький Set и есть. Структура множеств — это сами их элементы, опять же — более, чем достаточно для повседневной практики.
Вдобавок, я не стал бы недооценивать Set хотя бы из-за леммы Йонеды.
находясь в Set, ничто не мешает пользоваться ее благами
Так речь о том и идет, что мы не находимся в Set
Опять же, реальный аналог это Hask — псевдокатегория (вообще, спор открытый, там вроде есть какие-то костыли, которые позволяют из нее таки категорию сделать, но не суть), калька с Set.
Во-первых, хаск — это вполне себе категория, а совсем не псевдо. Она не декартово замкнута, но, скажем так, почти декартово замкнута. Во-вторых — нет, хаск — совсем не калька с Set.
находясь в Set, ничто не мешает пользоваться ее благами, пока не сталкиваешься объективно с проблемами вроде той, которую вы пытаетесь показать.
Ну так используя Set в качестве категории для ЯП, вы сталкиваетесь с этими проблемами вот прямо сразу. У вас оказывает, что почти все объекты из Set в рамках ЯП не выражаются. Это проблема, на которую можно закрыть глаза?
Но все же — хоть Set и скучна, ее более чем достаточно для плодотворного функционального программирования.
Смотрите, никто (ну, кроме вас, видимо) категорию Set для функционального программирования не использует. Почему, как думаете?
Т. е. вы с морфизмами отождествляете не термы сами по себе (которые, более того, можно отличить), а этакие классы эквивалентности термов.
Ну я бы не сказал, что это костыль. С-но, брать в качестве морфизмов классы эквивалентности выглядит более естественным, чем сами термы. Т.к. ведь и термы нам важны именно с точностью до эквивалентности (нет особого смысла разделять термы, которые приводятся к одной и той же нормальной форме).
Ну, стоило бы начать с разъяснения проблемы. Привести примеры, когда проблема действительно появляется, а затем показать, как её можно решить при помощи вашего подхода. И показать, что я как пишущий в ОО-стиле выиграю от вашего подхода.
Ну и как вы перешли к критике ООП, на самом деле тоже непонятно.
Проще говоря, хотя эти функции являются обертками над '+', они отличаются. И компилятор совершенно прав, что не даёт одно подставить на место другого. Он не имеет права считать, что если вы имеете a и a->b и хотите получить b, вы сделаете эти именно путем вызова a->b с параметром a.
Автоморфизм — это нечто, «замкнутое на самом себе». В случае, когда морфизмы — это функции, автоморфизмы — это функции, замкнутые на типе, например: int -> int.
Другое дело, что
curry . uncrurry
, например, дает как раз автоморфизм. Предполагаю, что это и есть источник путаницы.Переходя к практике — во всех языках программирования есть такая абстракция как «вызов функции». Так вот, в add 2 2 вы получаете результат за 1 вызов, а в add' 2 2 — за 2 вызова. И это объективно разница с точки зрения компилятора, потому что между этими двумя вызовами может быть всё что угодно.
В любом случае — этот спор по-крупному ничего не меняет. Термины — терминами, но главное — понимать суть. По крайней мере, так мне кажется.
И закапывание в матаппарат не отменяет практической части вопроса.
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help
Prelude> :t curry . uncurry
curry . uncurry :: (a -> b -> c) -> a -> b -> c
… что эквивалентно:
(a -> b -> c) -> (a -> b -> c)
Надеюсь, это разрешит сомнения.
Изоморфизм спешит на помощь