Comments 105
Вот я вроде бы даже знаю Haskell, но я все равно не понял, о чем эта статья и зачем она мне.
Можно ли вместо того, чтобы бегом отвечать на вопрос, для начала его сформулировать? Тем более, если целевая аудитория — «нематематики».
Можно ли вместо того, чтобы бегом отвечать на вопрос, для начала его сформулировать? Тем более, если целевая аудитория — «нематематики».
Поняв монады, теряшь способность их объяснить :) Как по мне, заметка получилась неплохая. В комментах разовьём.
Вывод особенно хорош применять при ревью чужого кода. Не раз ловил себя на мысли "дык это же изоморфно подходящему решению, которое я ожидал увидеть" и спокойно мержил код, зная, что при необходимости код легко выворачивается наизнанку и становится "более подходящим". А раньше я применял строгоя равенство и был более костным. Главное, не подняться до уровня "всё изоморфно всему" ведь все основные языки полны по Тьюрингу
А я вроде бы даже знаю математику, но все равно не понял, изоморфизм чего с чем мне предлагается.
Кроме этого, под кат обычно скрывается то, что необязательно для прочтения. А тут все равно все будут на него кликать, поэтому особого смысла в нем нет – пускай лучше те, кому неинтересно читать код на С#, проскроллят.
Кроме этого, под кат обычно скрывается то, что необязательно для прочтения. А тут все равно все будут на него кликать, поэтому особого смысла в нем нет – пускай лучше те, кому неинтересно читать код на С#, проскроллят.
Во всех случаях изоморфизм предлагался между множествами. Другими словами, предлагалась биекция — в каждом конкретном случае разная, разумеется, а не «одна на все случаи жизни».
Насчет скроллинга — не знаю, как-то скрывать лишнюю информацию приятнее, чем скроллить.
Насчет скроллинга — не знаю, как-то скрывать лишнюю информацию приятнее, чем скроллить.
Во всех случаях изоморфизм предлагался между множествами. Другими словами, предлагалась биекция — в каждом конкретном случае разная, разумеется, а не «одна на все случаи жизни».
Не между множествами, а между типами, а изоморфизм здесь — не биекция, а вычислимая ф-я, для которой есть обратная вычислимая. Не любая биекция вычислима.
Будьте корректны.
Биекция это всегда функция. В чем смысл ("вычислимой") — я не знаю. И последнее — любой тип даёт множество, составленное из всех возможных комбинаций этого типа, так что не могу всерьез принять ваши поправки.
В чем смысл ("вычислимой") — я не знаю.
В том, что не любая ф-я является вычислимой, очевидно. Биекция существует между любыми равномощными множествами, но вот вычислимая ф-я (с вычислимой обратной) — далеко не всегда. Множество биекций между двумя счетными множествами несчетно, а вот множество изоморфизмов — не более чем счетно.
И последнее — любой тип даёт множество, составленное из всех возможных комбинаций этого типа, так что не могу всерьез принять ваши поправки.
Любая селедка — рыба, но не любая рыба — селедка.
Не ищите там решения насущной проблемы. Ее там нет. Это про более плодотворный образ мыслей и мироощущение, не более того.
Кажется, вы забыли _объяснить_, что вы имели ввиду…
Нет, не догадались… Помимо явно пропущенных слов, это утверждение звучит как «изоморфизм работает благодаря изоморфизму».
И да, не понятно, с чего вдруг простое равенство слишком строгое? И зачем в C# может потребоваться обратное каррирование?
Как догадались, оба определения выше оказываются изоморфны. Это означает в точности следующее: если мне только одно из них, то в неявном виде мне даны сразу оба: все благодаря изоморфизму — двухстороннему преобразователю одного в другое.
Нет, не догадались… Помимо явно пропущенных слов, это утверждение звучит как «изоморфизм работает благодаря изоморфизму».
И да, не понятно, с чего вдруг простое равенство слишком строгое? И зачем в C# может потребоваться обратное каррирование?
На конкретных примерах на Haskell и C# я не только растолкую теорию для нематематиковПока у вас получилось только продемонстрировать примеры кода для математиков.
А уж как из равенства, завернутого в лямбду следует что-то про ООП, вообще за гранью понимания. Автор, тема-то интересная, но вы ее хоть потрудитесь сформулировать внятно.
А что тут такого непонятно? Завернутое в лямбду — это другой тип. Компилятор не даст просто так одно подменить другим, хотя поведение совершенно одинаковое. Считаете, что ООП тут не причем?
Компилятор не даст просто так одно подменить другим, хотя поведение совершенно одинаковое. Считаете, что ООП тут не причем?
Ну вообще, конечно, совершенно ни при чем, потому что "компилятор не дает подменить одно другим" из-за конкретной системы типов, а не ООП.
Т.е. вы отрицаете, что философия ООП сильно отпечаталась на устройстве компиляторов ООП-языков?
Нет, этого я не отрицаю. Но ваш пример никак с этим не связан. Если взять F# (который не ОО-язык), там будет все то же самое:
let f1 (a, b) = a + b
let f2 a b = a + b
let mutable t = f1
t <- f2error FS0001: Type mismatch. Expecting aint * int -> intbut given aint -> int -> int. The typeint * intdoes not match the typeint
Ну вы же понимаете, что F# — это только синтаксис ФПшный, не более? Это раз.
Два — думаю, вы согласитесь, что эту задачу можно было бы решить достаточно просто — самый глупый способ, через [Аттрибуты], более умный способ — class'ы Хаскеля. Просто это не очень практично вшивать прям в ядро, хотя в Haskell-сообществе то и дело появляются схожие разговоры.
Есть еще три — точно так же, как с монадой, моноидом, функтором, аппликативным функтором и т.д., ни один компилятор не может удостовериться наверняка, что соответ. законы таки выполняются на всех возможных входных данных. Отсюда вытекает главная причина, почему это не идет в мир, а остается на бумаге и в мыслях условных ученых.
Два — думаю, вы согласитесь, что эту задачу можно было бы решить достаточно просто — самый глупый способ, через [Аттрибуты], более умный способ — class'ы Хаскеля. Просто это не очень практично вшивать прям в ядро, хотя в Haskell-сообществе то и дело появляются схожие разговоры.
Есть еще три — точно так же, как с монадой, моноидом, функтором, аппликативным функтором и т.д., ни один компилятор не может удостовериться наверняка, что соответ. законы таки выполняются на всех возможных входных данных. Отсюда вытекает главная причина, почему это не идет в мир, а остается на бумаге и в мыслях условных ученых.
Ну вы же понимаете, что F# — это только синтаксис ФПшный, не более?
Нет, не понимаю.
Два — думаю, вы согласитесь, что эту задачу можно было бы решить достаточно просто
Какую конкретно задачу?
По первому — откройте, что ли, разницу между F# и, например, Haskell.
По второму — заставить компилятор принимать изоморфные параметры, пренебрегая в таких случаях строгим равенством.
По второму — заставить компилятор принимать изоморфные параметры, пренебрегая в таких случаях строгим равенством.
откройте, что ли, разницу между F# и, например, Haskell.
Это вы так тонко хотите намекнуть, что F# — это ОО-язык?
Не, ну если у вас есть ровно один ФП-язык, и это Хаскель, то с вами сложно спорить, но только не ожидайте, что другие с этим согласятся.
заставить компилятор принимать изоморфные параметры, пренебрегая в таких случаях строгим равенством.
А зачем?
Я не говорил, что F# — это ОО язык. Я говорил, что от ФП в нем только синтаксис.
По вопросу «зачем» — ответы могут быть очень разные и это выходит за контекст обсуждаемой темы. Я согласен с тем, что это малопрактично и очень способствует ошибкам, неуловимым. Я просто указал на саму возможность достаточно легко (если разработка компилятора, конечно, может считаться легкой задаче ;)) научить компилятор принимать изоморфизм.
По вопросу «зачем» — ответы могут быть очень разные и это выходит за контекст обсуждаемой темы. Я согласен с тем, что это малопрактично и очень способствует ошибкам, неуловимым. Я просто указал на саму возможность достаточно легко (если разработка компилятора, конечно, может считаться легкой задаче ;)) научить компилятор принимать изоморфизм.
Я говорил, что от ФП в нем только синтаксис.
А теперь попробуйте доказать (или, что то же самое, формально опровергнуть) это утверждение.
А, главное, если F# — это не ОО-язык, то и компилятор его — не ОО-компилятор, и философия его — не ОО-философия. Но при этом он продолжает демонстрировать поведение, которое вы приписываете ОО-философии. Не сходится.
По вопросу «зачем» — ответы могут быть очень разные и это выходит за контекст обсуждаемой темы.
Вот только с этого надо начинать. Потому что можно же просто взять язык с динамической типизацией, и в нем, при определенных подпрыгиваниях, все будет работать. И… что? Зачем мне нужно, чтобы компилятор принимал изоморфизм (даже если оставить за скобками спор о том, являются ли две конкретных функции изоморфными)?
Простите, у меня нет желания ничего опровергать ;)
Не вижу ничего таинственного в том, что ФП-синтаксис можно навесить на какие-то устоявшиеся парадигмы ООП-мира, уж систему типов — так точно.
Насчет вашего «зачем». Я бы задался другим «зачем», а именно — зачем вы сводите все к компилятору-то? Я же в выводе ясно написал, что первоочередно — это способ четче и последовательнее мыслить. Я нигде не утверждал, что нужны менять компиляторы. Также никому нигде не навязывал именно ФП языки и для наглядности провел читателя через классический ФП и классический ООП языки.
Давайте не будет «за деревьями не видеть леса»?
Не вижу ничего таинственного в том, что ФП-синтаксис можно навесить на какие-то устоявшиеся парадигмы ООП-мира, уж систему типов — так точно.
Насчет вашего «зачем». Я бы задался другим «зачем», а именно — зачем вы сводите все к компилятору-то? Я же в выводе ясно написал, что первоочередно — это способ четче и последовательнее мыслить. Я нигде не утверждал, что нужны менять компиляторы. Также никому нигде не навязывал именно ФП языки и для наглядности провел читателя через классический ФП и классический ООП языки.
Давайте не будет «за деревьями не видеть леса»?
Не вижу ничего таинственного в том, что ФП-синтаксис можно навесить на какие-то устоявшиеся парадигмы ООП-мира, уж систему типов
И в каком месте различие функций (a, a) -> a и a -> a -> a — это "устоявшаяся парадигма ОО-мира"?
Я бы задался другим «зачем», а именно — зачем вы сводите все к компилятору-то?
Затем, что вы зачем-то приводите пример работы компилятора (в том числе и не-ОО языка) как аргумент в пользу того, что "ООП, особенно строго типизированное, [...] работает на уровне "строгого равенства". И потому [...] часто бывает излишне строгим."
Да. Там еще было слово "(вынужденно) работает". Оно означает, что это не просто так, а есть причины. Часть из них вы и озвучили.
И это далеко не только про компилятор, кстати. Но и про саму философию тоже. В любом случае — с точки зрения выводов и того, что я хотел сказать читателям — наш с вами спор ничего не меняет.
И это далеко не только про компилятор, кстати. Но и про саму философию тоже. В любом случае — с точки зрения выводов и того, что я хотел сказать читателям — наш с вами спор ничего не меняет.
UFO just landed and posted this here
Не уверен. Я точно не GHC контрибьютор, но моих базовых знаний вроде бы хватает, чтобы представить как именно это должно работать. Собственно, по аналогии с функторами и оптимизациями fmap(g. f) = fmap(g). fmap(f). Слева два вызова fmap, а справа — один. Благодаря тому, что каждый конкретный функтор — это
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
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, там ничего нельзя проверить компилятором, однако данные языки пользуются относительным успехом.
Не в этом дело. Совсем не в формализации. А в кванторе всеобщености «для всех морфизмов выполянется...». Это означает, что нужно взять каждый морфизм и проверить. Все возможные комбинации. Потому что доказательства по индукции тут не работают — нет индуктивного шага.
UFO just landed and posted this here
Куда бы вы не запрятали «нужно будет доказать», оно остается. А значит — в виду отсутствия индуктивного шага — для теоретической безупречности нужно перебрать все возможные комбинации, «имя которым — легион». Я понял вашу мысль, но все же не могу понять как это решает (!) главную проблему комбинаторного ада.
Почему вы решили индуктивного шага нет? Индукционный шаг это просто инструмент для доказательства, на ряду с другими. И его также можно формализовать, например, здесь индукционный переход используется для док-ва коммутативности сложения.
Пока у вас получилось только продемонстрировать примеры кода для математиков.И для математиков получилось не очень — сомневаюсь, что им понравится определение:
все благодаря изоморфизму — двухстороннему преобразователю одного в другое.
Совершенно не понравилось. А как же про сохранение математической структуры?
Разве не пришлось бы тогда объяснять что такое «математическая структура»? Тем более, что сам по себе это не математический термин и в каждом конкретном случае понимается по-разному. Не говоря уже о том, что я несколько раз особо акцентировал внимания на «важных свойствах», которые сохраняются. Видимо, этого оказалось недостаточно.
сам по себе это не математический терминОчень даже математический! ИМХО достаточно:
Изоморфи́зм (от др.-греч. ἴσος — «равный, одинаковый, подобный» и μορφή — «форма») — это очень общее понятие, которое определяется по-разному в различных разделах математики. Изоморфизм определяется для множеств, наделённых некоторой структурой (например, для групп, колец, линейных пространств и т. п.). В общих чертах его можно описать так: обратимое отображение (биекция) между двумя множествами, наделёнными структурой, называется изоморфизмом, если оно сохраняет эту структуру. Если между такими структурами существует изоморфизм, то они называются изоморфными. Изоморфизм всегда задаёт отношение эквивалентности на классе таких структур.Вики.
Кто захочет — пройдет по вики дальше. Можно было и ссылкой на Вики ограничится, но зачем вместо не плохого определения, нпр., из Вики в статье давать негодное?
Это достаточно попсовое определение и с ним я не согласен. Изоморфизм не определяется по-разному в зависимости от раздела математики. Если брать за мерило теорию категорию (а на каком основании не брать, когда речь о таких проблемах?), то определение изоморфизма там одно и только одно и не зависит от конкретного раздела математики. Лично я считаю Википедию откровенно плохим источником, хотя это субъективно и наверняка обусловлено личным опытом.
Нпр., одно из наиболее авторитетных руководств по теории графов:
Понятно, что для неграфов будет другое определение.
Два графа изоморфны, если между их множествами вершин существует взаимно однозначное соответсвие, сохраняющее смежностьФ.Харари, Теория графов, М.: УРСС, 2003, С.24.
Понятно, что для неграфов будет другое определение.
с ним я не согласенИмеете право несогласится со всей математикой, но при этом не отказывайте читателю в праве не согласится с Вами :)
Лично я считаю Википедию откровенно плохим источникомВики не источник, она только содержит ссылки на авторитетные источники и их краткий пересказ, иногда цитаты. Понятно, что в одних статьях это м.б. сделано лучше, в других хуже, а в третьих совсем плохо, но вешать ярлык на всю вики, как и на любой большой сборник многих авторов явно не оправданно.
Верьте мне — все эти определения сводятся к одному обобщению. Теория категорий свела. Или не верьте — и проверьте сами. В том числе, существует категорий графов и гомоморфизмов и внутри этой категории существуют изоморфизмы.
Главный мой посыл не в том, что вы не нашкребете много разных определений изоморфизмов для разных разделов математикик, а в том, что там будет много ненужной конкретики, которую можно считать «деталями реализации», но не сутью, не «интерфейсом». Я же обращаю ваше внимание именно на интерфейс.
Главный мой посыл не в том, что вы не нашкребете много разных определений изоморфизмов для разных разделов математикик, а в том, что там будет много ненужной конкретики, которую можно считать «деталями реализации», но не сутью, не «интерфейсом». Я же обращаю ваше внимание именно на интерфейс.
Верьте мнеЭто явно не для Хабра. Здесь обычно используется научный метод, а не шаманские заклинания.
Главный мой посыл не в том, что вы не нашкребете много разных определений изоморфизмов для разных разделов математикикЗначит есть много разных определений? А выше Вы утверждали:
Изоморфизм не определяется по-разному в зависимости от раздела математики.И как Вам после этого верить? Какому из утверждений? ;)
там будет много ненужной конкретики, которую можно считать «деталями реализации», но не сутьюИ чтобы избежать конкретики Вы предложили пустое «определение»? ;)
Честно, нет желания тратиться на словоблудие. Я постарался вам объяснить разницу между «интерфейсом» и «деталями реализации», но вы упрямитесь. Все, что могу сделать для вас в плане более (на мой взгляд) глубокого понимания проблемы — посоветовать ознакомиться с тем, как так теоркат определяет изоморфизм, независимо от конкретики? На этом беседу считаю законченной, благодарю за комментарии.
Изоморфизм сохраняет алгебраическую структуру, не ясно какую структуру сохраняют ваши примеры. Судя по всему — никакую, потому что в первом же примере сравнивается бинарная операция сложения и унарная операция отображающая int -> func<int,int>.
Вы ошиблись. В данном случае алгебраической структурой можно считать сам факт, что при одинаковых аргументах обе функции возвращают одинаковый результат. Соответственно, curry/uncurry работает на любой бинарной функции и является полноправным изоморфизмом.
Алгебраическая структура это не «факт», это множество и отношения между элементами этого множества. Отношения важны потому, что позволяют, в частности, судить о внутреннем устройстве объектов множества. Например, если мы построим изоморфизм чего-то в конечное поле (скажем Z/7), то у элементов этого «чего-то» можно найти факторизацию (разложение) на простые множители.
Пока я вижу у вас тезисы о том, что есть биекция между функциями определенных сигнатур, а также о том, что нужно уметь абстрагироваться от деталей. Вывод про ООП несостоятелен хотя бы потому, что определения, что такое ООП нет. Вы ищете «гибкости», но не определяете ее строго. В самом деле «потеря желанной гибкости» выражается в уменьшени какой-то метрики или норма вектора «гибкости» уменьшается, может ряды какие-то сходятся медленнее или ещё что-то?
Здорово, что вы поднимаете эти вопросы, но хотелось бы видеть больше строгости в изложении.
Пока я вижу у вас тезисы о том, что есть биекция между функциями определенных сигнатур, а также о том, что нужно уметь абстрагироваться от деталей. Вывод про ООП несостоятелен хотя бы потому, что определения, что такое ООП нет. Вы ищете «гибкости», но не определяете ее строго. В самом деле «потеря желанной гибкости» выражается в уменьшени какой-то метрики или норма вектора «гибкости» уменьшается, может ряды какие-то сходятся медленнее или ещё что-то?
Здорово, что вы поднимаете эти вопросы, но хотелось бы видеть больше строгости в изложении.
Отчасти мне ваш посыл ясен и я скорее соглашусь, но текст-то для нематематиков. Если бы я хотел той меры строгости, о которой говорите вы, я был бы вынужден перейти на более подходящий для этого язык — т.е. на математику в чистом виде. Это первое.
Второе — вы даете слишком конкретные примеры, в рамках которых вы правы. А я вот вам дам функцию f: { (a, b) } и функцию g: { (b, a) } и они-таки изоморфны. Углубляться в строгость определений можно бесконечно — но не в статьях такого характера.
Если что — взгляд на фукнцию как на бинарное отношение (т.е. множество в конечном счету, удовлетворяющее как раз определенным взаимоотношениям) — освобождает меня от вашей изначальной претензии. Но опять же — текст нематематический.
Второе — вы даете слишком конкретные примеры, в рамках которых вы правы. А я вот вам дам функцию 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.
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, а потом уже статьи пишите.
И прекращайте свое воинствующее невежество — вас ведь читают другие люди, которые не разбираются в предмете и могут счесть ваши бредни за истину.
UFO just landed and posted this here
А мне интересно поспорить. Как вам такой пример — рассмотрим конечные группы ({0, 1, 2, 3}, +) и ({-2, -1, 1, 2}, *), операции + и * определены так
и
Предлагаю вам найти тут изоморфизм групп. Hint — биекций тут много, но, изоморфизма нет потому что -1*-1 = 1, ничего такого с + сделать не выйдет. В итоге отобразить одно в другое вы можете (биекция), но сохранить свойства группы (изоморфизм) не сможете.
* 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) — какому типу соответствует?
Я вижу несколько ответов на ваш вопрос. Первый — бесконечный лист, например [0..] в Haskell. Да, тут можно спорить с тем, что рано или поздно память все равно закончится и все такое. Согласен — реальный мир накладывает свои ограничения. Второй ответ — я нигде ни разу не утверждал, что подразумеваю работу «с категорией типов» (если такая вообще существует!): находясь в Set, ничто не мешает пользоваться ее благами, пока не сталкиваешься объективно с проблемами вроде той, которую вы пытаетесь показать. Опять же, реальный аналог это Hask — псевдокатегория (вообще, спор открытый, там вроде есть какие-то костыли, которые позволяют из нее таки категорию сделать, но не суть), калька с Set.
В любом случае следующее утверждение истинно: как только речь идет о Set — так сразу изомофримз <=> биекция. Исключений нет.
В любом случае следующее утверждение истинно: как только речь идет о Set — так сразу изомофримз <=> биекция. Исключений нет.
UFO just landed and posted this here
Мне понятно, что вы хотите сказать.
Но все же — хоть Set и скучна, ее более чем достаточно для плодотворного функционального программирования. Опять же, в сообществе Haskell условная категория Hask это такой плохенький Set и есть. Структура множеств — это сами их элементы, опять же — более, чем достаточно для повседневной практики.
Вдобавок, я не стал бы недооценивать Set хотя бы из-за леммы Йонеды.
Но все же — хоть Set и скучна, ее более чем достаточно для плодотворного функционального программирования. Опять же, в сообществе Haskell условная категория Hask это такой плохенький Set и есть. Структура множеств — это сами их элементы, опять же — более, чем достаточно для повседневной практики.
Вдобавок, я не стал бы недооценивать Set хотя бы из-за леммы Йонеды.
находясь в Set, ничто не мешает пользоваться ее благами
Так речь о том и идет, что мы не находимся в Set
Опять же, реальный аналог это Hask — псевдокатегория (вообще, спор открытый, там вроде есть какие-то костыли, которые позволяют из нее таки категорию сделать, но не суть), калька с Set.
Во-первых, хаск — это вполне себе категория, а совсем не псевдо. Она не декартово замкнута, но, скажем так, почти декартово замкнута. Во-вторых — нет, хаск — совсем не калька с Set.
находясь в Set, ничто не мешает пользоваться ее благами, пока не сталкиваешься объективно с проблемами вроде той, которую вы пытаетесь показать.
Ну так используя Set в качестве категории для ЯП, вы сталкиваетесь с этими проблемами вот прямо сразу. У вас оказывает, что почти все объекты из Set в рамках ЯП не выражаются. Это проблема, на которую можно закрыть глаза?
Но все же — хоть Set и скучна, ее более чем достаточно для плодотворного функционального программирования.
Смотрите, никто (ну, кроме вас, видимо) категорию Set для функционального программирования не использует. Почему, как думаете?
UFO just landed and posted this here
Т. е. вы с морфизмами отождествляете не термы сами по себе (которые, более того, можно отличить), а этакие классы эквивалентности термов.
Ну я бы не сказал, что это костыль. С-но, брать в качестве морфизмов классы эквивалентности выглядит более естественным, чем сами термы. Т.к. ведь и термы нам важны именно с точностью до эквивалентности (нет особого смысла разделять термы, которые приводятся к одной и той же нормальной форме).
UFO just landed and posted this here
Druu Мне тоже интересно, как задать топологию на вычислимых функциях.
Это называется теория доменов. В статье на википедии есть ссылки на разные материалы по теме, если интересно узнать подробнее. Я советую книгу Абрамского.
Тема интересная и правильная, но объяснено плохо.
Что именно стоило бы добавить? Как сделать лучше?
> Что именно стоило бы добавить?
Ну, стоило бы начать с разъяснения проблемы. Привести примеры, когда проблема действительно появляется, а затем показать, как её можно решить при помощи вашего подхода. И показать, что я как пишущий в ОО-стиле выиграю от вашего подхода.
Ну, стоило бы начать с разъяснения проблемы. Привести примеры, когда проблема действительно появляется, а затем показать, как её можно решить при помощи вашего подхода. И показать, что я как пишущий в ОО-стиле выиграю от вашего подхода.
Нет проблемы. Оставаясь в рамках ОО языка, возможно вообще ничего не выигрываете. Чтобы пользоваться тем же каррированием или lazy-вычислениями, понимание изоморфизма не нужно. Это статья про образ мыслей, а не конкретные инженерные практики. В вашем коде может и не быть изоморфизма, и все же, я настаиваю, что понимание таких вещей здорово прочищает голову и делает программиста гораздо сильнее.
Это биекция, но не изоморфизм. Потому что множества функций — разные. You're not my kind, так сказать.
Ну и как вы перешли к критике ООП, на самом деле тоже непонятно.
Ну и как вы перешли к критике ООП, на самом деле тоже непонятно.
Биекция — частный случай изоморфизма. Идти выше этого в короткой статье для «нематиков» я не вижу смысла.
Слегка ошибся. Биекция, но не автоморфизм.
Проще говоря, хотя эти функции являются обертками над '+', они отличаются. И компилятор совершенно прав, что не даёт одно подставить на место другого. Он не имеет права считать, что если вы имеете a и a->b и хотите получить b, вы сделаете эти именно путем вызова a->b с параметром a.
Проще говоря, хотя эти функции являются обертками над '+', они отличаются. И компилятор совершенно прав, что не даёт одно подставить на место другого. Он не имеет права считать, что если вы имеете a и a->b и хотите получить b, вы сделаете эти именно путем вызова a->b с параметром a.
Автоморфизм тут вообще не причем. Боюсь, что у вас некоторая путаница в голове. Вся идея статьи в том, что «компилятор совершенно прав», только если отталкиваться «строгим равенством». А это (иногда или, как мне кажется, довольно часто) излишне строго.
Автоморфизм — это нечто, «замкнутое на самом себе». В случае, когда морфизмы — это функции, автоморфизмы — это функции, замкнутые на типе, например: int -> int.
Другое дело, что
Автоморфизм — это нечто, «замкнутое на самом себе». В случае, когда морфизмы — это функции, автоморфизмы — это функции, замкнутые на типе, например: int -> int.
Другое дело, что
curry . uncrurryАвтоморфизм — это изоморфизм из множества в то же самое множество. В частности вот id — автоморфизм. А curry\uncurry и lazy\unlazy — нет. Ровно так же add и add' принадлежат к разным множествам функций. И компилятор совершенно прав с точки зрения компилятора. И имелось в виду, что хотя вам очевидно, что add и add' выполняют одинаковую задачу, компилятор такого вывода сделать не может. Но это всё теория.
Переходя к практике — во всех языках программирования есть такая абстракция как «вызов функции». Так вот, в add 2 2 вы получаете результат за 1 вызов, а в add' 2 2 — за 2 вызова. И это объективно разница с точки зрения компилятора, потому что между этими двумя вызовами может быть всё что угодно.
Переходя к практике — во всех языках программирования есть такая абстракция как «вызов функции». Так вот, в add 2 2 вы получаете результат за 1 вызов, а в add' 2 2 — за 2 вызова. И это объективно разница с точки зрения компилятора, потому что между этими двумя вызовами может быть всё что угодно.
Не знаю, откуда вы черпаете определения, но «автоморфизм» — это одно из фундаментальных понятий теорката. Собственно, как и «изоморфизм». И вообще — «морфизм». Так вот, если мы будет отталкиваться оттуда (а какие могут быть причины этого не делать, если эта теория как раз родилась в попытке разобраться в том числе, и с названными проблемами?), то ваше понимание автоморфизма — неверно. И даже по ваше определению lazy. unlazy — тоже автоморфизм, т.к. это как раз функция x -> x, поскольку (.) это композиция двух функций. Если примеры на Хаскеле непонятны, то внимательно посмотрите на возвращаемый тип делегата из C#. Так что, по-прежнему считаю, что у вас в голове легкая путаница. Или я не обладаю знаниями, которые есть у вас.
В любом случае — этот спор по-крупному ничего не меняет. Термины — терминами, но главное — понимать суть. По крайней мере, так мне кажется.
В любом случае — этот спор по-крупному ничего не меняет. Термины — терминами, но главное — понимать суть. По крайней мере, так мне кажется.
Неа. unlazy (точнее, fromLazy) это (() -> a) -> a, как вы сами записали. И это морфизм из ()->a в a, который соответственно не является эндоморфизмом, а следовательно и автоморфизмом.
И закапывание в матаппарат не отменяет практической части вопроса.
И закапывание в матаппарат не отменяет практической части вопроса.
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)Надеюсь, это разрешит сомнения.
Да, вы показали, что curry имеет обратный морфизм и следовательно является изоморфизмом. При этом автоморфизмом он по прежнему не является.
Честно говоря, не понимаю, что именно это меняет в контексте статьи. Не вижу смысл устраивать здесь терминологический спор и перебрасываться уже сугубо математическим комментами. Все таки, для нематематиков писалось. В любом случае, статья была немного о другом. Благодарю за обсуждение.
Это было сказано в контексте того, что данные функции принадлежат к разным множествам и не могут быть взаимозаменяемыми для компилятора.
Выше ветка, где, собственно, предлагается пример, где могут.
Мм. Не покажете точный коммент с примером?
Знаете, это не пример. Это рассуждение, что наверное такими-то средствами языка Haskell можно так сделать, что оно будет так работать.
А разве за этим примером не стоит конкретный компилятор, который это «съест и не подавится»? Да и на .NET есть пример с атрибутами — как раз метаинформация в первую очередь для компилятора и среды исполнения, и только уже потом для рефлексии и хитрых хаков.
Может быть стоит. Но насколько я знаю, в хаскеле класс это по сути способ задания полиморфной функции, а не изменения существующих. Атрибуты .net — это просто метаданные. И вы конечно можете создать аттрибут, который будет говорить сгенерировать версию данной функции, принимающую данный изоморфизм, но это ничего не изменит.
Выше я уже высказался по этой статье и повторяться не буду. Прошу прощения за оффтопик, но сложившаяся ситуация ИМХО хорошо иллюстрирует несовершенство системы оценок: оценка за статью (общий рейтинг) положительная, а если судить по комментам, то наоборот ;)
Sign up to leave a comment.
Изоморфизм спешит на помощь