От Аристотеля до Тьюринга: что такое функциональное программирование и как оно облегчает жизнь

Ну да. Так что для Бейсика (как и для ассемблера) основная парадигма – императивная, а написание на нём какой-то функциональщины, да и вообще декларативщины, потребует вначале создать инфраструктуру для неё, да и вообще окажется неэффективным (функциональщина на языках, не поддерживающих автоматическое управление памятью – боль: невозможно даже толком замыкание создать, а как без этого вернуть из функции функцию?)

Тут требуется очень подробное объяснение (или авторитетная ссылка), т.к. меня учили что это принципиально разные парадигмы, хотя в каком-то смысле...

не знаю почему вас этому учили, если честно, и это удивительно. Меня учили, что Машина Тьюринга, Лямбда-исчисление Чёрча, Машина Поста и Нормальные Алгорифмы Маркова эквивалентны и тому имеются строгие математические доказательства. Доказательствам тоже учили, но за давностью лет я их не помню. В практическом же смысле, обычно, новые архитектуры или парадигмы сводят к тьюринг-полноте конструктивным способом, просто реализуя в этой парадигме машину Тьюринга. Реализаций машины Тьюринга, к примеру, на Лиспе - полно. В принципе, её несложно написать самому. Обратный переход ещё проще, поскольку много лисп-машин написано на каком-либо императивном/объектном/ещё-каком-то языке. Так что, да, они эквивалентны и строго математически и конструктивно.

Практичный пример того, про что вы написали - простого автоматического верифицирования. Именно практичный, полезный пример использования, хочу видеть насколько это круто.

по-прежнему, не вполне понимаю чего именно вы хотите? Практичный - это выгодный, удобный. Выгодный удобный пример, показывающий, что программа для которой математически доказано её соответствие спецификации лучше, чем программа для которой это не доказано? Или выгодный, удобный пример показывающий, что автоматическое доказательство лучше ручного? Это смотря чего вы хотите достичь. Я застал времена, когда мы писали программы без каких либо тестов и это считалось нормальным. В этом смысле тесты и, тем более, верификация были лишними и это было не круто. А теперь без тестов совсем не крута. А автоматические тесты, по сути - недоделанные, ущербные попытки частично реализовать доказательство правильности программы. Пишем мы их только потому, что не умеем (слишком сложно) верифицировать программы формально. Автоматическая верификация в этом смысле абсолютно практична - делает всё, что нужно сама. Куда уж практичнее (выгоднее/удобнее)? Написал программу, автоматически проверил её корректность - что может быть круче? Или вы что-то другое имели в виду?

Ну допустим, я написал пару десятков программ на NASM в лохматые годы. Это вообще никак не относится к идее, что ассемблер не единственный язык ТОЛЬКО потому, что код пишут человеки.

Это относится к пониманию почему это так. Если вы не поняли, значит ваши программы были по сложности уровня хелло ворда и их не надо было поддерживать. Либо конкретно вы - гений уровня Джона Кармака. Остальные люди существенно примитивнее и даже имеющий выразительнейший синтаксис, Пёрл считают write-only языком. И всилу ограниченности понапридумывали примитивных костылей в виде языков высокого уровня, чтобы хоть как-то умещать в голове решаемую проблему и её реализацию. Так-то языки высокого уровня компьютеру определённо не нужны.

Ровно таким же адекватным, если человек начнет заявлять что "я всегда уверен, что делает чужой код "

А если человек начнёт заявлять «ООП даёт гарантии инкапсуляции»? Можете дать прямой ответ хотя бы с третьей попытки?

Но отмахнуться от тезиса с чужими библиотеками вы не можете. И, видимо поэтому его игнорируете.

Я уже прямо ответил вам, что чужие библиотеки тоже проверяются компилятором, транзитивно.

Патченный компилятор можно подсунуть, конечно, но тогда вам придётся взломать всю цепочку, начиная от формирования релизов разработчиками ghc. Подобные возможности (равно как и закладки в процессоре, например) в подобных обсуждениях выносятся за скобки.

Для статической линковки это было бы полбеды. Но что делать с динамическим кодом ?

Единственный проект в моей практике, где нужна была динамическая линковка и прочие dll — один мой личный хобби-проект (причём один из нескольких десятков).

HFT — всё в статике, никаких dll.
Мировое финансово-новостное агенство — статика, никаких dll.
Блокчейн ­— статика, никаких dll.

Не, я знаю, что есть задачи, где динамическая линковка сильно облегчает жизнь. Но моя личная выборка показывает, что на них наткнуться маловероятно.

Прежде чем мне сюда писать, попробуйте ответить на вопрос, почему за 30+ лет подход хаскеля с IO монадой не получил распрастранения не только в классических императивных языках, но и в подавляющем большинстве тех, которые считаются функциональными.

Новые функциональные языки чистые. Идрис чистый. Агда чистая. Lean чистый.

Я об этом и говорю - мир в себе.

Ну да, тот же блокчейн — это ведь образец мира в себе, ага.

Вам не надо, другим может быть надо

Это совсем не то же самое утверждение, что «если внешняя библиотека должна жить в IO при safe-опциях сборки, то язык игрушечный».

Я сказал ровно то, что без анализа кода хоть на хаскеле, хоть на ооп, нельзя гарантировать как он работает.

И вы ошиблись.

(а может там unsafe внутри ? Есть в хаскеле unsafe ? А может там библиотека подключена как не IO, а она на самом деле IO...)

В safe haskell, на который я уже сослался дважды, не может быть никакого unsafe. Компилятор это тоже проверяет.

Но замечу, что если за столько лет никто не сделал лучше, то далеко не это основная проблема и ошибки в ПО в 99% случаев не про "у нас наша же функция делает какую-то неведомую фигню, а должна просто возвращать foo-bar-buzz". Иными словами IO монада решает мало значимую проблему.

Как-то так выходит, что как только язык начинает заставлять вас аккуратно описывать, что делает функция, то и качество кода подтягивается, и качество дизайна в целом, и ошибок становится меньше.

В моей практике большинство нетривиальных багов в императивных языках — из-за темпоральной связности между разными кусками кода. «Чтобы метод Foo::Bar() делал что нужно. надо обязательно сначала вызвать Foo::Baz(), а Foo::Quux() не вызывать». На хаскеле добиться такой костыльности почему-то сложнее.

Именно IO монада, т к другие монады вполне используются в не функциональных языках.

Покажете примеры монад ST, STM, и любого из многочисленных парсеров на комбинаторах? Особенно что они там вполне используются.

Хорошо, вы можете утверждать, что если у вас функция не возвращает IO то с 99% вероятностью она и не делает IO. Но анализ кода это не отменяет, т к один процент остается.

В safe haskell — со 100% вероятностью.

В прочем коде, если вы работаете не со злоумышленниками, достаточно того, что в коде начнёт торчать какое-нибудь unsafePerformIO, вы спросите, зачем оно нужно, и уберёте его.

Но субъективно я в этом сомневаюсь, по причине того, что такую "полезную" вещь уже давно бы внедрили повсеместно, как например анонимные функции или монаду MayBe.

Сделать maybe сильно проще, чем сделать IO (и чистые функции вообще), потому что maybe не требует изменений самой семантики языка.

Не может быть никакой 100% гарантии.

Это следствие какой-то математической теоремы? Или всё же того, что вы в очередной раз проигнорируете отсылки к инструментам, которые дают такие гарантии?

Да. Функции, которые не возвращают IO - чистые, то есть просто преобразовывают данные. Буквально определение чистоты - что вызов функции можно эквивалентно заменить сразу на возвращаемое значение.

Теперь вроде должно быть корректно.

Почти. 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, но она ничего никуда не отправляет (и, опять же, физически математически не может использовать свой аргумент).

Может дело не в языке, а в том кто его использует?

Конечно, другой вопрос, что это человеческий фактор.
foo DQ ? и long foo; по сути одно и то же, однако MOV [foo], 0.33 вполне допустимо, а foo = 0.33; уже нет.
"Лучше" ли использование long, чем DQ? Наверное, зависит от того, какие задачи нужно решать, но то, что это уменьшает человеческий фактор для целого ряда задач - факт.

Может дело не в языке, а в том кто его использует? У кого-то лучше получается на плюсах, у кого то на хаскеле, на Джаве, на Тайп-скрипте, ... ?

Мой опыт споров в интернете показывает, что с подобными утверждениями спорить совершенно бессмысленно. На любой мой тезис в духе «на плюсах я профессионально пишу 20 лет, и там и сейчас получается всё хуже, чем получалось на хаскеле с 3-5 годами опыта, и у всех моих плюсатых коллег тоже всё хуже, чем у пишущих на хаскеле, и наблюдаемое мной распределение качества кода сильно не в пользу плюсов» мой собеседник всегда может ответить «skill issue, git gud вы все просто ниасилили» (что даже если arguendo так, то естественный вывод о сравнительном качестве языков от собеседника всё равно почему-то ускользает).

Мне интереснее другое (мне вообще интереснее, как у людей мозги работают, чем конкретные результаты работы этих мозгов — метауровень всегда веселее). Рассматриваете ли вы возможность, что питон/хаскель/жс в практике вас и вашего ближайшего социума медленнее плюсов не потому, что языки объективно тормознутые, а потому, что, ну, дело в том, «кто их использует»?

Собсна, сама дискуссия рядом (где вы ассемблер приплели и на которую сослались в следующем абзаце) показывает, что нет, всерьёз вы такую возможность не рассматриваете. Поэтому мой настоящий вопрос: почему? В чём для вас разница?

вы считаете мои (только мои? или те с которыми невозможно спорить?) аргументы аргументами соломенного пугала :)

Это общепринятый термин для метода спора ведения дискуссии, когда вместо ответа на аргументы собеседника («хаскель оказался быстрее плюсов») вы строите удобный вам аргумент («хаскель оказался быстрее ассемблера, в который он скомпилировался»), вкладываете его в уста собеседника, и потом спорите/высмеиваете/етц именно его, и потому, что выдуманный вами аргумент проще оспорить, или он смешнее, или что-то такое, хотя никакого отношения к исходному он не имеет.

Как ни странно, я считаю только такие подмены аргументов strawman'ами.

Более того, не все пределы должны сходиться, и не для всех пределов их сходимость важна на практике.

И такой же "наивный", но на Си шарпе:

Не понял, а табличка с мемоизацией у вас где?

В хаскель-коде чрезмерное использование символов. К примеру, вот это V.! что за конструкция ? Как мне вообще это узнать ?

text1[len-1] — что за конструкция? Как мне вообще это узнать?

Чем хуже s2[j-1] ?

Тем, что встроенного оператора индексирования нет, а делать расширение языка для чего-то подобного никому неинтересно (хотя синтаксического сахара в ghc более чем достаточно, и его добавляют весьма охотно). Видимо, не является проблемой для людей в массе своей.

И я еще должен угадывать порядок вычисления, что s2 'BS.index' (j - 1) должно быть вычислено до ==

А когда вы в C# пишете foo == callFun(bar), вы ничего не угадываете, боженька знания свыше даёт?

Инверсная логика построения программы сверху вниз.

И я скучаю по этому в языках вроде агды, которые по ряду причин запрещают такую логику построения (или делают её очень сильно неудобной).

Потому что, в конце концов, это логично: в идеале вы сначала описываете, что должно происходить на самом высоком уровне, без деталей. Детали — они дальше и глубже по тексту.

Вы даже по-русски так говорите: «мы создаём массив, потом заполняем его так-то, потом пробегаем по нему функцией, которая, кстати, определяется сяк-то». Вы не говорите «о, вот определение функции, не спрашивайте зачем, а вот ещё одно. а вот мы создаём массив. а вот теперь мы вызываем первую функцию (вернись и перечитай с учётом контекста)».

Тексты, учебники, доказательства теорем, что угодно, выигрывают в читабельности, когда в каждый момент времени вы понимаете, нахрена вы читаете данную конкретную строчку. А так как дара предвиденья у вас нет, то это значит, что эта строчка была упомянута выше (и вы его либо разбираете подробно, либо скипаете, если она вам с учётом контекста выше сейчас неинтересна).

Конкретно в приведенном примере вложенные конструкции where.

А вы возьмите «Реализация с мутабельностью», например — там один вложенный where.

Не смотря на все эти не нужные знания, я не могу до конца понять и представить как этот код будет работать и в каком порядке пойдут вычисления. Я должен это именно разбирать, как при разборе математического доказательства.

Нет, не должны. Единственное, что вы должны знать — что приоритет у вызова функций («у пробела») больше, чем у операторов, поэтому этот код парсится как

(foldl' outer (V.generate (n + 1) id) [0 .. m - 1]) V.! n

То есть, сначала генерируем массив «0, 1, 2, 3, ..., n». Потом проходимся по всем 0, 1, 2, ... m - 1 с функцией-свёрткой outer, начальное значение аккумулятора которой — тот массив (который и выполняет роль мемоизирующей таблички). Потом достаём из результирующей строчки значение n.

Но очень удобно, конечно, написать код без мемоизации, а потом «ой, чё-т с мемоизацией выглядит слооожна».

Опять инверсная логика - то что стоит справа будет вычислено и передано в функцию слева. Очень напоминает мне польскую нотацию в языке Форт, который так и умер вместе с этой нотацией... Зачем ? Почему не использовать скобки ?

Вопрос стиля. Мне с $ удобнее, вы в данном случае можете использовать скобки.

И я склонен думать, что в том числе и по причине такого дизайна языка, который требует чтения математических доказательств каждый раз...

Моя неироничная гипотеза — потому, что хаскель требует делает хорошо сначала, а это довольно плохо работает с херак-херак-дривен девелопмент.