Ну а ваш алгоритм этого не делает, независимо от программ. Вы опять сами себя переспорили.
Правда, ваша ошибка здесь в том, что вы считаете, что и программы, и алгоритмы должны всегда завершаться, но внутренняя неконсистентность вашей же логики с вашими же определениями даже смешнее.
Раньше вы путали знаки сравнения в любом месте, теперь только в декларации типа. Ну ладно, давайте с декларацией.
-- декларирую тип с ошибкой `<` вместо `≤`:
data PersonOrder (p1, p2 : Person) : Type where
MkPO : p1.name < p2.name → PersonOrder p1 p2
poReflexive : (p : Person) → PersonOrder p p
poReflexive = ??? -- не получится реализовать
там, где имеет место HOA (HomeOwner Assocation) — сообщество домовладельцев — и там в правилах сообщества прописаны требования к участникам (типа «крыша только красная, трава не длиннее 2 дюймов, собак кормить только мраморным стейком и т. п.»)
У далеко не всех HOA такие требования. Трава должна быть просто опрятной, крышу я спокойно поменял на слегка другого цвета вообще без согласования с HOA, окна — тоже, солары поставил в уведомительном порядке (лан, тут законы Техаса обязывают их разрешить, если уведомление направлено, так что я даже не ждал ответа).
А даже те правила, что есть, энфорсятся не всегда. Например, собакам запрещено «excessive barking», но это не мешает одному товарищу четыре раза в день по 15 минут выгуливать свою незатыкающуюся и триггерящуюся на любое движение псину, что несколько мешает держать окна открытыми и при этом заниматься требующими концентрации делами. Это практически невозможно починить в данной полураздолбайской HOA, и я был бы рад жить там, где это энфорсится куда строже.
Ну то есть всё это социальные конструкты, только одни получше, а другие похуже.
Да, и?
Я говорю не о том, какие это конструкты, а о том, откуда идёт инициатива по их насаждению. Снизу вверх — может, норм, может, плохо. Сверху вниз — практически всегда плохо.
А теперь возьмем ситуацию, когда команда разработчиков не может договориться про выбор методики работы. Что тогда делать бизнесу, садиться и плакать? Нет же, top-down-процесс спешит на помощь!
Во-первых, бизнес ничего не делает. В нормальной группе что-то решает в данном случае тимлид, а не весь бизнес целиком. Это совсем не тот же top-down-процесс, как если бы CEO посмотрел буллшит-доклад какого-нибудь Мартина на какой-нибудь конферфенции с задорно выглядящими графиками и решил «мы теперь все работает по аджайлу».
Во-вторых, устраиваясь на работу в данную группу к данному тимлиду, я в том числе осознанно и открыто делегировал ему часть ответственности и больший вес по принятию решений (по крайней мере, выяснить, хочу ли я ему это делегировать — моя цель на интервью как нанимающегося). Рождение в данном государстве с данной политической системе (или пересечение отрезка жизни с революцией) не является настолько же осознанным и добровольным.
В-третьих, поменять группу (или работу) куда проще, чем государство. Настолько проще, что по факту дисбалансом власти между тимлидом и линейным программистом можно пренебречь.
С учётом всего этого говорить, что там характеристики top-down-процессов одинаковые, и
не только государства воплощают этот принцип, а и любая (почти, так как bottom-up бизнесов крайне мало) другая организация
а вы попробуйте выразить Ферма на ваших типах и убедитесь, что это именно констрейнты
Как раз выразил выше (опустив не сильно важную для дискуссии деталь).
Так всё же, слова «уравнение a^n + b^n = c^n не имеет решения в целых ненулевых числах для n ≥ 3» являются просто констрейнтом на подмножество (и чего), или нет?
Я понимаю, что очень хочется уязвить собеседника, но в следующий раз попробуйте привязываться к контексту его комментария целиком, а не к одному ключевому слову.
Мне очень интересно, откуда у вас вылезет теоркат в разработке оптимизирующего компилятора императивного ЯП?
Даже для функциональщины для оптимизаций вроде «композиция катаморфизма F-алгебры и стрелки той же алгебры при определённых условиях выражается единым катаморфизмом» хватает совершенно базовых определений и практически школьного понимания универсального свойства (даже конусы строить не надо!), а применения всякого чуть более хардкорного теорката (codensity monad для функтора там, которая строится как right Kan extension для этого функтора вдоль него же) вполне описывается практически без теорката.
Только для первых трёх пунктов достаточно практически школьного уровня и справочника, для четвёртого и шестого — этим занимается очень мало людей (особенно на уровне выше, чем «запихнуть данную от аналитиков формулу в солвер»), для пятого — необходимость статов и теорвера несколько переоценена для продуктового машинного обучения.
А какие это результаты в случае программиста? В моём опыте чем больше для задачи нужно математики, тем хуже условия труда и тем меньше за работу платят.
Математика и высшее образование вообще меня сделали хуже, ИМХО.
Да не, почему? Это важная часть общения и самоактуализации, так что я не против, конечно! Просто, как говорится, употребляйте ответственно.
Ну а ваш алгоритм этого не делает, независимо от программ. Вы опять сами себя переспорили.
Правда, ваша ошибка здесь в том, что вы считаете, что и программы, и алгоритмы должны всегда завершаться, но внутренняя неконсистентность вашей же логики с вашими же определениями даже смешнее.
Окей, если все теоремы — тоже констрейнты, то какой смысл в высказывании «это просто констрейнт»? Что бывает кроме констрейнтов?
Лол.
Какое тут преобразование типа? Какой код выполняется? Можете ткнуть в это всё пальцем?
Дабл лол.
Раньше вы путали знаки сравнения в любом месте, теперь только в декларации типа. Ну ладно, давайте с декларацией.
Типы снова помогли отловить ошибку!
Их действительно можно перепутать, но не потому, что вы не знаете, какой значок что означает, а потому, что предметная область сложная.
Да, там ведь используются совершенно одинаковые навыки. Матан — это про зубрёж, как таблица умножения.
Таблицу умножения по какому основанию, кстати? По основанию 30 запомнить и вы вряд ли сможете уже, но что это говорит?
У далеко не всех HOA такие требования. Трава должна быть просто опрятной, крышу я спокойно поменял на слегка другого цвета вообще без согласования с HOA, окна — тоже, солары поставил в уведомительном порядке (лан, тут законы Техаса обязывают их разрешить, если уведомление направлено, так что я даже не ждал ответа).
А даже те правила, что есть, энфорсятся не всегда. Например, собакам запрещено «excessive barking», но это не мешает одному товарищу четыре раза в день по 15 минут выгуливать свою незатыкающуюся и триггерящуюся на любое движение псину, что несколько мешает держать окна открытыми и при этом заниматься требующими концентрации делами. Это практически невозможно починить в данной полураздолбайской HOA, и я был бы рад жить там, где это энфорсится куда строже.
Да, и?
Я говорю не о том, какие это конструкты, а о том, откуда идёт инициатива по их насаждению. Снизу вверх — может, норм, может, плохо. Сверху вниз — практически всегда плохо.
Во-первых, бизнес ничего не делает. В нормальной группе что-то решает в данном случае тимлид, а не весь бизнес целиком. Это совсем не тот же top-down-процесс, как если бы CEO посмотрел буллшит-доклад какого-нибудь Мартина на какой-нибудь конферфенции с задорно выглядящими графиками и решил «мы теперь все работает по аджайлу».
Во-вторых, устраиваясь на работу в данную группу к данному тимлиду, я в том числе осознанно и открыто делегировал ему часть ответственности и больший вес по принятию решений (по крайней мере, выяснить, хочу ли я ему это делегировать — моя цель на интервью как нанимающегося). Рождение в данном государстве с данной политической системе (или пересечение отрезка жизни с революцией) не является настолько же осознанным и добровольным.
В-третьих, поменять группу (или работу) куда проще, чем государство. Настолько проще, что по факту дисбалансом власти между тимлидом и линейным программистом можно пренебречь.
С учётом всего этого говорить, что там характеристики top-down-процессов одинаковые, и
просто неверно и подмена тезиса.
Как раз выразил выше (опустив не сильно важную для дискуссии деталь).
Так всё же, слова «уравнение a^n + b^n = c^n не имеет решения в целых ненулевых числах для n ≥ 3» являются просто констрейнтом на подмножество (и чего), или нет?
Вы:
Я:
Я понимаю, что очень хочется уязвить собеседника, но в следующий раз попробуйте привязываться к контексту его комментария целиком, а не к одному ключевому слову.
Я именно к этому контексту и отсылаю. Или мне нужно все ваши комментарии целиком сюда копировать, а то иначе вы не вспомните, что вы сами писали?
И моя религия выражается в том, что я имею наглость регулярно вам напоминать, что от
>вместо≥типы тоже спасают, и показывать, как?Не все алгоритмы обязаны завершаться на любом входе. Не понимаю вашей претензии.
Ну почему же, есть. Даже в Пирсе в TAPL (базовая, вводная книжка) про это целая глава отведена.
Так, стоп. А великая теорема Ферма — это тоже просто констрейнт?
А можете вы меня просвятить, пожалуйста?
Полностью поддерживаю (в естественноязычной интерпретации: высказывание «2 + 2 = 4» не будет ересью, даже если исходит от марксиста).
Маркс напихал взаимных противоречий в свою логическую систему и сидит довольный, потому что теперь может доказать что угодно. Ура! Ура! Ура!
Для подробного разбора, почему Гегель вместе с Марксом — это гибель мозга, можете почитать второй том Поппера Open Society and Its Enemies, например.
А ещё Петрика ересью считают!
Дело в том, что учение Петрика (или Маркса) не является наблюдаемым фактом в петриковщине (или экономике).
Оттого, что вы будете раз за разом повторять «типы нинужны», это не станет разумным, практическим аргументом.
Мне очень интересно, откуда у вас вылезет теоркат в разработке оптимизирующего компилятора императивного ЯП?
Даже для функциональщины для оптимизаций вроде «композиция катаморфизма F-алгебры и стрелки той же алгебры при определённых условиях выражается единым катаморфизмом» хватает совершенно базовых определений и практически школьного понимания универсального свойства (даже конусы строить не надо!), а применения всякого чуть более хардкорного теорката (codensity monad для функтора там, которая строится как right Kan extension для этого функтора вдоль него же) вполне описывается практически без теорката.
Только для первых трёх пунктов достаточно практически школьного уровня и справочника, для четвёртого и шестого — этим занимается очень мало людей (особенно на уровне выше, чем «запихнуть данную от аналитиков формулу в солвер»), для пятого — необходимость статов и теорвера несколько переоценена для продуктового машинного обучения.
Можете пояснить, какого уровня теорию множеств вы считаете необходимой для написания программ?
Берёте язык вроде Qimaera... А, тьфу ты, там опять математика, и даже теория типов и прочее.
Праввила отношений этих классов возьмутся откуда?
А какие это результаты в случае программиста? В моём опыте чем больше для задачи нужно математики, тем хуже условия труда и тем меньше за работу платят.
Математика и высшее образование вообще меня сделали хуже, ИМХО.