Зависимые типы, жидкие типы. Что лучше?

Потерялся в двух анонимах? )

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

const rule<class DeclVarID, parse_tree::DeclVar> declvar = "declvar";
const auto declvar_def = "var" >> id >> '=' >> expr;

vs

let declvar = str "var" >>. id .>> str "=" .>>. expr <!> "declvar" |>> ParseTree.DeclVar

Потерялся в двух анонимах? )

Похоже, да. Или не двух. Вы хоть нумеруйтесь, что ли…

зато они перегружены горизонтально и больше давят на моск.

пол парсера в одну строку?

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

Чтобы получить красивый текст прграммы.

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

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

пол парсера в одну строку?

Да в общем просто идиоматичный код в обоих случаях.

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

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

Только если они не любят математику. Потому что код на Haskell также красив, как геометрия на функциональных пространствах.

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

Не обязательно. Чтобы наслаждаться музыкой Баха не обязательно быть композитором.

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

Ха. Как раз недавно для прикола написал один и тот же транслятор дважды, на C++17/Boost и F#. Так вот нифига не очевидно, какой вышел проще.

Я вообще-то предлагал другие языки для написания трансляторов - как раз haskell и lisp. F# тоже по-идее здесь должен быть неплох.

У F# мусора поменьше, и строчек меньше, зато они перегружены горизонтально

Что значит перегружены горизонтально?

Это ты

это не я.

красивый текст прграммы.

на пистоне ещё красивше же, ну. и динамическая типизация же.

Это что за сцена ревности?

ты мне в последний раз заливал о том, что нельзя все failure обработать в одном месте, нужно failure01 failure02 и т.д. изобретать, в стат типизации, и что ракет могёт и дин и стат если надо. а теперь вдруг вопрос по хаскелю. неужели я тебя переубедил? ;)

Ну и где ваш хаскель

https://www.tiobe.com/tiobe-index/

Даже дельфя на 12 место скаканула.

Только если они не любят математику. Потому что код на Haskell также красив, как геометрия на функциональных пространствах.

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

Ну и где ваш хаскель
Даже дельфя на 12 место скаканула.

А где он должен быть, если даже такой достаточно популярный язык как руби на 13-м? Go - 14, Swift (на котором все яблофоны программируются на 14), Rust самый хайповый язык сегодняшнего дня на 29, а Lisp на 36 (популярней lua, kotlin, bash, typescript, elixir и vhdl) - что это вообще за критерий такой популярность на тиобе? Скажи еще, что на vhdl ничего не пишется - он ведь аж на 43-м месте!11 Какой ужос. О bash и typescript вообще молчу - «маргинальные недоязычки».

Я вообще-то предлагал другие языки для написания трансляторов - как раз haskell и lisp

Твой собеседник говорил про ML в целом. А на хаскеле будет лучше? Имхо, примерно то же самое.

На лиспе может и лучше. По крайней мере #lang brag из ракеты - идеален)

Что значит перегружены горизонтально?

Слишком длинные, слишком много смысла на строчку. Зависимые типы, жидкие типы. Что лучше? (комментарий)

занятно у тебя полыхнуло, маня

Это в твоей полыхающей вселенной vhdl вообще никому не нужен вместе с руби :)

Твой собеседник говорил про ML в целом. А на хаскеле будет лучше?

Не думаю, я в целом тоже про ML.

На лиспе может и лучше. По крайней мере #lang brag из ракеты - идеален)

На лиспе лучше в том смысле, что на нем можно написать нормальный рантайм помимо транслятора. У *ML из преимуществ (благодаря статике) это параметрический полиморфизм и статический паттерн матчинг. Ленивость еще хорошая штука, но я не уверен, что она организована в хаскеле как надо.

Во всем остальном Lisp лучше. А если нужна статика опять же - можно кое-где использовать typed racket, либо на CL сделать себе статику (искаробки нет).

на пистоне ещё красивше же, ну. и динамическая типизация же.

Ну как на питоне напишешь

    readFile templateFile
        >>= foldM (processLine processTemplate) context . lines
        >>= writeFile outFile . unlines . reverse . result

Так красиво не получится.

нельзя все failure обработать в одном месте, нужно failure01 failure02 и т.д. изобретать

Типизация ограниченная. failure я свожу просто к строкам.

getResult :: IO (Either String ())
getResult = runExceptT $ do ...

неужели я тебя переубедил

Нет. На Haskell я давно пишу утилитки по мелочи. Ему бы ещё переносимый GUI…

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

клоун, бегом показывать меня, где я писал про vhdl или руби.

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

С ленивостью и классами типов на Racket есть Hackett. Но это реально отдельный язык почти без интеграции с Racket. А тогда проще взять Haskell и получить более быстрый результат компиляции.

я понимаю, что вы там развели какого-то лоха на хаскель в вебе с помощью тех базвордов что ты пытаешься здесь втереть

А ты никак не можешь найти лоха, которого можно было бы развести на лисп, вот и бесишься?

Так красиво не получится.

а (на (ракете)) (красиво получается) ?

failure я свожу просто к строкам.

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

То что «даже дельфи» на каком-то там N-надцатом месте - о хаскеле ровным счетем ничего не говорит, так как ниже дельфи находятся другие популярные языки (в случае vhdl - для своих ниш). Если тебе на галере на хаскеле не дают прогать это никого не волнует, сходи поплачь в каком-то другом месте.

а (на (ракете)) (красиво получается) ?

Я же пишу: не настолько красиво как на хаскеле. Строчек в полтора раза больше, интерфейсы многословнее. Зато есть call/cc и контракты.

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

Если работает, то какая разница.

добавлен std::any в С++

Дык, ты же сам говорил, что это не может считаться динамической типизацией, если any_cast не будет автоматически выполняться. Да и если на то пошло, то void* в языке было изначально, так что std::any - это скорее ужесточение типизации.

Hack

Это ведь такая себе замена PHP, которая позволяет местами статическую типизацию использовать, разве нет? Kак и тайпскрипт я бы скорее записывал тут «победу статики».

Дык, ты же сам говорил, что это не может

Не может. Но подвижка в ту сторону. Также как тайпхинты в питоне - подвижка в сторону статической типизации.

Да и если на то пошло, то void* в языке было изначально

То не динамическая, то бестиповая. Внутри void* тип не хранится.

Строчек в полтора раза больше, интерфейсы многословнее.

кажется ты начал догадываться.

Зато есть call/cc

этим можно гордиться?

я понимаю, что вы там развели какого-то лоха на хаскель в вебе с помощью тех базвордов что ты пытаешься здесь втереть

А ты никак не можешь найти лоха, которого можно было бы развести на лисп, вот и бесишься?

В этом треде я надеялся услышать хоть какой-то конструктив от хаскель-фанбоев (хаскель как язык в некоторых нишах весьма выразительный - для написания «факториалов», например - т.е. программ, которые можно свести к одноразовому получению данных вписывающихся в заранее известный алгоритм, соответственно для микросервисной архитектуры, построенной на стабильном API и чистых функциях он тоже подходит). Для разбора грамматик, например, я думаю он тоже смотрелся бы нормально, при условии, если писать просто без ухода в дебри. Но в ответ мне начали рассказыть о якобы гарантиях того, что почему-то в вебе (!), где все данные прилетяют неясно откуда и в каком виде, именно хаскель будет гарантировать то, что деньги с моего счета не перейдут на счет хаскелиста. То есть очевидный тупак. А зачем мне кого-то разводить на лисп, если я сам могу выбирать на чем писать?

этим можно гордиться?

Ага.

https://www.schoolofhaskell.com/school/to-infinity-and-beyond/pick-of-the-week/the-mother-of-all-monads

https://pvk.ca/Blog/2013/09/19/all-you-need-is-call-slash-cc/

где все данные прилетяют неясно откуда

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

Не обязательно именно Haskell, но он тоже подходит.

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

А вот для этого как раз достаточно динамических языков типа лиспа и ребола.

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

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

А вот для этого как раз достаточно динамических языков типа лиспа и ребола.

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

В этом треде я надеялся услышать хоть какой-то конструктив от хаскель-фанбоев

Странно, что ты не понимаешь, что хаскель привлекает сторонников максимально строгой типизации. Есть языки строже, но работы на них ещё меньше. С позиции такого человека, вопрос звучит странно. Какие преимущества у хаскеля в вебе? Такие же, как и везде.

Я вон писал блокчейн на расте не столько потому, что мне блокчены интересны (хотя поначалу любопытно было), а потому что на расте.

о якобы гарантиях того, что почему-то в вебе (!), где все данные прилетяют неясно откуда

Почему ты так выделяешь веб? Вон в соседней теме «разработчики драйверов» рассказывают похожие сказки о том, что приходят «непредсказуемые данные». Они-то может и проходят, но вообще проверять входные данные идея всегда хорошая. И типизация даёт возможность понимать, что происходит, а не передавать туда-сюда словарь в котором непредсказуемым образом будут поля изменяться.

ты же понимаешь, что это чтиво из разряда зачем нам в С оператор цикла, если есть goto? call/cc на практике весьма сомнителен, универсальность удивительна разве что для любителей метапрога. на ski комбинаторах тоже можно наваять абсолютно всё, в том числе и твой call/cc. но ты серьёзно думаешь, что кто то будет так писать?

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

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

Вот есть

f :: DigitString -> SQL

g :: DigitString -> ....
g x y = ... f x ...

checkStringIsDigit :: String -> Maybe DigitString

И никак строку в f или g не передать, не проверив. А с контрактами появляется сильное желание поставить контракт только на вход g (ведь f больше ниоткуда не вызывается, зачем повторно проверку делать?). А потом через полгода кто-то делает вызов f, не проверив строку контрактом…

И даже с проверкой контрактом: в GLib всё проверяет контрактами и программы массово пишут в stderr что-то вроде: https://bugs.launchpad.net/ubuntu/+source/network-manager/+bug/1264364

А пользователи потом пишут программы, чтобы эти сообщения не видеть.

но ты серьёзно думаешь, что кто то будет так писать?

Так же как goto нужен, когда разработчик языка забыл реализовать какую-нибудь нужную конструкцию управления типа цикла n+1/2 раз или выхода из нескольких вложенных циклов, так и call/cc нужен, если разработчик языка забыл сделать генераторы, зелёные потоки, корутины или комбинаторы операций.

Причём Scheme даёт удобный способ любую нужную конструкцию с call/cc завернуть в макрос и использовать call/cc в пользовательском коде почти никогда не надо.

на ski комбинаторах тоже можно наваять абсолютно всё, в том числе и твой call/cc

???

Покажешь реализацию?

Странно, что ты не понимаешь, что хаскель привлекает сторонников максимально строгой типизации.

Динамическая типизация - тоже строгая. А с контрактами - еще даже более строгая, чем система типов хаскеля.

Есть языки строже, но работы на них ещё меньше.

Вопрос вообще не в строгости, а в том, _когда_ происходит проверка типов, и что собственно мы проверяем.

С позиции такого человека, вопрос звучит странно. Какие преимущества у хаскеля в вебе? Такие же, как и везде.

Ничего подобного, у С очевидные преимущества в написании драйверов перед лиспом, у кложи в разработки веба перед ... почти что перед всеми языками, питон простой язык-клей с кучей батареек, С++ для легаси или как С с классами, джава с шарпом для галер, пхп чтобы вордпрес, перл для написания однострочников, дельфи чтобы формочки клепать, 1с бухгалтерия, своя специализация у erlang, vhdl, prolog итд. В чем ниша хаскеля? Как оказалось веб? :)

Они-то может и проходят, но вообще проверять входные данные идея всегда хорошая.

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

И типизация даёт возможность понимать что происходит,

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

а не передавать туда-сюда словарь в котором непредсказуемым образом будут поля изменяться.

Ты этот словарь вначале получил без всяких гарантий - затем проверил контрактами (потому что проверять больше нечем) и когда отдаешь тоже контрактом проверяешь, раз тебе так важно. А вся статика - это только что между этими точками происходит. Т.е. про опечатки и сложение бульдогов с носорогами. Но прикол в том, что опечатки тебе подсветит ide или нормальный язык скажет, что извините в первый раз такое название вижу, вот вам варнинг держите. А енотобегемоты это ошибка _логическая_, чтобы ее сделать надо или вообще не понимать, что происходит в программе, или веществ объесться прям упороться или опечатка или зловред - то есть к вам в команду пробрался шпион от конкурентов и прописал True=False, решается системой контроля версий.

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

Есть множество валидных данных. Является ли то, что прилетело неясно откуда, элементом этого множества ты в любом случае проверяешь в рантайме. В языках со статической типизацией можно с определённой точностью описать это множество валидных данных. Тайпчекер проверит, действительно ли твоя функция-валидатор, которая будет выполняться в рантайме, возвращает элементы этого множества.

на ski комбинаторах тоже можно наваять абсолютно всё, в том числе и твой call/cc

Покажешь реализацию?

А мне call/cc на лямбда-исчислении, пожалуйста, оно читабельнее. А в SKI я сам потом скомпилю.

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

Ну так да, только невнимательность и все. А сколько трейдофов у статики? Впрочем, мне казалось мы тут +- схожего мнения по данному вопросу.

checkStringIsDigit :: String -> Maybe DigitString
И никак строку в f или g не передать, не проверив.

Нормальные контракты будут двигаться к тому, чтобы уметь выводить все что можно в статике, а все что нельзя - как обычно. Это и есть перспективное направление развития контрактов. Но если выбирать между _существующими_ системами типов, а не вымышленными, и существующими контрактами - то языки со статической типизацией проигрывают динамике как в выразительности, так и по итогу в гарантиях надежности, покрывая 2%-ный класс ошибок.

По существу примера - в динамике ты напишешь точно такую же ф-цию которая чекает строку на предмет состоит ли она из цифр. Один раз проверишь и дальше будешь ее передавать по цепочке преобразований, и в конце еще раз проверишь, что отдал не мусор. Статика рулит только, если у тебя все строки они уже известны на момент компиляции (то есть ты пишешь хеллоурлд), в реальном же мире 99% данных приходит из вне, как ты их будешь статически чекать на предмет корректности? _Все_ что ты можешь чекнуть в статике это только результат промежуточных преобразований и то далеко не всегда, а в основном только совпадение типов (чтобы *случайно* вместо бегемотов не подставить носорогов). Единственный реальный профит статики - это статический проход по ветвлению на тему не забыл ли ты какую-то ветку учесть / реализовать (и то возможности такой проверки ограничены). Да, это профит. 3%. И 97% боли.

И даже с проверкой контрактом: в GLib всё проверяет контрактами и программы массово пишут в stderr что-то вроде

Отлично, но почему им тут не помогла хваленая статика? Это неправильная, допустим, статика, плохая, но правильная где? :) Тред ведь об этом.

В чем ниша хаскеля? Как оказалось веб? :)

Если брать статистически, то всякие преобразователи данных. Pandoc, freearc, … У них код на хаскеле красивее получается.

Прикол в том, что они не проверяются на этапе компиляции, просто потому что на момент компиляции этих данных у нас нет.

Так статические типы вообще не про проверку данных. Они про проверку функций.

Ничего она не дает без нормальных зависимых типов (которых нет).

В общем случае даёт. Разве что вместо обычного if придётся пользоваться функциями типа

IsNotZero :: Int -> Maybe NotZero Int
IsNotZero 0 = Nothing
IsNotZero x = Just NotZero x

И нормальные зависимые типы прикручиваются через LiquidHaskell, если надо.

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

В Typed Racket тоже зависимые типы: https://docs.racket-lang.org/ts-reference/Experimental_Features.html

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

затем проверил контрактами (потому что проверять больше нечем) и когда отдаешь тоже контрактом проверяешь

Вот про то и речь. Что контрактами что-то проверяешь дважды, а что-то пропускаешь. В статической системе типов (хоть Haskell хоть Typed Racket) просто пропустить проверку не получится: программа не скомпилируется.

Или кто-то троллит или Вы общаетесь на разные темы.
Как узнать, что собеседник Вас понимает?
Как узнать, что собеседник понял Вашу конструкцию и её подоплёку?

Или Вам просто скучно?

Один раз проверишь и дальше будешь ее передавать по цепочке преобразований, и в конце еще раз проверишь, что отдал не мусор. Статика рулит только, если у тебя все строки они уже известны на момент компиляции.

Я же привёл пример. Статика не позволит тебе пропустить проверку в начале цепочки. А в динамике либо проверка происходит на входе каждой функции (оборонительное программирование), либо есть вероятность запустить алгоритм не с первого шага, а со второго без проверки. Либо программист начинает мыслить в духе анекдота: «Чтобы заварить чай надо взять пустой чайник, налить в него воду, закипятить, залить воду в заварник, добавить заварку. У вас есть чайник с кипящей водой, как используя его заварить чай? Вылить воду и выполнить заданный алгоритм.».

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

Отлично, но почему им тут не помогла хваленая статика?

Какая статика в GLib/GObject? Там даже типы при выполнении программы создаются.

но правильная где? :) Тред ведь об этом.

Так в заголовке треда ведь.

Или Вам просто скучно?

Ответ на свой вопрос я уже получил. Теперь занимаюсь миссионерством Haskell и Racket,

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

Есть множество валидных данных. Является ли то, что прилетело неясно откуда, элементом этого множества ты в любом случае проверяешь в рантайме

Именно.

В языках со статической типизацией можно с определённой точностью описать это множество валидных данных.

Но контракты, как система валидации данных, явно мощнее. Т.е. как завтипы. Только у каждой системы есть свои преимущества / недостатки. Завтипы все конпеляем на каждый чих доказываем _всю_ программу, зато надежно. Но и страшно, и вообще их по факту нет. Контракты - почти так же надежно как завтипы (исключение - набухался и забыл проверить что-то очень важное), но будут тормозить в рантаймме (тормозить, но работать, а завтипов там вообще не будет). Не требуют длительной и ресурсоемкой перекомпиляции всей программы с доказательством ее корректности. И, если у нас вообще какие-то участки кода обмазанные контрактами почти никогда не используются, то они и не будут влиять на производительность. Мы вообще в типичной программе можем хотеть гарантий в 1% кода, остальные 99% могут работать по принципу «как-то работает и слава богу». Конечно бывают и противоположные варианты, но тогда придется тормозить на контрактах. Потому что выбора-то все равно никакого нет.

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

_Статически_ он может проверить только то, что срослось по (указанным разработчиком) типам. Т.е., что разработчик _предполагая_, что у него будет сортированный массив или валидный json не решит передать дальше какой-то мусор, а точнее чекер ему просто не позволит взять что попало, а только мусор попадающий в указанный тип. Но ведь и разработчик если не с бодуна не будет подставлять музыкальный трек вместо json'a. А чекнули мы этот пользовательский json все равно контрактом в рантайме и просто ему верим (контракту), потому что если он неверно работает - то никакие типы не помогут.

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

Это подтверждает мою мысль, что у Вас, как и у меня, рядом нет специалиста, я имею в виду сильного специалиста.

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

Но контракты, как система валидации данных, явно мощнее.

Любой контракт является функцией. Для любой функции X можно сопоставить тип «проверено функцией X». Зависимые типы позволяют для разных значений возвращать разные типы. Если рассматривать только контракты на входящие данные, а не на результат функции, зависимые типы не обязательны. Обычные алгебраические типы Haskell полностью эквивалентны произвольным контрактам на аргументы. Зависимые типы позволяют не выполнять лишние проверки (если уже проверили, что результат x больше нуля и x – бесконечное целое, нет смысла проверять, что x + 10 тоже больше нуля).

Но контракты, как система валидации данных, явно мощнее.

Нет.