Но интересно было бы посмотреть как там компилятор выводит типы функций, я ни разу не видел.
Если вам прямо именно вывод типов, то, в зависимости от теоретической подготовки и желания инвестировать время — возьмите любую вводную статью из гугла по 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, который копировать тоже нельзя.
К сожалению, вы опоздали. Диагональный функтор Δ = x ↦ (x, x) : 𝒞 → 𝒞 × 𝒞 на самом деле роляет в программировании и вылезает что в языках с субструктурными системами типов (раст и боров чекер или linear haskell, где он соответствует процедуре удваивания ресурсов), что в семантике обычных языков (копирование данных), что в формализациях некоторых конструкций вроде параллельных вычислений.
А чем создание матрицы состояний не является функциональным подходом? На хабре в своё время была статья про расстояние Левенштейна на хаскеле, и там достаточно оптимальный код на плюсах работал, скажем, секунду, а достаточно идиоматичный код на хаскеле — 1.3 секунды. У вас (императивный же) питон или js будут работать в разы, если не на порядки дольше.
Более того, неидиоматичный, но всё ещё функциональный (мутабельность локальная и проверяемая компилятором) код там оказывался быстрее плюсов.
Справедливости ради, типизация везде дает эффект лучшей предсказуемости. Но не настолько крутой, чтобы вообще не писать тесты. Кстати, как выглядят тесты на Haskell, они вообще бывают нужны?
Да, особенно если речь о взаимодействии с внешним миром и/или об интеграционных тестах.
Для внутренней, чистой логики их нужно сильно меньше, потому что много чего ловится типами. Хаскель же по большому счёту популяризовал property-based testing, и, например, либа quickcheck — про них. Вы пишете выражение вроде \list → reverse (reverse list) === list, а либа сама генерирует примеры, проверяет выражение, и в случае нахождения контрпримера пытается его уменьшить. Где-то рядом model-based-тесты, где у вас есть медленная, но легко понимаемая и проверяемая модель вашей логики, и есть оптимизированная, но тяжёло проверяемая. Вы аналогично пишете prop-тесты, что их результаты совпадают.
Чтобы тесты (особенно property-based) на внутреннюю логику не писать и довериться тайпчекеру на все 100%, нужны ещё более сильные системы типов, вроде идриса или агды.
ИМХО хорошим ресурсом на тему будет книжка Сэнди Магвайра «Algebra-driven design». Там мало формальной теории (и её можно скипать), но идеи она передаёт выразимые и в более мейнстримных языках.
Понимание теорката для ФП нужно настолько же, насколько понимание теории вокруг машины Тьюринга, умение доказать существование универсальной МТ и неразрешимость, и всё такое, нужны для вашего среднего императивного программирования.
ИМХО интро-статья про ФП, говорящая про теоркат, делает услугу только своему автору, который осилил узнать прочитать на википедии про функторы и теперь обязан их ввернуть, потому что это якобы показывает его понимание теорката. Хотя функтор — это примерно второй раздел первой главы в любом, даже самом простом учебнике теорката, сразу после определения категории, а до третьего раздела первой главы, с естественными преобразованиями (без которых, кстати, монаду определить невозможно), автор дочитать уже не смог. Всем остальным в целевой аудитории таких статей упоминание теорката только вредит.
Никто же не объясняет каррирование через декартово замкнутые категории, power objects, экспоненциирование и сопряжение функторов B × — и (—)^B? Не объясняет, конечно. Так и с функторами и монадами это всё не нужно.
Функторы и монады — это не штука из теорката. Функторы и монады — это просто такие интерфейсы вроде «ассоциативный контейнер». Функтор — это штука, которая умеет map с определёнными законами. Если ваш тип умеет map , удовлетворяющий этим законам, то он функтор. Если ваш тип умеет bimap с похожими законами, то он бифунктор (как пара из двух элементов, например). Из бифунктора и подходящего объекта можно сделать функтор. Из двух функторов можно сделать бифунктор. Всякое такое вот.
А если серьёзно, ну давайте лучше с процедурным программированием сравним и ответим честно на 2 вопроса: что нельзя написать процедурно?
Любой алгоритм можно написать процедурно. И λ-исчисление, и машина Тьюринга, собсна, Тьюринг-полны.
В чём отличие, кроме "красоты"?
Отличие в том, какую информацию о функции даёт её тип, и, соответственно, что нельзя написать (а я утверждаю, что современное ФП — это не про «передачу функции в функции», что умеют почти все языки, а про выражение семантики в типах).
Если у меня в хаскеле написано foo :: Int → String, то я знаю (при некоторых дополнительных не важных для принципа вводных), что эта функция не общается с внешним миром, не отправляет запрос к БД, не читает и не пишет в глобальные переменные, и не отправляет мой ~/.bitcoin/wallet на сервер злоумышленника. Если у меня в плюсах написано std::string foo(int), то эта функция может делать всё что угодно.
Соответственно, рефакторить типизированный код куда проще и одно удовольствие. В моей практике хаскеля там действительно работает «if it compiles after refactoring, it works», в моей практике плюсов это не работает почти никогда.
Короче, отличие в том, что о коде проще рассуждать, и компилятор проверяет больше вещей.
Хотите красоты - делаете DSL, не пытаясь решать сразу все проблемы мира
Кстати, и eDSL, и DSL на хаскеле и подобных языках делать — одно удовольствие.
Я привел простые примеры используемые всеми практически.
Полупроводниковые транзисторы тоже используются практически всеми. Думаю, даже более всеми, чем AES и тензорфлоу вместе взятые.
Почему тот факт, что я отправляю этот комментарий через HTTPS, использующий некоторую математику средней продвинутости, означает нужность математики, а тот факт, что я пишу этот комментарий с компьютера, элементная база которого завязана на кванты, нужность квантов не означает?
Нюанс в чем ? В тех вакансиях что вижу я и рядом со мной почему то математика (хоть базовая) нужна в 95% случаев.
Базовая (уровня школы) — да. Высшая, с профильным дипломом, о котором вы писали изначально (и что потом заменили почему-то на базовую математику, кстати, что я ранее не заметил и упустил) — нет.
Зависит от части компилятора. Ну формально libm не компилятор, но рядом. А если какие нить плюсовые стандартные библиотеки ковырять современные, там есть математика и не совсем простая.
Там халява. Сосбна, где там (особенно если вычеркнуть libm, что вы неявно сделали) вообще какая-то нетривиальная математика вылезает, кромеусловных функций Бесселя, которые зачем-то запихнули в стандарт?
Я вообще в основном фронтенды делал. И там, например, вылезают вещи вроде таких: https://dl.acm.org/doi/pdf/10.1145/3371078 (но это ещё изич). Или таких: https://arxiv.org/pdf/2307.08759 . Или таких: https://bentnib.org/quantitative-type-theory.pdf . Или формальных доказательств корректности, с Agda, Coq и прочим. Или с модальной темпоральной логикой (правда, ей мы занимались очень мало, увы). О вещах вроде теории типов в общем (без неё вы вторую и третью статью просто не прочитаете, совсем) я и не говорю — это просто база. Ну и туда же мои любимые теоркат и матлог — мне, например, нужно их сильно больше, чем я понимаю сейчас, чтобы полностью понять третью и четвёртую секцию в статье по третьей ссылке выше.
Но при этом я понимаю, что среднему программисту это всё нафиг не нужно вообще, совсем, и не говорю, что это обязательно, и что нужны какие-то профильные дипломы (тем более, что это в вузах обычно не рассказывают).
Хм...
И поэтому таких вот вопросов у меня не возникает, да.
Если вам прямо именно вывод типов, то, в зависимости от теоретической подготовки и желания инвестировать время — возьмите любую вводную статью из гугла по 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, который копировать тоже нельзя.К сожалению, вы опоздали. Диагональный функтор Δ = x ↦ (x, x) : 𝒞 → 𝒞 × 𝒞 на самом деле роляет в программировании и вылезает что в языках с субструктурными системами типов (раст и боров чекер или linear haskell, где он соответствует процедуре удваивания ресурсов), что в семантике обычных языков (копирование данных), что в формализациях некоторых конструкций вроде параллельных вычислений.
Попробуйте программирование змейкой.
А чем создание матрицы состояний не является функциональным подходом? На хабре в своё время была статья про расстояние Левенштейна на хаскеле, и там достаточно оптимальный код на плюсах работал, скажем, секунду, а достаточно идиоматичный код на хаскеле — 1.3 секунды. У вас (императивный же) питон или js будут работать в разы, если не на порядки дольше.
Более того, неидиоматичный, но всё ещё функциональный (мутабельность локальная и проверяемая компилятором) код там оказывался быстрее плюсов.
Да, особенно если речь о взаимодействии с внешним миром и/или об интеграционных тестах.
Для внутренней, чистой логики их нужно сильно меньше, потому что много чего ловится типами. Хаскель же по большому счёту популяризовал property-based testing, и, например, либа quickcheck — про них. Вы пишете выражение вроде
\list → reverse (reverse list) === list, а либа сама генерирует примеры, проверяет выражение, и в случае нахождения контрпримера пытается его уменьшить. Где-то рядом model-based-тесты, где у вас есть медленная, но легко понимаемая и проверяемая модель вашей логики, и есть оптимизированная, но тяжёло проверяемая. Вы аналогично пишете prop-тесты, что их результаты совпадают.Чтобы тесты (особенно property-based) на внутреннюю логику не писать и довериться тайпчекеру на все 100%, нужны ещё более сильные системы типов, вроде идриса или агды.
ИМХО хорошим ресурсом на тему будет книжка Сэнди Магвайра «Algebra-driven design». Там мало формальной теории (и её можно скипать), но идеи она передаёт выразимые и в более мейнстримных языках.
Понимание теорката для ФП нужно настолько же, насколько понимание теории вокруг машины Тьюринга, умение доказать существование универсальной МТ и неразрешимость, и всё такое, нужны для вашего среднего императивного программирования.
ИМХО интро-статья про ФП, говорящая про теоркат, делает услугу только своему автору, который осилил
узнатьпрочитать на википедии про функторы и теперь обязан их ввернуть, потому что это якобы показывает его понимание теорката. Хотя функтор — это примерно второй раздел первой главы в любом, даже самом простом учебнике теорката, сразу после определения категории, а до третьего раздела первой главы, с естественными преобразованиями (без которых, кстати, монаду определить невозможно), автор дочитать уже не смог. Всем остальным в целевой аудитории таких статей упоминание теорката только вредит.Никто же не объясняет каррирование через декартово замкнутые категории, power objects, экспоненциирование и сопряжение функторов B × — и (—)^B? Не объясняет, конечно. Так и с функторами и монадами это всё не нужно.
Функторы и монады — это не штука из теорката. Функторы и монады — это просто такие интерфейсы вроде «ассоциативный контейнер». Функтор — это штука, которая умеет
mapс определёнными законами. Если ваш тип умеетmap, удовлетворяющий этим законам, то он функтор. Если ваш тип умеетbimapс похожими законами, то он бифунктор (как пара из двух элементов, например). Из бифунктора и подходящего объекта можно сделать функтор. Из двух функторов можно сделать бифунктор. Всякое такое вот.Любой алгоритм можно написать процедурно. И λ-исчисление, и машина Тьюринга, собсна, Тьюринг-полны.
Отличие в том, какую информацию о функции даёт её тип, и, соответственно, что нельзя написать (а я утверждаю, что современное ФП — это не про «передачу функции в функции», что умеют почти все языки, а про выражение семантики в типах).
Если у меня в хаскеле написано
foo :: Int → String, то я знаю (при некоторых дополнительных не важных для принципа вводных), что эта функция не общается с внешним миром, не отправляет запрос к БД, не читает и не пишет в глобальные переменные, и не отправляет мой~/.bitcoin/walletна сервер злоумышленника. Если у меня в плюсах написаноstd::string foo(int), то эта функция может делать всё что угодно.Соответственно, рефакторить типизированный код куда проще и одно удовольствие. В моей практике хаскеля там действительно работает «if it compiles after refactoring, it works», в моей практике плюсов это не работает почти никогда.
Короче, отличие в том, что о коде проще рассуждать, и компилятор проверяет больше вещей.
Кстати, и eDSL, и DSL на хаскеле и подобных языках делать — одно удовольствие.
Так хаскель не отрицает. Хаскель как раз за счёт системы типов проверяет, что всё нормально раскинуто либо в чистые, либо в
Полупроводниковые транзисторы тоже используются практически всеми. Думаю, даже более всеми, чем AES и тензорфлоу вместе взятые.
Почему тот факт, что я отправляю этот комментарий через HTTPS, использующий некоторую математику средней продвинутости, означает нужность математики, а тот факт, что я пишу этот комментарий с компьютера, элементная база которого завязана на кванты, нужность квантов не означает?
Базовая (уровня школы) — да. Высшая, с профильным дипломом, о котором вы писали изначально (и что потом заменили почему-то на базовую математику, кстати, что я ранее не заметил и упустил) — нет.
Там халява. Сосбна, где там (особенно если вычеркнуть libm, что вы неявно сделали) вообще какая-то нетривиальная математика вылезает, кроме условных функций Бесселя, которые зачем-то запихнули в стандарт?
Я вообще в основном фронтенды делал. И там, например, вылезают вещи вроде таких: https://dl.acm.org/doi/pdf/10.1145/3371078 (но это ещё изич). Или таких: https://arxiv.org/pdf/2307.08759 . Или таких: https://bentnib.org/quantitative-type-theory.pdf . Или формальных доказательств корректности, с Agda, Coq и прочим. Или с модальной темпоральной логикой (правда, ей мы занимались очень мало, увы). О вещах вроде теории типов в общем (без неё вы вторую и третью статью просто не прочитаете, совсем) я и не говорю — это просто база. Ну и туда же мои любимые теоркат и матлог — мне, например, нужно их сильно больше, чем я понимаю сейчас, чтобы полностью понять третью и четвёртую секцию в статье по третьей ссылке выше.
Но при этом я понимаю, что среднему программисту это всё нафиг не нужно вообще, совсем, и не говорю, что это обязательно, и что нужны какие-то профильные дипломы (тем более, что это в вузах обычно не рассказывают).
И поэтому таких вот вопросов у меня не возникает, да.