Хабр Курсы для бэкендеров
РЕКЛАМА
Практикум, Хекслет, SkyPro, авторские курсы — собрали всех и попросили скидки. Осталось выбрать!
Поток Бэкенд доступен 24/7 благодаря поддержке друзей Хабра
Комментарии 16
Очень интересно, спасибо!
Мы не будем рассматривать множества
и
как одинаковые
Тут нюанс - а как же их рассматривать если принадлежность любому из них сводится к рассмотрению предложения 
? И получится, что этим двум множествам принадлежат одни и те же объекты. Т.е., то же самое, вроде термы 
и 
различны, но равенство троек дает одно и то же логическое предложение. Если же рассматривать декартово произведение как множество отображений из 
в 
, с свойством покоординатной принадлежности, то это вообще одно и то же, так, как 
. Так, что может не зря их считают за одно и то же - это и есть одно и то же.
Эээ, смотрите, вот у вас есть универсальное правило, как для кортежей строить предикаты принадлежности. Вы в своём примере два раза применили это правило к разным кортежам, и да, полученные предикаты логически равны. Но правила принадлежности типу недостаточно, оно вообще нужно только на этапе проверки корректности типизации программы. Для составных типов смысл существования - в деструктуризации: получить i-ый элемент кортежа, например. И в вашем примере у этих элементов будут разные типы.
Думаю я понял вас, но дело в том, что тогда вы не рассматриваете просто множества. Для простого математического множества есть только отношение принадлежности: для любого терма он или принадлежит данному множеству или нет. И в этом рассмотрении декатровы тройки равны. Но, разумеется, можно создать более сложную структуру - допустим какое-то "множество с типами" и с ним уже делать различия. Вот интересно как вы это формально определите. В принципе, я уверен, это должно быть уже сделанно в каком-нибудь раннем источнике.
У автора этой статьи есть прекрасное свойство - он приводит источники. Я пишу следуя известной монографии Nicolas Bourbaki "Theory of Sets" Springer-Verlag Berlin Heidelberg 2004. Есть и русский перевод, например, Бурбаки Н. - Основные структуры анализа. Теория множеств., Мир, 1965. Там, кстати, невероятные опечатки, так, что давайте сопоставлять с английской версией. Среди определенного круга математиков эта книга сегодня не пользуется популярностью, позвольте не погружаться в причины. Мне важен, в этой книге, точный подход, что подразумевает построение математики с нулю - с понятия алфавита и знакосочетаний из этого алфавита. Не подразумевается знание предварительных математических понятий, например даже кванторов, которые не определяются в других монографиях или называются первичными элементами или примитивами. Для нашего разговора важно, что построенная Бурбаками система является эквивалентной ZF. Кстати а какую монографию/источник вы имеете ввиду, говоря о фактах из ZF?
Так вот, на странице 72 [2004], стр. 82 [1965], вводится понятие пары с помошью специального субстантивного (substantific) знака. Так, что если U и T термы, то (U, T) также терм для которого вводится аксиома пары. Определение аксиомы на стр. 24 [2004], стр. 40 [1965]. И декартово произведение прекрасно существует стр. 74 [2004], стр. 83 [1965]. Кстати, определение существования стр. 36 [2004], стр. 53 [1965].
Таким образом все приведенные мной формулы и утверждения верны по этой монографии. Никаких костылей и равенство это реляциооный знак веса 2 в эгалитарной теории.
Далее, если, по вашему, можно ввести понятие пары используя множество, т.е. пары Куратовского (Н. К. Верещагин, А.Шень НАЧАЛА ТЕОРИИ МНОЖЕСТВ Москва Издательство МЦНМО, 2012, стр. 36), то разве это означает, что пара не существует? В каком источнике по ZF вы это видели? и что означает по вашему не "существует"? Опять-таки интересен источник.
Кстати, в вики https://ru.wikipedia.org/wiki/Упорядоченная_пара полный бедлам: всего два предложения и одно по Куратовскому, другое по Бурбакам.
Разве я говорил, что Бурбаки это ZF(или ZFC)? - посмотрите выше: я писал эквивалентно ZF. Т.е. после построения формальной системы получаем те же самы теоремы.
Ну и самое главное: значит для вас "не существует" и "не существует как примитив" это одно и то же? Этим вы обесцениваете вообще свои заявления. Вы можете заявить что не существует дифференцируемой функции, а оказывается она не существует как примитив. Но что означает существует как примитив? и отдельно что означает просто существование? Вот тут-то и ясна важность цитирования - по какой монографии вы вещаете о ZF? Откуда вы берете определение примитива?
В Бурбаках тройка определяется по паре. Ассоциативность коньюкции влечет ассоциативность декартова произведения и единственность тройки. С этого и начался весь разговор, см. выше. В теории множеств нет разных троек. Для этого нужна какая-нибудь надстройка, например, что-то вроде теории типов.
После этого момента типы-суммы исчезают из императивного программирования. В императивных языках конца XX века доминировало влияние Pascal и C. В Pascal не было типов-сумм, потому что Вирт считал их менее гибкими, чем не размеченные (untagged) объединения.
Не специалист по этому всему, но в Pascal же чуть ли не с рождения были variant records? Википедия считает что это и есть tagged unions https://en.wikipedia.org/wiki/Tagged_union#1970s_&_1980s
В C, возможно, нет типов-сумм, потому что его создатели заимствовали систему типов из языка PL/I от IBM
В C тоже можно сделать tagged unions "на коленке", но нужно следить вручную за тегами. В телекомах это вообще такая классика, используется в куче протоколов и есть даже специальный термин TLV (type-length-value / tag-length-value) https://en.wikipedia.org/wiki/Type–length–value
Насколько мне известно, ни в одной реализации Паскаля теги фактически не проверялись. Возможно, дело в этом.
Да, Вирт их добавил, но видимо не до конца поверил в их безопасность. В итоге получился компромисс: тег есть, но его проверка на совести программиста, а мы знаем, к чему это приводит) Именно поэтому в функциональных языках, где проверка исчерпываемости это киллер-фича, типы-суммы и взлетели
Неплохой перевод интересного материала.
Я глянул страничку автора книги. Он, конечно, молодец, но 30 долларов за 162 страницы мне было бы жмотно заплатить.
Для большинства вся эта история просто забавный факт, мы используем struct и enum не особо задумываясь почему они так называются
Но вот эта детективная работа по поиску первоисточников, когда показывается как за каждой строчкой кода, за каждым ключевым словом, стоит чья-то мысль, чья-то научная работа, написанная 60 лет назад - это круто
Алгебра предполагает кроме операций и нейтральные элементы для этих операций, 0 для сложения и 1 для произведения.
Статья не полна без затрагивания единичного типа unit type, нейтрального для типа-произведения и нулевого типа never type нейтрального для типа-суммы в Rust именно они позволяют полностью замкнуть алгебраическую систему типов с целью, с которой она задумывалась - доказать корректность программ, о чем мечтал Дейкстра, соответственно на примере Rust:
Unit type - () и struct Foo;
Never type - ! и enum Foo {};
Требую рассмотреть!
чисто технически, есть ведь ещё и типы-степени (функции)… сосредотачиваться лишь на суммах и произведениях — не так хорошо, я полагаю, но как бы с другой стороны, функции должны быть даже в тех япах, где нету структур… немного спускаясь в полуфилософскую шутливость, операции открылись словно наоборот от классической алгебры. если конечно не вспоминать о first class – функциях и замыканиях…
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Ранняя история алгебраических типов данных