У вас очень много опечаток в фразе "Agda это решает через костыли".
Не нашёл ни одной, потому что написано то, что я и так хотел сказать.
Код пишется один раз, а читается много раз. Куда удобнее читать код, в котором не используются (визуальные) многозначковые комбинации или, чего хуже, слова, для тех вещей, для которых в предметной области есть устоявшаяся нотация.
где используются кастомные операторы и функции-закорючки, в порядке их появления — трёхместный _⊢[_]_ (_ обозначает, куда идёт аргумент) и бинарный _⇒_ на первой строке; четырёхместный _⊢[_]_⦂_ и бинарный _,_ во второй строке, и бинарный ƛ в третьей. Как бы вы написали это обычными словами, чтобы это можно было прочитать?
Если бы на клавиатурах реально был символ ≗
Одна из причин мне использовать эргодокс со слоями. Греческие буквы и наиболее частые символы я повесил на отдельные слои.
и у него было человеческое название
Поточечное пропозициональное равенство двух функций.
Но вот это вот изобретение нотации в шарообоазном вакууме в отрыве от реального мира - спасибо, нет.
Ох уж этот реальный мир и отсылки к нему, когда по реальным миром каждый понимает что-то своё.
в риальном мире так та и матиматика ненужна, и вуз, и дажи старшые классы школы. чаивые калькулятар пащитает, а граматнаст тоже ненужна ведь вы этоттекст тоже можите прачитать и панять што яимел ввиду
Клавиатура заточена под ввод букв и цифр, а не вот этой вот вашей красоты.
Agda это успешно решает вводом закорючек через аккорды. Например, ≡ — это \==, а ≗ — \circeq.
Люди общаются между собой словами. Все эти значочки надо как-то называть (а значит слова будут)
В агде это тоже решается: люди вполне успешно описывают эти значочки терминами из предметной области, например.
Незнакомый с нотацией человек мало того что неспособен прочесть написанное, он даже не может нормально задать вопрос "что делает Х", потому что непонятно как назвать Х.
И это.
Что-то я подозреваю что гуглить это всё тоже окажется околоневозможно.
Пользователю важно, что там есть тесты? Нет. Менеджменту и бизнесу важно, что там есть тесты? Нет.
Тесты ничего не добавляют, только вынуждают раздувать код в восемь и шесть седьмых раз, чтобы добавить все нужные моки, интерфейсы, SOLID и DI. Вы знаете, что в Штатах сейчас вообще правительство DEI запретило? Это просто хотели запретить DI из-за феерического разбазаривания ресурсов на пять экранов кода на каждую функцию, но просто когда печатали текст указа, то случайно вместе с D нажали на кнопку над ней (и тесты это не поймали, обратите внимание — толку с них?).
если легче читать с аннотациями, то вывод типов - это усложнение чтения
Топ-левел-байндинги легче читать с аннотациями, нетривиальные функции легче читать с аннотациями, простые вещи и локальные переменные легче читать без аннотаций.
У вас тезис уровня «вы определитесь, или говорящие имена переменных, или i как индекс массива».
ибо аннотации в общем случае удваивают количество кода
Мутабельность к этому не имеет вообще никакого отношения.
фотон без наблюдения ведёт себя иначе, чем если за ним наблюдают.
И там, где это важно, это пытаются минимизировать. Вы же даже не пытаетесь это сделать, а ставите те эксперименты, которые легче поставить (напихать трейсов и потом с умным видом сидеть их разглядывать), а не те, которые относятся к вашему предмету исследования (почему тормозит).
это именно про типы и было.
Абсолютно верно, без типов этой проблемы нет.
Этот тип является суммой множества типов
Вы даже сами сказали, «этот тип». Тип один, всё.
причём крайне разнородных, таких, как "контейнер сложных документов"
Обычная индукция/рекурсия, не вижу проблем.
и "ошибка".
Если это не часть семантики yaml, то это они зря, конечно. Но это вопрос конкретной реализации, а не теории типов.
в реализации этого типа под капотом точно та же структура, что получается при динамической типизации
Да, и? Вы думаете, тут цель — выпендриться и иметь в рантайме какое-то другое представление (что, кстати, делают с GADT'ами, но вы ещё не там)? Тут цель — это проверки в компилтайме, до запуска.
а просто когда у вас список становится большим, а он вон на простых примерах уже большой, чтобы возникнуть проблемам
а отсылка про то, что такое наблюдение влияет на наблюдаемый объект, она разве не про мутабельность была?
Эта отсылка была к тому, что ПО с дебагами и прочими трейсами ведёт себя совсем не так, как без них.
ага, это просто цена за инструмент. просто нужно о ней знать и всё.
Попробуйте в следующий раз дочитывать комментарии до конца. Или хрен с ними с комментариями, фразы-то до конца дочитывайте.
и О(N^2) на время разработки
и О(N^4) на поиск багов
А использовали бы типы — не было бы такой ерунды у вас, как вы описываете.
Возможность написать функцию, которая будет обрабатывать сразу много разных типов.
Нет, конечно. Она всё ещё обрабатывает ровно один тип.
а в языке динамической типизации эту сборку осуществляет компилятор, а не программист. вот и вся разница.
А кто в языке с динамической типизацией осуществляет проверку, что вещи вне этого списка не придут, и кто отличает String как Real от String как String?
На практике я бы считал приближённо и в интервальной арифметике — всё равно все данные с погрешностями. А там уже и формулы расслабить можно, и полегче будет.
Но, опять же, я ничего не знаю о предметной области.
Ставь лайк, если любишь искать ключи где светлее, а не где потерял.
Ведь мир-то (весь мир!) состоит из мутабельных объектов.
Бездоказательное утверждение, отсылающее к эмоциям. Причём тут вообще мутабельность и объекты?
Кому в голову такое придёт?
Соломенным чучелам, с которыми вы активно спорите.
трейсы исключений помогают в сложных случаях, когда отсутствует понимание: где находится источник ошибки.
В случае таймаутов от этих трейсов (вызывающего сервера, отваливающегося по таймауту вызываемого) толку, как с трейсов изнутри grep для понимания, где в приложении, пишущем логи, по которым вы грепаете, проблема.
У меня всё больше впечатление, что к разработке софта вы относитесь как-то сбоку, как ПМ или скрам-мастер там, не знаю.
ну вслух, что ли мою фразу перечитайте. слово прямо рядом со словом "клетка" стоит.
То есть, это вы сказали, не я. QED.
ибо помимо аннотаций типов, мы теперь вынуждены иматься с return ошибок
Чем это сложнее, чем throw ошибок?
с написанием дублей методов для типов с их матчингом
Что это вообще значит?
и сборкой многих типов в единый АДТ
Чего там собирать? Это O(1) от размера кодовой базы и O(n) от количества типов ошибок, которых в стандартных оперднях очень мало.
(который является попыткой инкарнации динамической типизации)
Вы это повторяете в который раз, но в который раз отказываетесь пояснить, какое отношение АДТ имеют к динамической типизации.
То, что в инте может быть 0, может быть 1, а может быть 42 — это случайно не проявления динамической типизации, кстати?
вот в Python, например, программист не думает об управлении памятью, а в Rust вынужден постоянно об этом думать.
Да, абсолютно бессмысленное упражнение, ведь между кодом на Rust и Python нет никакой разницы по характеристикам исполнения.
именно невычислимы. но адепты типов стремятся это сделать.
Я боюсь, вы даже не понимаете, в каком смысле тут упоминалась невычислимость. Это, конечно, очень смешно.
И, кстати, типы и ООП во многом синонимы. И вы должны были бы оппонировать автору статьи. Но нет - вам кажется, что вы не такие.
Не все базисы, по которым раскладывается intrinsic-сложность систем, одинаково полезны. ООП — неудачный базис [в большинстве задач, и в подавляющем большинстве задач, с которыми сталкивался лично я]. ФП (в смысле типов) — куда более удачный базис [снова в большинстве задач].
У этой ОС есть очень даже фиксированный API под именем POSIX.
Модули ядра ты пишешь через POSIX?
Нет, только матом, только им описывается обратная совместимость Хаскеля!
А мне норм. Я как-то раз спокойно в 2019-м году взял компилятор, написанный мной в начале 2017-го и с тех пор не обновлявшийся, поменял в stack.yaml резолвер на актуальный stackage lts, потратил где-то 10 минут на выковыривание устаревших методов из кодовой базы в несколько тыяч строк, и всё после этого сразу заработало (получив заодно где-то ЕМНИП 20% прироста производительности тупо за счёт обновления компилятора и библиотек).
А то, что милые люди из WellTyped поломали систему сборки?
Эээ, я тут открыл для себя ghcup и последние года три получаю свежий ghc оттуда, так что не в курсе — а что там поломали?
Я постарался донести до ряда людей (Зубин, Гамари) простую мысель, что OCaml легко проходит через сцену любого копроративного театра безопасности за счёт того, что bootstrap компилятор поставляется в байткоде.
Не видел ни одной компании, где отсутствие бутстраппинга являлось бы ключевым препятствием перед корпоративной красной лентой. Основная сложность в нашей общей компании-то была ЕМНИП в том, чтобы убедить клоунов актёров из этого театра дать blanket permission на либы в hackage.
Кстати, как там gcc нынче бутстрапится, и кому это мешает?
Не просто безграмотность, а воинственная безграмотность.
вот итератор/счётчик позиции цикла или этих ваших итераций - это целое число, встроенный тип?
Подразумевая, что вы имели в виду индекс массива, то это встроенный тип Fin, параметризованный (гошники зажмурились) длиной (все остальные зажмурились) массива. Функция
writeAt : Array n a → Fin n → a → Array n a
не может выйти за границы вообще никогда, для любого массива любой длины, полученного откуда угодно, хотя Array и Fin являются библиотечными типами.
Что вы устали? Игнорировать эмпирические данные? Так вы и в прошлый раз это скипали и не отвечали по существу. Я вам пример, как разделение на чистые и нечистые функции не увеличивает объём кода, вы продолжаете бегать с «в два, нет, в три, нет, в десять раз больше пять экранов текста!»
затем, что этот код мы пишем? пишем.
Это тупейший клей между рантайм-системой и вашей бизнес-логикой. Там нечего тестировать.
прежде чем отдавать его клиентам убедиться нужно, что он работает? нужно
Чем меняют поведение наблюдаемой системы и её перф-характеристики.
Там, где я работал и где скорость ответа действительно была важна и приводила к более плачевным денежным исходам, чем «юзер монополиста подождёт вызова такси не 5 секун, а 10, и с вероятностью 1% в следующий раз предпочтёт идти пешком», это не работало. Работает только снятие полного дампа трафика и дальше уже существенно более тяжёлая артиллерия, чем дебаг-данные, трейсы ошибок и профайлинг средствами языка/окружения.
Впрочем, это так, лирика. Лучше скажите, как тут помогают трейсы исключений? Вы до таймаутов и прочих проблем на проде на них вообще забиваете, что ли, лол?
чуть глаза поднимите прямо на процитированный Вами текст, в нём написано в какую. прямо в Вашей цитаете есть ответ.
Так там нету.
вынуждены писать более сложный код
Что сложнее? Как раз проще: понятно, что может завершиться ошибкой (и какой), а что — нет.
от повышения сложности код становится менее надёжным, а не более, как хотелось бы
я пожаловался что с переходом на return error мы утратили весьма удобный инструмент
Только его и не было.
который помогал в отладке
При разработке или на проде? В первом случае вы код прямо пишете сейчас новый, какие там глубокие стектрейсы для ваших кеширующих микросервисов? Во втором случае, может, есть какая-то связь с отсутствием выразительных типов?
Да не, снова ерунда.
вы НАМЕРЕННО задали вопрос из области "были примеры, где этот инструмент не работал".
После ваших просьб в разговоре об ФП написать аналог вашей функции на SQL (до сих пор лолирую) или черри-пикинга отдельных библиотек в отдельном языке я на вашем месте бы не стал про это даже вспоминать.
я подтвердил, что да, были примеры, где этот инструмент не работал. и зафиксировал, что вы уводите дискуссию от первоначального пункта 1
Да не, вы просто инструменты путаете. Вы говорите об экзепшонах, когда дело в какой-нибудь там виртуальной машине для джавы или дотнета (в которых я не шарю совсем, поэтому не смогу поддержать разговор), которая может выборочно и чуть ли не ретроспективно собирать трейсы, деоптимизировать, и так далее.
Соответственно, законы физики и теории вычислимости не мешают тому же .NET CLR записывать трейс каждый раз, когда вы в F# возвращаете его аналог Left , или мне наваять за пару вечеров плагин к ghc, который каждой функции будет добавлять констрейнтHasCallStack , чтобы потом его захватывать в моей собственной иерархии ошибок.
Просто это всё нафиг никому не нужно, потому что ценность трейсов в сильно типизированных языках переоценена. Это как жаловаться, что JS безапелляционно лучше C++, потому что в JS есть eval.
Только при этом они есть даже в питоне. Просто спецификации формата — это, внезапно, спецификации формата, которые нужны, чтобы показать, условно, сколько знаков после запятой печатать, а не что-то там затыкать. Использование %d или %fв том же питоне — это просто дань традиции, чтобы программистам из других языков было проще и привычнее.
Нет никаких причин, почему нельзя было бы писать просто % в хаскельном printf — типы аргументов всё равно известны статически, и как их печатать, тоже известно статически. Просто WTF-момент от простых процентов больше, чем экономия пары знаков.
А написать типизированный принтф, терм которого после частичного применения к чему-нибудь вроде
printf "Hello {}, your age is {}"
имел бы тип Show a ⇒ Show b ⇒ a → b → String , даже проще, чем париться с полноценным разбором строки форматирования в компилтайме и последующим тайпчекингом аргументов.
Не нашёл ни одной, потому что написано то, что я и так хотел сказать.
Код пишется один раз, а читается много раз. Куда удобнее читать код, в котором не используются (визуальные) многозначковые комбинации или, чего хуже, слова, для тех вещей, для которых в предметной области есть устоявшаяся нотация.
У вас есть код
где используются кастомные операторы и функции-закорючки, в порядке их появления — трёхместный
_⊢[_]_(_обозначает, куда идёт аргумент) и бинарный_⇒_на первой строке; четырёхместный_⊢[_]_⦂_и бинарный_,_во второй строке, и бинарныйƛв третьей. Как бы вы написали это обычными словами, чтобы это можно было прочитать?Одна из причин мне использовать эргодокс со слоями. Греческие буквы и наиболее частые символы я повесил на отдельные слои.
Поточечное пропозициональное равенство двух функций.
Ох уж этот реальный мир и отсылки к нему, когда по реальным миром каждый понимает что-то своё.
в риальном мире так та и матиматика ненужна, и вуз, и дажи старшые классы школы. чаивые калькулятар пащитает, а граматнаст тоже ненужна ведь вы этоттекст тоже можите прачитать и панять што яимел ввиду
Как в C отличается порядок выполнения
str && str[0] == 'a'противstr & str[0] == 'a'?Agda это успешно решает вводом закорючек через аккорды. Например, ≡ — это \==, а ≗ — \circeq.
В агде это тоже решается: люди вполне успешно описывают эти значочки терминами из предметной области, например.
И это.
Да норм:
Пользователю важно, что там есть тесты? Нет. Менеджменту и бизнесу важно, что там есть тесты? Нет.
Тесты ничего не добавляют, только вынуждают раздувать код в восемь и шесть седьмых раз, чтобы добавить все нужные моки, интерфейсы, SOLID и DI. Вы знаете, что в Штатах сейчас вообще правительство DEI запретило? Это просто хотели запретить DI из-за феерического разбазаривания ресурсов на пять экранов кода на каждую функцию, но просто когда печатали текст указа, то случайно вместе с D нажали на кнопку над ней (и тесты это не поймали, обратите внимание — толку с них?).
Топ-левел-байндинги легче читать с аннотациями, нетривиальные функции легче читать с аннотациями, простые вещи и локальные переменные легче читать без аннотаций.
У вас тезис уровня «вы определитесь, или говорящие имена переменных, или
iкак индекс массива».Откуда удвоение-то?
Кто запрещает? Почему?
В чём мучение?
Мутабельность к этому не имеет вообще никакого отношения.
И там, где это важно, это пытаются минимизировать. Вы же даже не пытаетесь это сделать, а ставите те эксперименты, которые легче поставить (напихать трейсов и потом с умным видом сидеть их разглядывать), а не те, которые относятся к вашему предмету исследования (почему тормозит).
Абсолютно верно, без типов этой проблемы нет.
Вы даже сами сказали, «этот тип». Тип один, всё.
Обычная индукция/рекурсия, не вижу проблем.
Если это не часть семантики yaml, то это они зря, конечно. Но это вопрос конкретной реализации, а не теории типов.
Да, и? Вы думаете, тут цель — выпендриться и иметь в рантайме какое-то другое представление (что, кстати, делают с GADT'ами, но вы ещё не там)? Тут цель — это проверки в компилтайме, до запуска.
Какие проблемы возникают?
Эта отсылка была к тому, что ПО с дебагами и прочими трейсами ведёт себя совсем не так, как без них.
Попробуйте в следующий раз дочитывать комментарии до конца. Или хрен с ними с комментариями, фразы-то до конца дочитывайте.
А использовали бы типы — не было бы такой ерунды у вас, как вы описываете.
Нет, конечно. Она всё ещё обрабатывает ровно один тип.
А кто в языке с динамической типизацией осуществляет проверку, что вещи вне этого списка не придут, и кто отличает String как Real от String как String?
Лол ок.
На практике я бы считал приближённо и в интервальной арифметике — всё равно все данные с погрешностями. А там уже и формулы расслабить можно, и полегче будет.
Но, опять же, я ничего не знаю о предметной области.
Причём тут ФП? Мы уже тесты обсуждаем, а они совершенно не нужны. Нет ни единого проекта, в котором использовались бы тесты и который был бы полезен.
Ставь лайк, если любишь искать ключи где светлее, а не где потерял.
Бездоказательное утверждение, отсылающее к эмоциям.Причём тут вообще мутабельность и объекты?Соломенным чучелам, с которыми вы активно спорите.
В случае таймаутов от этих трейсов (вызывающего сервера, отваливающегося по таймауту вызываемого) толку, как с трейсов изнутри grep для понимания, где в приложении, пишущем логи, по которым вы грепаете, проблема.
У меня всё больше впечатление, что к разработке софта вы относитесь как-то сбоку, как ПМ или скрам-мастер там, не знаю.
То есть, это вы сказали, не я. QED.
Чем это сложнее, чем throw ошибок?
Что это вообще значит?
Чего там собирать? Это O(1) от размера кодовой базы и O(n) от количества типов ошибок, которых в стандартных оперднях очень мало.
Вы это повторяете в который раз, но в который раз отказываетесь пояснить, какое отношение АДТ имеют к динамической типизации.
То, что в инте может быть 0, может быть 1, а может быть 42 — это случайно не проявления динамической типизации, кстати?
Да, абсолютно бессмысленное упражнение, ведь между кодом на Rust и Python нет никакой разницы по характеристикам исполнения.
Я боюсь, вы даже не понимаете, в каком смысле тут упоминалась невычислимость. Это, конечно, очень смешно.
Не все базисы, по которым раскладывается intrinsic-сложность систем, одинаково полезны. ООП — неудачный базис [в большинстве задач, и в подавляющем большинстве задач, с которыми сталкивался лично я]. ФП (в смысле типов) — куда более удачный базис [снова в большинстве задач].
Модули ядра ты пишешь через POSIX?
А мне норм. Я как-то раз спокойно в 2019-м году взял компилятор, написанный мной в начале 2017-го и с тех пор не обновлявшийся, поменял в stack.yaml резолвер на актуальный stackage lts, потратил где-то 10 минут на выковыривание устаревших методов из кодовой базы в несколько тыяч строк, и всё после этого сразу заработало (получив заодно где-то ЕМНИП 20% прироста производительности тупо за счёт обновления компилятора и библиотек).
Эээ, я тут открыл для себя ghcup и последние года три получаю свежий ghc оттуда, так что не в курсе — а что там поломали?
Не видел ни одной компании, где отсутствие бутстраппинга являлось бы ключевым препятствием перед корпоративной красной лентой. Основная сложность в нашей общей компании-то была ЕМНИП в том, чтобы убедить
клоуновактёров из этого театра дать blanket permission на либы в hackage.Кстати, как там gcc нынче бутстрапится, и кому это мешает?
Не просто безграмотность, а воинственная безграмотность.
Подразумевая, что вы имели в виду индекс массива, то это встроенный тип
Fin, параметризованный (гошники зажмурились) длиной (все остальные зажмурились) массива. Функцияне может выйти за границы вообще никогда, для любого массива любой длины, полученного откуда угодно, хотя
ArrayиFinявляются библиотечными типами.Как вы могли устать отвечать, если ни единого ответа на это от вас не было?
Как можно игнорировать то, чего нет?
Я вам снова на примере показал, как это количество сократить до
round $ 1 / (1 + 12)= 8%, а вы снова это игнорируете.Абсолютно верно. Бизнесу не нужны тесты и аджайл. Бизнесу нужен работающий код. Ваше слепое поклонение тестам совершенно необоснованно.
Что вы устали? Игнорировать эмпирические данные? Так вы и в прошлый раз это скипали и не отвечали по существу. Я вам пример, как разделение на чистые и нечистые функции не увеличивает объём кода, вы продолжаете бегать с «в два, нет, в три, нет, в десять раз больше пять экранов текста!»
Это тупейший клей между рантайм-системой и вашей бизнес-логикой. Там нечего тестировать.
Карго-культ и секта.
Ну так см. последний абзац.
Или
Data.String.Interpolate.Чем меняют поведение наблюдаемой системы и её перф-характеристики.
Там, где я работал и где скорость ответа действительно была важна и приводила к более плачевным денежным исходам, чем «юзер монополиста подождёт вызова такси не 5 секун, а 10, и с вероятностью 1% в следующий раз предпочтёт идти пешком», это не работало. Работает только снятие полного дампа трафика и дальше уже существенно более тяжёлая артиллерия, чем дебаг-данные, трейсы ошибок и профайлинг средствами языка/окружения.
Впрочем, это так, лирика. Лучше скажите, как тут помогают трейсы исключений? Вы до таймаутов и прочих проблем на проде на них вообще забиваете, что ли, лол?
Так там нету.
Что сложнее? Как раз проще: понятно, что может завершиться ошибкой (и какой), а что — нет.
Бездоказательное утверждение.
Получили статические гарантии. Это лучше.
Только его и не было.
При разработке или на проде? В первом случае вы код прямо пишете сейчас новый, какие там глубокие стектрейсы для ваших кеширующих микросервисов? Во втором случае, может, есть какая-то связь с отсутствием выразительных типов?
Да не, снова ерунда.
После ваших просьб в разговоре об ФП написать аналог вашей функции на SQL (до сих пор лолирую) или черри-пикинга отдельных библиотек в отдельном языке я на вашем месте бы не стал про это даже вспоминать.
Да не, вы просто инструменты путаете. Вы говорите об экзепшонах, когда дело в какой-нибудь там виртуальной машине для джавы или дотнета (в которых я не шарю совсем, поэтому не смогу поддержать разговор), которая может выборочно и чуть ли не ретроспективно собирать трейсы, деоптимизировать, и так далее.
Соответственно, законы физики и теории вычислимости не мешают тому же .NET CLR записывать трейс каждый раз, когда вы в F# возвращаете его аналог
Left, или мне наваять за пару вечеров плагин к ghc, который каждой функции будет добавлять констрейнтHasCallStack, чтобы потом его захватывать в моей собственной иерархии ошибок.Просто это всё нафиг никому не нужно, потому что ценность трейсов в сильно типизированных языках переоценена. Это как жаловаться, что JS безапелляционно лучше C++, потому что в JS есть
eval.Только при этом они есть даже в питоне. Просто спецификации формата — это, внезапно, спецификации формата, которые нужны, чтобы показать, условно, сколько знаков после запятой печатать, а не что-то там затыкать. Использование
%dили%fв том же питоне — это просто дань традиции, чтобы программистам из других языков было проще и привычнее.Нет никаких причин, почему нельзя было бы писать просто
%в хаскельном printf — типы аргументов всё равно известны статически, и как их печатать, тоже известно статически. Просто WTF-момент от простых процентов больше, чем экономия пары знаков.А написать типизированный принтф, терм которого после частичного применения к чему-нибудь вроде
имел бы тип
Show a ⇒ Show b ⇒ a → b → String, даже проще, чем париться с полноценным разбором строки форматирования в компилтайме и последующим тайпчекингом аргументов.