но если интересны подробности, то в такси был большой картографический блок (с нуля написанный) плюс система сбора/хранения координат/треков водителей, при том, что по ней нужно быстро искать понятие "ближайший".
Знаете какой самый козырный и самый масштабируемый способ её решать? Если конечно плевать на перфекционизм? И, главное, не лезть во всякие градиентные спуски и прочую псевдоматематическую ненужность.
Да конечно не нужно. Это всё вообще никогда не нужно.
Я недавно форму заполнял на 6 экранов и примерно сотню полей суммарно, и к концу её валидация занимала минуты две при каждом изменении формы. Почему? Потому, что литкод-маэстро нечистых функций, её писавшие, тоже сделяли х-к х-к и в продакшен, и в итоге у них там алгоритм Шлемиеля, ведущий к тому, что первое поле проверяется при проверке первого, второго и последующих, второе — при проверке второго и последующих, и так далее, и в итоге O(n²) на ровном месте. И на каждое поле они отправляли запрос на сервер и обратно.
Зачем? Почему? Потому, что на их игрушечных данных всё работало, можно релизить MVP!
точно-точно! переписывают на микросервисы
Какое отношение микросервисы имеют к обсуждаемому вопросу?
Покрытие тестами около 80%.
До сих пор не понимаю, зачем тесты писать. Только замедляют работу :shrug:
И обратно, абсолютно так же все пока что упомянутые вами возражения против типизации работают и как возражения против тестов. И экранов кода там больше, и бро из соседнего комментария с MVP тестами не пользовался.
Как они помогают прийти к нужному результату? Они только мешают, их обновлять надо, поддерживать, все дела. А так нафигачил и го в прод. Я вот на одном проекте без тестов фигачил и очень быстро всё сделал, триллионы долларов заработали.
Нет, вы не просили аргументов. Вы сказали, что ваше эмпирическое мнение — что всего лишь 1% функций чистые. На это я ответил, что либо вы неправильно декомпозируете задачу, либо просто у вас такие задачи, где бизнес-логики толком нет, а есть только перекладывание жсонов.
В ответ на это можно было бы рассказать, например, подробности про решаемые задачи, а вы зачем-то стали пускать пыль в глаза про Яндекс.Лавку.Такси.Алису.
высокомерное
Лол, с такой чувствительностью к критике картина становится всё более цельной.
знаете, как, например, появилась Яндекс-лавка?
Не знаю и не очень интересно, потому что дальше снова какое-то непроверяемое пускание пыли в глаза, которое вообще не имеет никакого отношения к долгосрочной поддерживаемости кода (как вам расскажет любой эффективный менеджер, срезающий косты и рапортующий об успехах, а после него — хоть потоп).
а сейчас в лавке НЕговнокодит уже около 100 человек. Но клиент не видит результатов их труда, увы
Подчищают за вами, видимо.
У меня тоже такой пример перед глазами есть. Был на одной моей работе чувак, и начал он разрабатывать одну, скажем, фичу. Пре-MVP выкатился очень быстро, потому что чувак максимально срезал углы. Про это написали в анонсе новой версии, бизнес пипл что-то там оценили, что это привлекло 100500 новых клиентов и денег и вызвало энтузиазм, и все радостно получили бонусы.
Проблема в том, что чувак срезал углы. Поддерживать и развивать эту кодовую базу за пределами пре-MVP было очень больно: добавляешь что-то в одном месте, так в другом разваливается. С этого проекта за моё время там ушло трое других людей потому, что над ним невозможно работать, не удалось найти никого другого, кто хотел бы им заниматься, бизнес пипл пришлось всё время придумывать, почему обещанные фичи не реализуются, исходный чувак с бонусом и красивой строчкой резюме упорхал в следующую компанию, а исходные менеджеры, выписавшие ему и себе бонусы, тоже куда-то там упорхали.
Но да, в глазах общественности чувак молодец и гений, а все остальные — туповатые лентяи, раз ничего не могут после него сделать.
прибыли, понимаете, похрен: говнокод там или нет
Ещё выгоднее веществами барыжить или там, не знаю, pump & dump на шиткоинах. Может, ну его нафиг это программирование?
плевать на ошибки в коде, отлавливая их где-нибудь "наверху": грохнулось — перезапустили, а потом на статистику ошибок поглядели и что-то поправили, или даже оставили так
Потом, правда, Алиса кладёт весь NTP, с диска C: всё удаляется, и так далее, но это ничего страшного, просто посмотрим статистику ошибок и что-то поправим.
А если не секрет, зачем вообще с таким подходом тесты писать? Написали код, запустили-потыкали пару раз, вроде работает ⇒ деплоим в прод. Если что-то навернётся — тоже перезапустили, статистика ошибок, оставили так.
Аргументы по существу кончились (вернее, их и не было изначально), и пошёл спердоб/адхом? Ну как хотите.
это не я живу в нечистом мире, это Вы пытаетесь от него абстрагироваться
Да, потому что, ещё раз, тогда проще и разрабатывать, и тестировать, и рассуждать о коде. Это (более частными терминами и с большими костылями) пишут в каждой первой книжке по архитектуре ПО — dependency injection, SRP, какая-нибудь там гексагональная архитектура, и прочая ерунда.
Короче, не вижу в этом ничего плохого. А вот так патологически бороться за говнокодинг, как вы это делаете — это я не очень понимаю. Зачем так делать?
вот тем, к чему я руку приложил, вы точно скорее всего пользовались: яндекс. такси, яндекс.лавка.
А, понятно, зачем. Просто вы — из того сорта яндексистов, которые наслаждаются своей элитарностью, которая им даруется местом, где они просиживают штаны и говнокодят (ведь они же прошли все литкод-интервью в Яшечку!). Притом, что говнокодинг в Яндексе — это тоже притча во языцех (фокус на литкодинге к другим результатам и не приводит). Я бы не хотел идти работать в Яндекс.
И нет, не пользовался ни одним из них.
но там вообще и запаха типов и иммутабельности нет, уж извините.
Здесь мы обсуждаем чистоту. И расчёт путей и цен — не чистая задача? Поиск ближайших таксистов и соотнесение их с заказчиками — не чистая задача?
а что сделали Вы?
Ничего, конечно же. Я ж только языком трепать могу, сорьки, куда мне до Маэстро Литкода.
Они добавляют воздействия на изначально неустойчивую систему.
Мои (скудные, впрочем) знания об энергосистемах заставляют меня думать, что энергосистема — это всегда неустойчивая система. Из отрицательных обратных связей там разве что только локальный возврат частоты некоторых видов генераторов к базовой частоте сети, а почти все остальные обратные связи — положительные. Но, впрочем, этот вопрос я изучал поверхностно для базового ознакомления с предметной областью, когда занимался моделированием генерации ветряков как одним из рабочих проектов по машинному обучению, да и давно это было.
И, короче, это означает, что это (расшатывающее) воздействие нужно дополнительно парировать (например, аккумуляторами, а лучше — простаивающими резервами натгаза/угля, потому что штиль и облака могут быть долго), что повышает суммарную стоимость, и что зелёные атомофобы не учитывают.
Ну, в лучшем случае не учитывают. Пару лет назад мне какой-то клоун тут рассказывал, что ну ничё страшного, поживём с регулярными вечерними rolling blackout'ами ради светлого будующего, которое наступит, когда солары и ветряки станут надёжными (как достичь этой прекрасной поры, правда, не уточнялось).
"Я хорошо выпил вчера, опёрся на кирпичную стену, и она развалилась. Но строители здесь ни при чём, это надо меньше пить и аккуратнее передвигаться".
Я по-прежнему склонен считать, что более близкой аналогией будет таки вождение под градусом, но это вопрос количественного сравнения разных причин... вернее, сравнения вашего и моего количественного сравнения разных причин блэкаута 2021-го, и я не уверен, что это влезет в комментарии.
К сожалению (я тоже не люблю топологию), похоже, без этого никуда. Лучше всего взять какую-нибудь лайтовую книжку по топологии и просто по ней пробежаться-прорешать задачи, чтобы развить топологическую интуицию. Introduction to Topology: Pure and Applied, например, меня порадовала (и там в конце главы с прикольными прикладными задачами, что хороший отдых от всей этой фундаментальной абстрактщины). Только заранее рекомендую открыть её errata и держать рядом — там есть ошибки и опечатки.
Поэтому вопрос к тем кто глубоко в теме: что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Ничего не могу сказать, к сожалению (но я ненастоящий сварщик).
Математика — это просто наука о том, как обращаться с закорючками по правилам, а основания математики — это кусочек этой науки, в котором закорючками являются правила обращения с другими закорючками.
Насколько я могу судить, физикам вся эта глубокая муть не нужна: они счастливо работают с наивной математикой по большому счёту 19-го века, и им норм. Я по разным причинам наиболее интересуюсь теорией топосов, и если смотреть на работы теоретических физиков по их применению, например, в качестве оснований (а не языка для выражения), то там дело ограничивается очень узким множеством статей вроде таких — https://arxiv.org/pdf/2110.06793 или https://arxiv.org/pdf/1106.5660 , у которых цитирований по десятку-другому максимум (то есть, физикам эта тема не очень интересна, а ИМХО если уж что из оснований и может претендовать на прорывные результаты, так это топосы).
И, например, не придумано экспериментов, способных фальсифицировать наличие или отсутствие C в ZF+C-аксиоматике нашего мира (я склонен считать, что парадокс Банаха-Тарского ближе к нереализуемым бесконечностям, чем к отсутствию C, и если для вас он что-то опровергает, то в вашем мире не должно существовать и, скажем, всего множества вещественных чисел), или отличить ZF+C от других аксиоматик, или сказать, описывается наш мир классической или конструктивной логикой.
Но это всё, конечно, не значит, что таких экспериментов не может быть. И даже если вдруг окажется, что в нашем мире C нет, или логика классическая, то это не делает ZF+C и классическую логику более плохой математикой.
Основания математики по определению замкнуты на себя самих.
Почему? Многие разделы чистой математики вполне себе имеют практическую пользу в обучении и могут сильно помочь в глубоком понимании прикладной математики и ее практическом применении. Нужно смотреть шире, у нас всегда много неявных (неочевидных) связей.
Если вкратце, то потому что чистые математики редко этим руководствуются, и польза вне самой чистой математики оказывается скорее случайным побочным эффектом, чем результатом целенаправленной работы.
А как мы ее тогда в теорем-прувере формализовать будем?
Как обычно и как любую другую теорию, просто используя прувер как метаязык.
Именно, что "почему-то". Подозреваю - что из за контингента участников: вряд ли там большинство составляют программисты "с земли", на этой самой земле пашущие как папы Карло.
Всех теоретиков, обмазывающихся эндофункторами в моноидальных категориях, уже всосал хаскель. В плюсах остались практики (например, Бен Дин, пашущий как папа Карло в геймдеве в Blizzard).
А разгадка проста: монады дают очень продуктивный базис для декомпозиции кода, и при этом не обязательно понимать, откуда они берутся «теоретически».
И вообще, у меня лично сложилось впечатление, что в какой-то момент C++ пошел не в ту сторону, и началось это ещё где-то со SFINAE, когда template стало возможным использовать не как подсобное средство, а для "метапрограммирования"
В идеальном мире у нас есть нормальный метаязык времени компиляции. Но что делать в реальном мире? Макросы? Внешняя кодогенерация? Писать всё на лиспе или хаскеле с дженериками и TH?
Неужто изолированные участки энергосети лучше, чем единая энергосистема?
Большинство связей между сегментами идут переменным током, а это означает, что надо поддерживать синхронизацию (что имеет определённые сложности). DC ties не требуют синхронизации, но их делать тяжелее на высокую мощность.
А во-вторых, далеко не все функции сводятся к чистым (моё эмпирическое мнение - не более 1% в реальном мире)
Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Ну либо решаемые задачи — «принять жсон отсюда и переложить как есть туда». Не знаю, что в таком случае тестировать или обкладывать типами (хотя параметризм мог бы помочь).
Тест для функции, сохраняющей данные в файл
Эта функия называется Data.ByteString.Lazy.writeFile. Что вы там тестировать собрались? Она уже протестирована авторами библиотеки bytestring.
Ну и по предыдущему комментарию:
Я просил, чтобы мне показали http-сервер без тестов, но мне не показали.
Когда-то давно писал тестовым заданием на прикладного хаскелиста маленькую http api-шку, которая получает картинку, распознает там объекты и складывает в БД (а потом возвращает обратно, если что).
Сервер — поверх servant. Там (в самом сервере) просто нечего было тестировать, все типами описано и компилятором проверяется.
А тесты были только уровня интеграционных и только для «бизнес-логики», которая вполне себе реализуется чистыми функциями, и которую так писать даже удобнее, опять же. В более выразительном языке и это можно было бы покрыть типами.
Это уже не первый блэкаут. В предыдущий раз (примерно где-то в 2005-м)
В 2011-м. Системных блекаутов за последние лет 40 было три: в 1989-м, в 2011-м и в 2021-м, и все три — из-за очень нехарактерных погодных условий. При этом в 2011-м не было такого же, как в 89-м и 21-м: всего-то rolling blackout'ы в большей части затронутых мест на один день (а не полное отключение на два с половиной дня).
При этом цены на электричество в 0.1 доллар за кВт-час означают, что среднее домохозяйство за год сэкономит где-то 0.1 × 1.6 × 10⁴ = 2.2 тысячи долларов (ещё раз, за год), на что можно купить воттакенный генератор, manual transfer switch, и топлива к нему, и обеспечить себе энергетическую безопасность не только от системных блекаутов, но и от условного пожара на подстанции в те же +42, врезавшегося в столб автомобилиста, или тому подобных вещей. А за четыре года можно купить какой-нибудь батарейный блок этак на 10 киловатт-часов.
Спасибо, но между 100%-стабильной региональной системой (которых не бывает, к слову) и электричеством на 15 центов дешевле для меня выбор очевиден, и я не понимаю тех, кто выбирает первое.
ветряков почти не было, а блэкаут всё равно случился.
«Сегодня я выпил перед тем, как сел за руль, и попал в аварию, но алкоголь ни при чём, так как другие люди попадают в аварии и трезвыми.»
где на бестиповом языке писали 1-2 строки, на типовом теперь пишут 1-2 экрана да и ещё иммутабельность пропагандируют, с которой 1-2 экрана превращается в 5-10.
А почему не 50-100?
Аннотации типов в большинстве мейнстримных языков с продвинутой системой типов нужны мало где, поэтому оверхед по писанине от типизации сильно меньше (а при чтении он из оверхеда превращается во благо, кстати), и он существенно меньше, чем выигрыш на становящихся ненужными тестах.
с типами компиляторы писать проще
И снова нет. Тайпчекер — весьма нетривиальная часть компилятора, и куда проще просто забить и напихать рантайм-проверки.
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения, тем быстрее при прочих равных будет ваша программа.
Не очень применимый к чистой математике вопрос. Лучше спрашивать «весело ли это» и «что получится».
В прикладных задачах ничего особо интересного не получится. Весело ли это? Кому как.
Т.е. выводить теорию множеств из теории категорий
Сделано в ETCS. Полезна тем, что можно обобщать над аксиоматикой теории множеств.
а теорию категорий из теории типов?
Я бы не стал, получится неудобная и неизящная конструкция.
Да, у нас есть системы типов, и есть классы категорий, реализующие внутреннюю логику этих систем типов, но формулировать эти вещи лучше по отдельности и строить соответствие пропозиционально, а не дефиниционально, так сказать.
Вообще, конечно, смешно: и многие другие, и я лично задали вам кучу вопросов или высказали кучу утверждений, на которые можно что-то сказать по существу. Вы выбираете продолжать вот эту максимально жириновскую ветку на этой странице в максимально жириновском стиле, что смешно вдвойне, учитывая её начало.
Лично мне было бы куда интереснее услышать, почему верящие в науку люди выбирают объект верований именно так, но та ветка кончилась, а жаль.
Если бы ветер занимал бОльшую часть генерации, то его было бы справедливо обвинять в блэкаутах
Второй раз настоятельно рекомендую перечитать исходный комментарий, на который вы отвечали изначально, где написано «тоже» перед «как-то виноваты».
Кстати, ветер - это недиспетчеризуемый источник энергии.
Это как раз примерно то, что мы тут обсуждаем.
Я смотрел в районе блэкаута 15 февраля.
А надо смотреть не в три часа дня понедельника, когда блекаут уже полсуток как был, а в 1-2 ночи, когда он начался (ну, если вы хотите понять, почему он начался, конечно). И тогда вы увидите, что ветер в тот момент начала блекаута упал с примерно 9.5 ГВт пика предыдущего дня и 23 ГВт пика предыдущей недели до где-то 4.8 ГВт, ровно в тот момент, когда начались отключения. А газ в этот момент упал с примерно 44 гигаватт до 33.
27 ГВт газа чуть позже полдня того же дня — это эластичность генерации (днём на обогрев нужно меньше энергии, и солары хотя бы в это время работают), а не остановившиеся непроизвольно по техническим причинам электростанции.
Плюс, если вы действительно хотите понять, почему начался блекаут, то стоит озаботиться более глубоким ковырянием цепочки событий. И если вы этим займётесь, то обнаружите, что существенной проблемой, помимо прочих, было прекращение подачи энергии на, условно, насосы и обогревалки для газопроводов, потому что они не всегда подаются от той же электростанци, которую обеспечивают, а операторы других электростанций не были информированы, кого отключать точно нельзя.
Поэтому каждый пропавший ватт с вашей электростанции пропадает из электросети с вероятностью 1 и вдобавок утягивает за собой ещё сколько-то ватт с вероятностью k > 0. Поэтому чем более надёжной была бы генерация, тем меньше следующей генерации бы утащилось, и так суперлинейно (или, по крайней мере, с сильно более чем единичным коэффициентом).
Звучит как чистые функции.
И это тоже.
Не ожидал другого.
Да конечно не нужно. Это всё вообще никогда не нужно.
Я недавно форму заполнял на 6 экранов и примерно сотню полей суммарно, и к концу её валидация занимала минуты две при каждом изменении формы. Почему? Потому, что литкод-маэстро нечистых функций, её писавшие, тоже сделяли х-к х-к и в продакшен, и в итоге у них там алгоритм Шлемиеля, ведущий к тому, что первое поле проверяется при проверке первого, второго и последующих, второе — при проверке второго и последующих, и так далее, и в итоге O(n²) на ровном месте. И на каждое поле они отправляли запрос на сервер и обратно.
Зачем? Почему? Потому, что на их игрушечных данных всё работало, можно релизить MVP!
Какое отношение микросервисы имеют к обсуждаемому вопросу?
До сих пор не понимаю, зачем тесты писать. Только замедляют работу :shrug:
Абсолютно та же логика работает с типами.
И обратно, абсолютно так же все пока что упомянутые вами возражения против типизации работают и как возражения против тестов. И экранов кода там больше, и бро из соседнего комментария с MVP тестами не пользовался.
Как они помогают прийти к нужному результату? Они только мешают, их обновлять надо, поддерживать, все дела. А так нафигачил и го в прод. Я вот на одном проекте без тестов фигачил и очень быстро всё сделал, триллионы долларов заработали.
Что не так?
Нет, вы не просили аргументов. Вы сказали, что ваше эмпирическое мнение — что всего лишь 1% функций чистые. На это я ответил, что либо вы неправильно декомпозируете задачу, либо просто у вас такие задачи, где бизнес-логики толком нет, а есть только перекладывание жсонов.
В ответ на это можно было бы рассказать, например, подробности про решаемые задачи, а вы зачем-то стали пускать пыль в глаза про Яндекс.Лавку.Такси.Алису.
Лол, с такой чувствительностью к критике картина становится всё более цельной.
Не знаю и не очень интересно, потому что дальше снова какое-то непроверяемое пускание пыли в глаза, которое вообще не имеет никакого отношения к долгосрочной поддерживаемости кода (как вам расскажет любой эффективный менеджер, срезающий косты и рапортующий об успехах, а после него — хоть потоп).
Подчищают за вами, видимо.
У меня тоже такой пример перед глазами есть. Был на одной моей работе чувак, и начал он разрабатывать одну, скажем, фичу. Пре-MVP выкатился очень быстро, потому что чувак максимально срезал углы. Про это написали в анонсе новой версии, бизнес пипл что-то там оценили, что это привлекло 100500 новых клиентов и денег и вызвало энтузиазм, и все радостно получили бонусы.
Проблема в том, что чувак срезал углы. Поддерживать и развивать эту кодовую базу за пределами пре-MVP было очень больно: добавляешь что-то в одном месте, так в другом разваливается. С этого проекта за моё время там ушло трое других людей потому, что над ним невозможно работать, не удалось найти никого другого, кто хотел бы им заниматься, бизнес пипл пришлось всё время придумывать, почему обещанные фичи не реализуются, исходный чувак с бонусом и красивой строчкой резюме упорхал в следующую компанию, а исходные менеджеры, выписавшие ему и себе бонусы, тоже куда-то там упорхали.
Но да, в глазах общественности чувак молодец и гений, а все остальные — туповатые лентяи, раз ничего не могут после него сделать.
Ещё выгоднее веществами барыжить или там, не знаю, pump & dump на шиткоинах. Может, ну его нафиг это программирование?
Потом, правда, Алиса кладёт весь NTP, с диска C: всё удаляется, и так далее, но это ничего страшного, просто посмотрим статистику ошибок и что-то поправим.
А если не секрет, зачем вообще с таким подходом тесты писать? Написали код, запустили-потыкали пару раз, вроде работает ⇒ деплоим в прод. Если что-то навернётся — тоже перезапустили, статистика ошибок, оставили так.
Аргументы по существу кончились (вернее, их и не было изначально), и пошёл спердоб/адхом? Ну как хотите.
Да, потому что, ещё раз, тогда проще и разрабатывать, и тестировать, и рассуждать о коде. Это (более частными терминами и с большими костылями) пишут в каждой первой книжке по архитектуре ПО — dependency injection, SRP, какая-нибудь там гексагональная архитектура, и прочая ерунда.
Короче, не вижу в этом ничего плохого. А вот так патологически бороться за говнокодинг, как вы это делаете — это я не очень понимаю. Зачем так делать?
А, понятно, зачем. Просто вы — из того сорта яндексистов, которые наслаждаются своей элитарностью, которая им даруется местом, где они просиживают штаны и говнокодят (ведь они же прошли все литкод-интервью в Яшечку!). Притом, что говнокодинг в Яндексе — это тоже притча во языцех (фокус на литкодинге к другим результатам и не приводит). Я бы не хотел идти работать в Яндекс.
И нет, не пользовался ни одним из них.
Здесь мы обсуждаем чистоту. И расчёт путей и цен — не чистая задача? Поиск ближайших таксистов и соотнесение их с заказчиками — не чистая задача?
Ничего, конечно же. Я ж только языком трепать могу, сорьки, куда мне до Маэстро Литкода.
Мои (скудные, впрочем) знания об энергосистемах заставляют меня думать, что энергосистема — это всегда неустойчивая система. Из отрицательных обратных связей там разве что только локальный возврат частоты некоторых видов генераторов к базовой частоте сети, а почти все остальные обратные связи — положительные. Но, впрочем, этот вопрос я изучал поверхностно для базового ознакомления с предметной областью, когда занимался моделированием генерации ветряков как одним из рабочих проектов по машинному обучению, да и давно это было.
И, короче, это означает, что это (расшатывающее) воздействие нужно дополнительно парировать (например, аккумуляторами, а лучше — простаивающими резервами натгаза/угля, потому что штиль и облака могут быть долго), что повышает суммарную стоимость, и что зелёные атомофобы не учитывают.
Ну, в лучшем случае не учитывают. Пару лет назад мне какой-то клоун тут рассказывал, что ну ничё страшного, поживём с регулярными вечерними rolling blackout'ами ради светлого будующего, которое наступит, когда солары и ветряки станут надёжными (как достичь этой прекрасной поры, правда, не уточнялось).
Я по-прежнему склонен считать, что более близкой аналогией будет таки вождение под градусом, но это вопрос количественного сравнения разных причин... вернее, сравнения вашего и моего количественного сравнения разных причин блэкаута 2021-го, и я не уверен, что это влезет в комментарии.
К сожалению (я тоже не люблю топологию), похоже, без этого никуда. Лучше всего взять какую-нибудь лайтовую книжку по топологии и просто по ней пробежаться-прорешать задачи, чтобы развить топологическую интуицию. Introduction to Topology: Pure and Applied, например, меня порадовала (и там в конце главы с прикольными прикладными задачами, что хороший отдых от всей этой фундаментальной абстрактщины). Только заранее рекомендую открыть её errata и держать рядом — там есть ошибки и опечатки.
Ничего не могу сказать, к сожалению (но я ненастоящий сварщик).
Математика — это просто наука о том, как обращаться с закорючками по правилам, а основания математики — это кусочек этой науки, в котором закорючками являются правила обращения с другими закорючками.
Насколько я могу судить, физикам вся эта глубокая муть не нужна: они счастливо работают с наивной математикой по большому счёту 19-го века, и им норм. Я по разным причинам наиболее интересуюсь теорией топосов, и если смотреть на работы теоретических физиков по их применению, например, в качестве оснований (а не языка для выражения), то там дело ограничивается очень узким множеством статей вроде таких — https://arxiv.org/pdf/2110.06793 или https://arxiv.org/pdf/1106.5660 , у которых цитирований по десятку-другому максимум (то есть, физикам эта тема не очень интересна, а ИМХО если уж что из оснований и может претендовать на прорывные результаты, так это топосы).
И, например, не придумано экспериментов, способных фальсифицировать наличие или отсутствие C в ZF+C-аксиоматике нашего мира (я склонен считать, что парадокс Банаха-Тарского ближе к нереализуемым бесконечностям, чем к отсутствию C, и если для вас он что-то опровергает, то в вашем мире не должно существовать и, скажем, всего множества вещественных чисел), или отличить ZF+C от других аксиоматик, или сказать, описывается наш мир классической или конструктивной логикой.
Но это всё, конечно, не значит, что таких экспериментов не может быть. И даже если вдруг окажется, что в нашем мире C нет, или логика классическая, то это не делает ZF+C и классическую логику более плохой математикой.
Основания математики по определению замкнуты на себя самих.
Если вкратце, то потому что чистые математики редко этим руководствуются, и польза вне самой чистой математики оказывается скорее случайным побочным эффектом, чем результатом целенаправленной работы.
Как обычно и как любую другую теорию, просто используя прувер как метаязык.
Всех теоретиков, обмазывающихся эндофункторами в моноидальных категориях, уже всосал хаскель. В плюсах остались практики (например, Бен Дин, пашущий как папа Карло в геймдеве в Blizzard).
А разгадка проста: монады дают очень продуктивный базис для декомпозиции кода, и при этом не обязательно понимать, откуда они берутся «теоретически».
В идеальном мире у нас есть нормальный метаязык времени компиляции. Но что делать в реальном мире? Макросы? Внешняя кодогенерация? Писать всё на лиспе или хаскеле с дженериками и TH?
Большинство связей между сегментами идут переменным током, а это означает, что надо поддерживать синхронизацию (что имеет определённые сложности). DC ties не требуют синхронизации, но их делать тяжелее на высокую мощность.
Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Ну либо решаемые задачи — «принять жсон отсюда и переложить как есть туда». Не знаю, что в таком случае тестировать или обкладывать типами (хотя параметризм мог бы помочь).
Эта функия называется
Data.ByteString.Lazy.writeFile. Что вы там тестировать собрались? Она уже протестирована авторами библиотекиbytestring.Ну и по предыдущему комментарию:
Когда-то давно писал тестовым заданием на прикладного хаскелиста маленькую http api-шку, которая получает картинку, распознает там объекты и складывает в БД (а потом возвращает обратно, если что).
Сервер — поверх servant. Там (в самом сервере) просто нечего было тестировать, все типами описано и компилятором проверяется.
А тесты были только уровня интеграционных и только для «бизнес-логики», которая вполне себе реализуется чистыми функциями, и которую так писать даже удобнее, опять же. В более выразительном языке и это можно было бы покрыть типами.
В 2011-м. Системных блекаутов за последние лет 40 было три: в 1989-м, в 2011-м и в 2021-м, и все три — из-за очень нехарактерных погодных условий. При этом в 2011-м не было такого же, как в 89-м и 21-м: всего-то rolling blackout'ы в большей части затронутых мест на один день (а не полное отключение на два с половиной дня).
При этом цены на электричество в 0.1 доллар за кВт-час означают, что среднее домохозяйство за год сэкономит где-то 0.1 × 1.6 × 10⁴ = 2.2 тысячи долларов (ещё раз, за год), на что можно купить воттакенный генератор, manual transfer switch, и топлива к нему, и обеспечить себе энергетическую безопасность не только от системных блекаутов, но и от условного пожара на подстанции в те же +42, врезавшегося в столб автомобилиста, или тому подобных вещей. А за четыре года можно купить какой-нибудь батарейный блок этак на 10 киловатт-часов.
Спасибо, но между 100%-стабильной региональной системой (которых не бывает, к слову) и электричеством на 15 центов дешевле для меня выбор очевиден, и я не понимаю тех, кто выбирает первое.
«Сегодня я выпил перед тем, как сел за руль, и попал в аварию, но алкоголь ни при чём, так как другие люди попадают в аварии и трезвыми.»
Ветряки разбалансируют систему. Запас прочности меньше.
Притом, что они добавляют неустойчивости.
Да, там масштабные производители электричества обменялись телефончиками и теперь знают, кого отключать не надо.
А почему не 50-100?
Аннотации типов в большинстве мейнстримных языков с продвинутой системой типов нужны мало где, поэтому оверхед по писанине от типизации сильно меньше (а при чтении он из оверхеда превращается во благо, кстати), и он существенно меньше, чем выигрыш на становящихся ненужными тестах.
И снова нет. Тайпчекер — весьма нетривиальная часть компилятора, и куда проще просто забить и напихать рантайм-проверки.
Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения, тем быстрее при прочих равных будет ваша программа.
Не очень применимый к чистой математике вопрос. Лучше спрашивать «весело ли это» и «что получится».
В прикладных задачах ничего особо интересного не получится. Весело ли это? Кому как.
Сделано в ETCS. Полезна тем, что можно обобщать над аксиоматикой теории множеств.
Я бы не стал, получится неудобная и неизящная конструкция.
Да, у нас есть системы типов, и есть классы категорий, реализующие внутреннюю логику этих систем типов, но формулировать эти вещи лучше по отдельности и строить соответствие пропозиционально, а не дефиниционально, так сказать.
Смешались в кучу кони, либертарианцы, вода, Уругвай.
Конечно! У Уругвая ж вон получилось.
Вообще, конечно, смешно: и многие другие, и я лично задали вам кучу вопросов или высказали кучу утверждений, на которые можно что-то сказать по существу. Вы выбираете продолжать вот эту максимально жириновскую ветку на этой странице в максимально жириновском стиле, что смешно вдвойне, учитывая её начало.
Лично мне было бы куда интереснее услышать, почему верящие в науку люди выбирают объект верований именно так, но та ветка кончилась, а жаль.
Нет. У вас представления, как бы наглядно пояснить… короче, уровня телевизионной пропаганды про загнивающий запад.
Второй раз настоятельно рекомендую перечитать исходный комментарий, на который вы отвечали изначально, где написано «тоже» перед «как-то виноваты».
Это как раз примерно то, что мы тут обсуждаем.
А надо смотреть не в три часа дня понедельника, когда блекаут уже полсуток как был, а в 1-2 ночи, когда он начался (ну, если вы хотите понять, почему он начался, конечно). И тогда вы увидите, что ветер в тот момент начала блекаута упал с примерно 9.5 ГВт пика предыдущего дня и 23 ГВт пика предыдущей недели до где-то 4.8 ГВт, ровно в тот момент, когда начались отключения. А газ в этот момент упал с примерно 44 гигаватт до 33.
27 ГВт газа чуть позже полдня того же дня — это эластичность генерации (днём на обогрев нужно меньше энергии, и солары хотя бы в это время работают), а не остановившиеся непроизвольно по техническим причинам электростанции.
Плюс, если вы действительно хотите понять, почему начался блекаут, то стоит озаботиться более глубоким ковырянием цепочки событий. И если вы этим займётесь, то обнаружите, что существенной проблемой, помимо прочих, было прекращение подачи энергии на, условно, насосы и обогревалки для газопроводов, потому что они не всегда подаются от той же электростанци, которую обеспечивают, а операторы других электростанций не были информированы, кого отключать точно нельзя.
Поэтому каждый пропавший ватт с вашей электростанции пропадает из электросети с вероятностью 1 и вдобавок утягивает за собой ещё сколько-то ватт с вероятностью k > 0. Поэтому чем более надёжной была бы генерация, тем меньше следующей генерации бы утащилось, и так суперлинейно (или, по крайней мере, с сильно более чем единичным коэффициентом).