человека как пример "умеющего рассуждать" не надо приводить
Если почитать мой комментарий, то можно заметить, что человека (особенно в среднем) я и не приводил как такой пример.
Более того, лично я считаю, что ЛЛМ — это не «смотрите, оно уже почти как люди, общий искусственный интеллект будет уже завтра», а скорее «смотрите, люди в среднем на самом деле почти как предсказатель токенов, естественная глупость уже вчера».
(а не верили бы в любую чушь с раскрытым ртом) не было бы всего того безумия что творится на планете
Мои наблюдения говорят, что чем больше человек считает, что его верования — самые верные верования (не называя их верованиями, конечно), тогда как большинство по тем же вопросам верят во всякую чушь, тем больше он сам верит во всякую чушь.
ЛЛМ не умеют размышлять (что бы это ни значило), но умеют, упрощая, рекурсивно генерировать следующий токен согласно некоторому распределению из обучающей выборки. Поэтому если в обучающей выборке было достаточно текстов с разговорами
на абстрактные, философские, отношенческие и прочие плохо формализуемые темы
то ЛЛМ будет выдавать вполне себе неотличимые локально от людей результаты.
А текстов было достаточно. В интернете этого много, а люди сильно более похожи друг на друга, чем может показаться.
И, кстати, чем хуже оно формализуется, тем более неотличима ЛЛМ от человека (в человеколюбиво-оптимистичном случае; в мизантропо-циничном — тем ближе ЛЛМ к максимуму по людям). На вопросах по теоркату даже топовые модели сливаются очень быстро, генерируя легко проверяемый бред уровня эквивалентности уравнений a + b = c и a = b + c. А вот на вопросах о «порекомендуй книжку почитать, если мне понравилась эта вот поэтому, а вот та не понравилась потому», или «проинтерпретируй текст этой песни», или вообще полный буллшит уровня «основываясь на истории общения и статистике по другим людям и вообще по научным данным, дай прогноз моей жизни на следующие 12 месяцев», оно показывает себя глубже и шире подавляющего большинства людей, с кем я общался.
Плюс, у меня есть впечатление, что вы сравниваете среднее по ЛЛМкам с околомаксимумом по людям. А найти хорошего человека-советчика на все эти вот темы — это, вообще говоря, известная проблема.
Этот код успешно используется десятилетиями, это конечно косвенное и статистическое доказательство, но с такими сроками и объемами вполне надежное.
А потом заголовки
В загрузчике GRUB2 выявлена 21 уязвимость
В библиотеке Libxml2, разрабатываемой проектом GNOME и применяемой для разбора содержимого в формате XML, выявлено 5 уязвимостей, две из которых потенциально могут привести к выполнению кода при обработке специально оформленных внешних данных.
Ник Велнхофер (Nick Wellnhofer), сопровождающий библиотеку libxml2, объявил, что отныне будет трактовать уязвимости как обычные ошибки. Сообщения об уязвимостях не будут рассматриваться в приоритетном порядке, а станут исправляться по мере появления свободного времени.
Уязвимости в пакетах с Kea DHCP и cyrus-imapd, позволяющие повысить привилегии в системе
Уязвимость в KDE Konsole, позволяющая выполнить код при открытии страницы в браузере
Уязвимости в PAM и libblockdev, позволяющие получить права root в системе
Уязвимость в GNU screen, позволяющая выполнить код с правами root
Дальше мне надоело копипастить заголовки из моего фида opennet, фильтрованного по «уязви». Их там дофига (NB размер скроллбара справа):
Но есть и куча книг в которых все конструкции языка С/С++ совершенно разжеваны, то есть напрямую доказаны, разве вы не знаете об этом?
Я боюсь, что вы не понимаете, что такое доказательство.
Если вас не убеждает то, что язык используется для объяснения(!) положений стандартов, то есть этот язык фактически признан аксиоматическим, других аргументов у меня не будет.
Русский язык тоже можно использовать почти как псевдокод для объясенния(!) полжоений стандартов, но это не делает его доказанным.
Очень жаль, что вы выбрали напрочь проигнорировать основной вопрос моего комментария, и так как он составлял 69% моего текста по объёму, то вы точно сделали это осознанно.
вы наверно не поверите, но я в плюсах писал целые функции на ассемблере, плюсы позволяют писать на Ассемблере, поэтому я знаю о чем говорю
«В плюсах можно делать ассемблерные вставки ⇒ сравнение с кодом на плюсах можно подменять на сравнение с ассемблером, в который компилируется код на плюсах или хаскеле». Топовая логика, ничего не скажешь.
Кстати, на хаскеле тоже можно делать ассемблерные вставки и писать на ассемблере целые функции.
Библиотеку с этими функциями потом (после 3 месяцев тестирования) купила одна оченьизвестная контора, возможно они до сих пор где то работают.
Серьёзное достижение для профессионального программиста.
Ваши попытки придать вес вашим словам через подобные никак не связанные с темой обсуждения отсылки вместе с вашей постоянной апелляцией к «а вы авторитет? а вы пытаетесь выдать себя за авторитет? а почему вы так написали, как будто, если очень напрячься, можно подумать, что вы выдаёте себя за авторитета?» складываются в забавную картину.
А, ну для этого любого онлайн-репла достаточно. Я за вас погуглил «haskell online repl» и нашёл второй ссылкой https://tryhaskell.org/, чтобы типы заодно выводились.
Но лучше, конечно, поставить что-нибудь локально, например, через ghcup.
Может дело не в языке, а в том кто его использует? У кого-то лучше получается на плюсах, у кого то на хаскеле, на Джаве, на Тайп-скрипте, ... ?
Мой опыт споров в интернете показывает, что с подобными утверждениями спорить совершенно бессмысленно. На любой мой тезис в духе «на плюсах я профессионально пишу 20 лет, и там и сейчас получается всё хуже, чем получалось на хаскеле с 3-5 годами опыта, и у всех моих плюсатых коллег тоже всё хуже, чем у пишущих на хаскеле, и наблюдаемое мной распределение качества кода сильно не в пользу плюсов» мой собеседник всегда может ответить «skill issue, git gud вы все просто ниасилили» (что даже если arguendo так, то естественный вывод о сравнительном качестве языков от собеседника всё равно почему-то ускользает).
Мне интереснее другое (мне вообще интереснее, как у людей мозги работают, чем конкретные результаты работы этих мозгов — метауровень всегда веселее). Рассматриваете ли вы возможность, что питон/хаскель/жс в практике вас и вашего ближайшего социума медленнее плюсов не потому, что языки объективно тормознутые, а потому, что, ну, дело в том, «кто их использует»?
Собсна, сама дискуссия рядом (где вы ассемблер приплели и на которую сослались в следующем абзаце) показывает, что нет, всерьёз вы такую возможность не рассматриваете. Поэтому мой настоящий вопрос: почему? В чём для вас разница?
вы считаете мои (только мои? или те с которыми невозможно спорить?) аргументы аргументами соломенного пугала :)
Это общепринятый термин для метода спора ведения дискуссии, когда вместо ответа на аргументы собеседника («хаскель оказался быстрее плюсов») вы строите удобный вам аргумент («хаскель оказался быстрее ассемблера, в который он скомпилировался»), вкладываете его в уста собеседника, и потом спорите/высмеиваете/етц именно его, и потому, что выдуманный вами аргумент проще оспорить, или он смешнее, или что-то такое, хотя никакого отношения к исходному он не имеет.
Как ни странно, я считаю только такие подмены аргументов strawman'ами.
Но интересно было бы посмотреть как там компилятор выводит типы функций, я ни разу не видел.
Если вам прямо именно вывод типов, то, в зависимости от теоретической подготовки и желания инвестировать время — возьмите любую вводную статью из гугла по Hindley Milner type inference, либо откройте википедию по этой же теме, либо почитайте какую-нибудь современную обзорную статью по bidirectional typing, например.
Под типом функции имеется в виду то, что написано (или что выводит компилятор) после :: в её объявлении, не более. Типы «контекстов» там тоже указываются.
Потому что мне подобные копирования кажутся пассивной агрессией, а я предпочитаю активную.
Я вижу здесь утверждение близкое к тому что на плюсах функция может делать не понятно что, а в хаскеле функции делают исключительно то что нужно.
Нет, не «исключительно» что нужно. Но у вас сильно больше средств их ограничить.
Абсолютная строгость — это, опять же, в идрис или в агду. Хаскелю есть куда расти, и на их фоне его система типов — это дно и набор костылей, конечно.
И отсюда я делаю вывод что вы считаете что на хаскеле функции сами собой получаются ЛУЧШЕ чем на плюсах.
«Лучше» — это ещё не «совершенство». Но да, как-то так выходит, что функции действительно получаются «лучше». Язык стимулирует их разбивать на чистую и нечистую части, DI проще делать (в конце концов, DI — это просто монада), и так далее.
Кстати ваше заявление в виде "то я знаю" тоже тянет на претензию в превосходстве! Вы объявили себя авторитетом которому НУЖНО верить на слово. Вроде как если уж ВЫ об этом знаете, это не подлежит сомнению.
Извините, я постоянно забываю, что у некоторых людей есть максимально прокачанный скилл «додолбаться до любой запятой, напрочь игнорируя цели дискуссии и сводя её осмысленность в ноль», и поэтому иногда выбираю формулировки из предположения, что люди этим заниматься не будут.
Вы правда считаете, что «я» в упомянутой вами фразе — это конкретный я-который-IUIUIUIUIUIU, а не я-который-любой-чувак-который-в-данный-момент-читает-код? И вы продолжаете так считать даже после соседней дискуссии, где мы с другим человеком обсуждали, почему любой читающий этот код человек узнает то же самое?
то есть все функции в стиле ФП это просто совершенство по вашему?
Нет. Можете, пожалуйста, ради удовлетворения моего любопытства рассказать, как вы сделали такой вывод из моих слов?
Или что вы хотите сказать этим вашим "нельзя написать", что это гарантирует?
Про это написан следующий после процитированной вами фразы абзац. Я, в принципе, могу его скопировать сюда ещё раз, но будет конструктивнее, если вы скажете, что вам в нём непонятно или с чем вы несогласны, чтобы я мог раскрыть тему.
Вы не путаете тип функции и тип результата, который возвращает функция?
Нет, не путаю. Тип результата — это составляющая типа функции. Когда я смотрю на тип функции, то я в том числе смотрю на тип её результата (который, к слову, может зависеть от типов или даже значений её параметров).
Почти. foo всё ещё не живёт в IO, поэтому вы не можете так писать (ну и bar скобки не нужны). Вы можете написать
main = do
someInt ← bar
let fooResult = foo someInt
-- нужен ещё какой-то IO-экшн,
-- иначе толку с foo нет,
-- и её вызов вырежется компилятором
print fooResult
Но тут снова foo ничего не делает, не читает с диска, не отправляет на сервер, и так далее. Все возможные эффекты спрятаны в bar, которая ровно поэтому и помечена как возвращающая IO что-то
в описании функции должно присутствовать IO?
Функция должна иметь тип формы ... → IO SomeType
В описании функции meh :: IO Int → String формально присутствует IO, но она ничего никуда не отправляет (и, опять же, физически математически не может использовать свой аргумент).
С другой стороны, её интерфейс такой же как у State и смысл тот же - контекст с get и put методами.
ИМХО это так не стоит говорить, потому что ИМХО логично определять интерфейс как семантику операций, а она у ST и State разная (даже если беглое определение неформальным языком использует похожие слова).
Да, это я понял, чтобы в функции делать IO оно должно быть явно прописано в объявлении. Не смог понять как это правильно записать
Потому что на самом деле функция не «делает IO». Функция возвращает описание IO-действия, которое при своей интерпретации рантайм-системой хаскеля вернёт значение такого-то типа (или закончится экзепшоном, но не будем вскрывать эту тему). На практике «возвращает IO-действие с результатом типа Int» иногда сокращают до «делает IO и возвращает Int», но это абьюз терминологии, который, видимо, в данном случае путает.
Поэтому для того, что вы имеете в виду, нужно, чтобы у bar был тип SomeInput → IO Int, и поэтому это:
В общем, напишем bar так, чтобы она выполняла IO и возвращала Int, насколько я понял это вполне возможно
на самом деле невозможно. bar будет возвращать IO Int.
Но для того, чтобы выполнить это IO, которое вернула bar, нужно, чтобы выполняющий код тоже жил в IO(другой, более любимый лично мной вариант абьюза терминологии — «функция живёт в монаде M» означает, что она возвращает что-то, завёрнуте в M). foo в IO не живёт и поэтому выполнить то IO-действие, описание которого ей передала bar, не может. Он может его только проигнорировать.
Скрытый текст
Технически никто никогда не выполняет IO, кроме рантайм-системы хаскеля, которая просто берёт ваш main и его интерпретирует. Принимающие IO и возвращающие IO функции, вроде гипотетической twice :: IO a → IO (a, a) с понятной по имени и типу семантикой, правильнее считать берущими одно описание набора действий с IO-эффектами и возвращающими какое-то новое описание на базе того, что они приняли, но это не так важно для дискуссии.
синтаксис вида baz :: Int -> Int -> Int -> Int это прям отдельное спасибо создателям, такой вывих мозга и пальцев надо ещё умудрится придумать.
С каррированием и частичным применением хорошо работает, а так как семантики «сделали IO, вернули просто Int» нет, то, думаю, ваше возражение к синтаксису снимется.
Нет. Нужно, чтобы barвозвращалаIO-действие, а не принимала его.
Более того, от одного взгляда на тип bar понятно, что своим аргументом она пользоваться не может (кроме как через unsafePerformIO и подобные, но safe haskell это проверяет и запрещает). Значит, bar эквивалентна простому значению Int.
Забавно, что вы даже не видели код, но уже вполне готовы его обсуждать.
Подобные вещи пишутся примерно так же быстро, как на императивных языках. И читаются они тоже примерно так же быстро. Тут каких-то хитрых вещей с доказательствами и не возникает, потому что речь, в конце концов, только о реализации, а не о доказательстве её корректности.
Нет, не знаете! Вы знаете о том, что она не возвращает во внешний мир результатов об этом.
Какая операционная или денотационная разница?
Можно пропатчить бинарный код (или компилятор) так, что это утверждение станет не верным.
Почему во всех обсуждениях гарантий и профитов от типизации возникают какие-то очень странные контраргументы, которых, более того, не возникает при обсуждении гарантий и профитов от любых других подходов, вроде TDD или ООП?
Во всех этих разговорах подразумевается, что никто не патчит компилятор или бинарь, чтобы сделать вашу жизнь хуже. Никто не ломает намеренно библиотеку для тестирования, чтобы она вместо failure выводила success, если хостнейм машины равен "Arlekcangr's work PC". Никто не подменяет работающий бинарь в продакшене на версию, написанную соседней командой, которая вроде должна делать то же, но не делает. Никто не делает #define int std::vector<std::string> перед объявлением функции.
Вы часто видели, чтобы в тредах об ООП на «инкапсуляция помогает скрывать данные и реализацию» кто-то всерьёз отвечал «нет! компилятор можно пропатчить, чтобы он игнорировал private! можно сделать #define private public!», и это воспринималось в условиях дискуссии как валидное возражение?
Кроме того, если внутри этой функции используется бинарная библиотека, о которой вы ничего не знаете (не важно каким инструментом она собрана - пропатченым компилятором хаскеля или вообще компилятором си, но в хаскель импортирована как "чистая")
Компилятор эти свойства проверяет транзитивно. И в safe haskell вы не можете импортировать нечистые библиотеки как чистые.
Если же весь код открыт, то и в случае ооп можно сказать отправляет она что-то или нет.
Только прямой и ручной инспекцией всего кода, а не компилятором.
не менее не допускающих полной верификации кода без дополнительного его аннотирования пред-условиями (можно считать, что и сигнатура этой функции тоже есть аннотация предусловия, что объявленная с такой сигнатурой функция, не имеет побочных эффектов. Но кроме этого никаких других способов это установить не существует)
Так и в обсуждаемом случае полной верификации нет. Просто отсутствие IO.
Можно философски думать об IO как о State, где состояние хранится во внешнем мире, - но это не совсем справедливо. Во-первых, State можно безболезненно копировать, а мир - нельзя. Во-вторых, State неизменно, если его не менять, а мир меняется сам по себе.
Потому что ваш исходный собеседник опечатался, и вместо State имел в виду ST, который копировать тоже нельзя.
Если почитать мой комментарий, то можно заметить, что человека (особенно в среднем) я и не приводил как такой пример.
Более того, лично я считаю, что ЛЛМ — это не «смотрите, оно уже почти как люди, общий искусственный интеллект будет уже завтра», а скорее «смотрите, люди в среднем на самом деле почти как предсказатель токенов, естественная глупость уже вчера».
Мои наблюдения говорят, что чем больше человек считает, что его верования — самые верные верования (не называя их верованиями, конечно), тогда как большинство по тем же вопросам верят во всякую чушь, тем больше он сам верит во всякую чушь.
ЛЛМ не умеют размышлять (что бы это ни значило), но умеют, упрощая, рекурсивно генерировать следующий токен согласно некоторому распределению из обучающей выборки. Поэтому если в обучающей выборке было достаточно текстов с разговорами
то ЛЛМ будет выдавать вполне себе неотличимые локально от людей результаты.
А текстов было достаточно. В интернете этого много, а люди сильно более похожи друг на друга, чем может показаться.
И, кстати, чем хуже оно формализуется, тем более неотличима ЛЛМ от человека (в человеколюбиво-оптимистичном случае; в мизантропо-циничном — тем ближе ЛЛМ к максимуму по людям). На вопросах по теоркату даже топовые модели сливаются очень быстро, генерируя легко проверяемый бред уровня эквивалентности уравнений a + b = c и a = b + c. А вот на вопросах о «порекомендуй книжку почитать, если мне понравилась эта вот поэтому, а вот та не понравилась потому», или «проинтерпретируй текст этой песни», или вообще полный буллшит уровня «основываясь на истории общения и статистике по другим людям и вообще по научным данным, дай прогноз моей жизни на следующие 12 месяцев», оно показывает себя глубже и шире подавляющего большинства людей, с кем я общался.
Плюс, у меня есть впечатление, что вы сравниваете среднее по ЛЛМкам с околомаксимумом по людям. А найти хорошего человека-советчика на все эти вот темы — это, вообще говоря, известная проблема.
А потом заголовки
В загрузчике GRUB2 выявлена 21 уязвимость
В библиотеке Libxml2, разрабатываемой проектом GNOME и применяемой для разбора содержимого в формате XML, выявлено 5 уязвимостей, две из которых потенциально могут привести к выполнению кода при обработке специально оформленных внешних данных.
Ник Велнхофер (Nick Wellnhofer), сопровождающий библиотеку libxml2, объявил, что отныне будет трактовать уязвимости как обычные ошибки. Сообщения об уязвимостях не будут рассматриваться в приоритетном порядке, а станут исправляться по мере появления свободного времени.
Уязвимости в пакетах с Kea DHCP и cyrus-imapd, позволяющие повысить привилегии в системе
Уязвимость в KDE Konsole, позволяющая выполнить код при открытии страницы в браузере
Уязвимости в PAM и libblockdev, позволяющие получить права root в системе
Уязвимость в GNU screen, позволяющая выполнить код с правами root
Дальше мне надоело копипастить заголовки из моего фида opennet, фильтрованного по «уязви». Их там дофига (NB размер скроллбара справа):
Я боюсь, что вы не понимаете, что такое доказательство.
Русский язык тоже можно использовать почти как псевдокод для объясенния(!) полжоений стандартов, но это не делает его доказанным.
Очень жаль, что вы выбрали напрочь проигнорировать основной вопрос моего комментария, и так как он составлял 69% моего текста по объёму, то вы точно сделали это осознанно.
«В плюсах можно делать ассемблерные вставки ⇒ сравнение с кодом на плюсах можно подменять на сравнение с ассемблером, в который компилируется код на плюсах или хаскеле». Топовая логика, ничего не скажешь.
Кстати, на хаскеле тоже можно делать ассемблерные вставки и писать на ассемблере целые функции.
Серьёзное достижение для профессионального программиста.
Ваши попытки придать вес вашим словам через подобные никак не связанные с темой обсуждения отсылки вместе с вашей постоянной апелляцией к «а вы авторитет? а вы пытаетесь выдать себя за авторитет? а почему вы так написали, как будто, если очень напрячься, можно подумать, что вы выдаёте себя за авторитета?» складываются в забавную картину.
А, ну для этого любого онлайн-репла достаточно. Я за вас погуглил «haskell online repl» и нашёл второй ссылкой https://tryhaskell.org/, чтобы типы заодно выводились.
Но лучше, конечно, поставить что-нибудь локально, например, через ghcup.
Лол.
Мой опыт споров в интернете показывает, что с подобными утверждениями спорить совершенно бессмысленно. На любой мой тезис в духе «на плюсах я профессионально пишу 20 лет, и там и сейчас получается всё хуже, чем получалось на хаскеле с 3-5 годами опыта, и у всех моих плюсатых коллег тоже всё хуже, чем у пишущих на хаскеле, и наблюдаемое мной распределение качества кода сильно не в пользу плюсов» мой собеседник всегда может ответить «
skill issue, git gudвы все просто ниасилили» (что даже если arguendo так, то естественный вывод о сравнительном качестве языков от собеседника всё равно почему-то ускользает).Мне интереснее другое (мне вообще интереснее, как у людей мозги работают, чем конкретные результаты работы этих мозгов — метауровень всегда веселее). Рассматриваете ли вы возможность, что питон/хаскель/жс в практике вас и вашего ближайшего социума медленнее плюсов не потому, что языки объективно тормознутые, а потому, что, ну, дело в том, «кто их использует»?
Собсна, сама дискуссия рядом (где вы ассемблер приплели и на которую сослались в следующем абзаце) показывает, что нет, всерьёз вы такую возможность не рассматриваете. Поэтому мой настоящий вопрос: почему? В чём для вас разница?
Это общепринятый термин для метода
спораведения дискуссии, когда вместо ответа на аргументы собеседника («хаскель оказался быстрее плюсов») вы строите удобный вам аргумент («хаскель оказался быстрее ассемблера, в который он скомпилировался»), вкладываете его в уста собеседника, и потом спорите/высмеиваете/етц именно его, и потому, что выдуманный вами аргумент проще оспорить, или он смешнее, или что-то такое, хотя никакого отношения к исходному он не имеет.Как ни странно, я считаю только такие подмены аргументов strawman'ами.
Более того, не все пределы должны сходиться, и не для всех пределов их сходимость важна на практике.
Если вам прямо именно вывод типов, то, в зависимости от теоретической подготовки и желания инвестировать время — возьмите любую вводную статью из гугла по Hindley Milner type inference, либо откройте википедию по этой же теме, либо почитайте какую-нибудь современную обзорную статью по bidirectional typing, например.
Под типом функции имеется в виду то, что написано (или что выводит компилятор) после
::в её объявлении, не более. Типы «контекстов» там тоже указываются.Потому что мне подобные копирования кажутся пассивной агрессией, а я предпочитаю активную.
Нет, не «исключительно» что нужно. Но у вас сильно больше средств их ограничить.
Абсолютная строгость — это, опять же, в идрис или в агду. Хаскелю есть куда расти, и на их фоне его система типов — это дно и набор костылей, конечно.
«Лучше» — это ещё не «совершенство». Но да, как-то так выходит, что функции действительно получаются «лучше». Язык стимулирует их разбивать на чистую и нечистую части, DI проще делать (в конце концов, DI — это просто монада), и так далее.
Извините, я постоянно забываю, что у некоторых людей есть максимально прокачанный скилл «додолбаться до любой запятой, напрочь игнорируя цели дискуссии и сводя её осмысленность в ноль», и поэтому иногда выбираю формулировки из предположения, что люди этим заниматься не будут.
Вы правда считаете, что «я» в упомянутой вами фразе — это конкретный я-который-IUIUIUIUIUIU, а не я-который-любой-чувак-который-в-данный-момент-читает-код? И вы продолжаете так считать даже после соседней дискуссии, где мы с другим человеком обсуждали, почему любой читающий этот код человек узнает то же самое?
Нет. Можете, пожалуйста, ради удовлетворения моего любопытства рассказать, как вы сделали такой вывод из моих слов?
Про это написан следующий после процитированной вами фразы абзац. Я, в принципе, могу его скопировать сюда ещё раз, но будет конструктивнее, если вы скажете, что вам в нём непонятно или с чем вы несогласны, чтобы я мог раскрыть тему.
Нет, не путаю. Тип результата — это составляющая типа функции. Когда я смотрю на тип функции, то я в том числе смотрю на тип её результата (который, к слову, может зависеть от типов или даже значений её параметров).
Если вы продолжите развивать эту мысль, то в итоге придёте к системе типов хаскеля с плюсовым синтаксисом, да.
Почти.
fooвсё ещё не живёт вIO, поэтому вы не можете так писать (ну иbarскобки не нужны). Вы можете написатьНо тут снова
fooничего не делает, не читает с диска, не отправляет на сервер, и так далее. Все возможные эффекты спрятаны вbar, которая ровно поэтому и помечена как возвращающаяIO что-тоФункция должна иметь тип формы
... → IO SomeTypeВ описании функции
meh :: IO Int → Stringформально присутствуетIO, но она ничего никуда не отправляет (и, опять же,физическиматематически не может использовать свой аргумент).ИМХО это так не стоит говорить, потому что ИМХО логично определять интерфейс как семантику операций, а она у
STиStateразная (даже если беглое определение неформальным языком использует похожие слова).Потому что на самом деле функция не «делает IO». Функция возвращает описание
IO-действия, которое при своей интерпретации рантайм-системой хаскеля вернёт значение такого-то типа (или закончится экзепшоном, но не будем вскрывать эту тему). На практике «возвращаетIO-действие с результатом типаInt» иногда сокращают до «делаетIOи возвращаетInt», но это абьюз терминологии, который, видимо, в данном случае путает.Поэтому для того, что вы имеете в виду, нужно, чтобы у
barбыл типSomeInput → IO Int, и поэтому это:на самом деле невозможно.
barбудет возвращатьIO Int.Но для того, чтобы выполнить это
IO, которое вернулаbar, нужно, чтобы выполняющий код тоже жил вIO(другой, более любимый лично мной вариант абьюза терминологии — «функция живёт в монадеM» означает, что она возвращает что-то, завёрнуте вM).fooвIOне живёт и поэтому выполнить тоIO-действие, описание которого ей передалаbar, не может. Он может его только проигнорировать.Скрытый текст
Технически никто никогда не выполняет
IO, кроме рантайм-системы хаскеля, которая просто берёт вашmainи его интерпретирует. ПринимающиеIOи возвращающиеIOфункции, вроде гипотетическойtwice :: IO a → IO (a, a)с понятной по имени и типу семантикой, правильнее считать берущими одно описание набора действий сIO-эффектами и возвращающими какое-то новое описание на базе того, что они приняли, но это не так важно для дискуссии.С каррированием и частичным применением хорошо работает, а так как семантики «сделали
IO, вернули простоInt» нет, то, думаю, ваше возражение к синтаксису снимется.Нет. Нужно, чтобы
barвозвращалаIO-действие, а не принимала его.Более того, от одного взгляда на тип
barпонятно, что своим аргументом она пользоваться не может (кроме как черезunsafePerformIOи подобные, но safe haskell это проверяет и запрещает). Значит,barэквивалентна простому значениюInt.Забавно, что вы даже не видели код, но уже вполне готовы его обсуждать.
Подобные вещи пишутся примерно так же быстро, как на императивных языках. И читаются они тоже примерно так же быстро. Тут каких-то хитрых вещей с доказательствами и не возникает, потому что речь, в конце концов, только о реализации, а не о доказательстве её корректности.
Вам стоит номинироваться на медаль «самый краткий strawman argument».
В тех статьях описывались фантазии? Или что вы пытаетесь сказать?
Какая операционная или денотационная разница?
Почему во всех обсуждениях гарантий и профитов от типизации возникают какие-то очень странные контраргументы, которых, более того, не возникает при обсуждении гарантий и профитов от любых других подходов, вроде TDD или ООП?
Во всех этих разговорах подразумевается, что никто не патчит компилятор или бинарь, чтобы сделать вашу жизнь хуже. Никто не ломает намеренно библиотеку для тестирования, чтобы она вместо
failureвыводилаsuccess, если хостнейм машины равен "Arlekcangr's work PC". Никто не подменяет работающий бинарь в продакшене на версию, написанную соседней командой, которая вроде должна делать то же, но не делает. Никто не делает#define int std::vector<std::string>перед объявлением функции.Вы часто видели, чтобы в тредах об ООП на «инкапсуляция помогает скрывать данные и реализацию» кто-то всерьёз отвечал «нет! компилятор можно пропатчить, чтобы он игнорировал
private! можно сделать#define private public!», и это воспринималось в условиях дискуссии как валидное возражение?Компилятор эти свойства проверяет транзитивно. И в safe haskell вы не можете импортировать нечистые библиотеки как чистые.
Только прямой и ручной инспекцией всего кода, а не компилятором.
Так и в обсуждаемом случае полной верификации нет. Просто отсутствие IO.
Потому что ваш исходный собеседник опечатался, и вместо
Stateимел в видуST, который копировать тоже нельзя.