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

Веба на хацкелле просто дохрена. В том числе и на фронте

Можно поподробнее, с примером? Я просто не знаю, под каким микроскопом выискивать это «дохрена».

Ещё есть https://github.com/lettier/movie-monad

You can play video files from your hard drive 💻 or stream videos from the web. 🕸️
To play web videos, click the file open button, paste the URL into the text box, and click open.
Movie Monad can handle file://, https://, and http://.
You can play and pause. ⏯️
You can seek/scrub ⏪ ⏩ through the video. 📼
You can put the video on repeat.

Что же ты делаешь со мной? Я такое делал в делфи за десять минут.

Но всё равно, чтобы писать качественно, читаемо, красиво в конце концов, нужен большой опыт с человеком явно умнее тебя, а у таких людей нет времени. Вот и имеем, что имеем по Хаскелу

В интернетах один человек сформулировал это несколько иначе: чтобы стать продуктивным с хаскелем, нужно месяцы обучения; написать рабочий сервис на clojure или питоне можно после пары дней обучения.

написать рабочий сервис на clojure или питоне можно после пары дней обучения

А на php+mysql можно писать опердени уже через 22 часа и 33 минуты.

allowed to be used in decidable predicates

Это то, что он автоматически вычисляет. Остальное надо как в Агде явно обосновывать.

В принципе, этим определением можно закончить тред :)

В зависимых типах разрешены неразрешимые предикаты?

В зависимых типах разрешены неразрешимые предикаты?

В зависимых типах разрешены не только предикаты.

В интернетах один человек сформулировал это несколько иначе: чтобы стать продуктивным с хаскелем, нужно месяцы обучения; написать рабочий сервис на clojure или питоне можно после пары дней обучения.

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

Ох прекратите это! Вот это кидание мелкими тулзами на хацкелле типа pandoc в ответ на просьбу предъявить примеры софта больше похоже на спор детсадовцев-импотентов, обпившихся стекломоем. Pandoc с тем же успехом мог быть написан на поцкале, пердле или вообще чём угодно. Это довольно уникальная тулза, и вряд ли её кто-то стал бы переписывать. Просто авторам нравился хацкелл и всё.

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

Хачкелловая тусовка в основном крутится вокруг веба, крипты и некоторых других штук, код в которых не то чтобы часто показывают. У того же Clojure, насколько я помню, присутствия на десктопе ровно ноль, но почему-то мало кто задаётся вопросом о нужности этого языка, ибо мы все знаем: Clojure не нужен!

Об активности сообщества же можно косвенно следить по репозитарию библиотек. И тут всё весьма неплохо. Чуть получше, чем в Rust, но в основном засчёт более устоявшейся экосистемы всилу возраста языка. Такие вот дела.

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

Мне кажется, что с этими вопросами нужно к психоаналитику.

Мне кажется, что с этими вопросами нужно к психоаналитику.

Ах, какая печаль! Не понимаешь ты высоких метафор. Тьху, деревенщина!

Можете привести пример? Если типы с параметрами-значениями, то в LH они тоже есть.

Если типы с параметрами-значениями, то в LH они тоже есть.

А я вот давно LH не трогал. Там можно в качестве параметра список использовать? Или другие сложные типы с несколькими конструкторами.

Там можно в качестве параметра список использовать?

{-@ f :: {x:[[a]] | len x > 0} -> Int @-}
f :: [[a]] -> Int
f x = length x

?

Не-не-не, я имел ввиду в качестве параметра типа. Представь, например, что у меня есть полиморфный вариант v :: Variant [A, B, C], где значение этого типа – одно из значений типов A, B или C соответственно. Можно ли с помощью LH проверить инварианты относительно такого значения? Или, например, что в case v of я проверил все возможные значения. В последний раз, когда я такое писал, GHC не всегда вроде отлавливал что case не полный. Хотя может это баг был, но в LH такое видеть в любом случае хотелось бы.

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

Если ты возьмешь Sigma и Cryptol, то это трансляторы-интерпретаторы запросов — то, что обычно пишется на C/C++. Есть пару аналитических систем у Target и Barclays, которым по не совсем ясным для меня причинам показалось недостаточно какой-нибудь Julia. Все эти примеры не являются самодостаточными системами. Единственный пример крупной самодостаточной — это Cardano с их криптовалютой и DSL-ями Marlowe и Plutus, где и блокчейн, и логика вокруг него написана упертыми хаскелистами (или упоротыми).

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

data T = A Int | B String | C Double
f (A x) = x
f (B x) = length x

Выдаёт: «Your function is not total»

Можно ли с помощью LH проверить инварианты относительно такого значения?

Так в условие такой тип можно загнать. Условие ведь (почти) произвольная функция.

data T = A Int | B String | C Double

Выдаёт: «Your function is not total»

А где здесь полиморфизм-то? Я об анонимных суммах говорил, типа Which из https://hackage.haskell.org/package/data-diverse-4.7.0.0/docs/Data-Diverse-Which.html или Variant из https://hackage.haskell.org/package/HList-0.5.0.0/docs/Data-HList-Variant.html.

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

Условие ведь (почти) произвольная функция.

Вот именно, что «почти».

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

Каким образом синглтоны заменяют зависимые типы?

Заменяют – так себе термин.

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

А мир пока еле на статику переходит.

Он это делает последние 50 - 60 лет и никак не перейдет, так что и в обозримом будущем этого можно не ожидать.

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

Все еще хуже, чем я предполагал. Веб на хаскеле очевидно ненужен, крипта просто хайповая тема, которая кое-кого не отпускает, все эти хаскель-криптостартапы загибаются не дойдя толком и до прототипа, потому что что там делать в «крипте» на хаскеле при уже существующем миллиарде +- одинаковых криптовалют. А для разработки торговых страток хаскели не подходят бай дизайн. Я думал, вы там про разработку компиляторов парсеры грамматик итд что-то скажете - это, навскидку, кроме академических забав, единственная ниша, в которой хаскель мог бы норм смотреться.

У того же Clojure, насколько я помню, присутствия на десктопе ровно ноль

Как раз-таки потому что у кложи есть ниша - это production web, data analytics, machine learning & finance. Кложура не на десктопе по причине JVM.

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

Интернет != веб. Упомянутые мной конторы связаны с вебом, но их проекты на хаскеле не связаны с вебом. То есть, они не предоставляют читаемой конечным пользователем инфы, это какие-то внутренние служебные языки запросов и сервисы.

хотелось бы мне посмотреть на код игр на хаскеле

Мне тоже :) А еще хотелось бы посмотреть на сроки их разработки.

нет, я имел именно веб, не связанное с вебом, а именно веб, сервера нттр пишут, службы и т.д. в общем типичный бэк. В принципе вполне удачно для бэка хаскель плюс-минус готов. В нем даже есть темплейт библиотеки для фронта, но обычно там всегда просто жс который дергает рест. По поводу игр https://keera.co.uk/ вот они например.

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

Честно говоря, я никак не могу понять, почему трансляторы на хаскеле и ML получаются лучше всего. Да, неизменяемые типы данных, да, вывод типов, да, функциональные. А как это связать с трансляторами — ума не приложу.

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

К сожалению, я не знаю ни одного крупного примера такого софта на хаскеле.

По поводу игр https://keera.co.uk/ вот они например

https://www.youtube.com/watch?v=lALGsM12RDc — вот один из их шедевров.

А Вы это специально? Это такой троллинг?

Честно говоря, я никак не могу понять, почему трансляторы на хаскеле и ML получаются лучше всего.

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

Еще вариант писать на Lisp (95%) + C (5%) как раз так и сделано в лиспах. Не уверен, что на хаскеле можно написать рантайм особо отличный от хаскель.

В идеале нужен был бы нормальный низкоуровневый язык с s-expr, (опциональной) статической типизацией и выводом типов. Но пока есть rust и haskell.

типа Which из https://hackage.haskell.org/package/data-diverse-4.7.0.0/docs/Data-Diverse-Which.html или Variant из https://hackage.haskell.org/package/HList-0.5.0.0/docs/Data-HList-Variant.html.

Это для меня слишком жёсткий матан. И на онлайновом LH они не подключаются.

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

Так есть же Racket / Typed Racket. Или надо без сборщика мусора? Тогда разве что кодогенерация по образу L++.

Было вообще удивительно видеть что кто-то додумался использовать хаскель для игр. По поводу веба, проще искать по популярным фреймворками типа yesod и более низкоуровневой требухе от них типа wai и warp. А так не в вебе да есть и какие-то более менее известные названия например https://www.tesla.com/careers/search/job/haskell-engineerdatatools-82891?source=Indeed?source=Indeed

Это для меня слишком жёсткий матан. И на онлайновом LH они не подключаются.

Это не то чтобы прямо жёсткий матан, если особо в реализацию не углубляться. Там просто каст в Any и обратно, а нужный тип отслеживается через индекс. Variant – крайне удобная штука при обработке ошибок. Например, у меня в некоторых проектах есть типа вроде type Result a = Variant [Error1, Error2, Error3, ..., a]. И дальше ты в коде можешь сделать

case res of
  V err1 -> ...
  V err2 -> ...
  <....>
  V val -> ...

В сочетании с реализациями исключений в каких-нибудь эффектах (freer, polysemy, сам по вкусу выбери) у тебя получаются checked exceptions в самом лучшем виде. Это так, как пример.

Я понимаю, что в теории refinement types вполне должны с подобным работать, но в силу ограниченности реализации LH тут не всегда подходит. Ну или мы с тобой слишком тупые чтобы их подружить :)

Да, без сборщика нужен. L++ не уверен что компиляция в С++ это верный путь, проект выглядит заброшеным (2015 год последнее обновление). Но если в нем есть нормальная поддержка макросов уже неплохо, можно присмотреться. Низкоуровневый лисп нужен не столько из-за скобочек (хотя они тоже полезны), сколько из-за нормальных макросов, вменяемой системы типов, контрактов и так далее - всего что из этих скобочек может следовать.

Зачем haskell в вебе, можешь меня просветить? Язык с достаточно сложным синтаксисом и семантикой, статически типизированный, весь про матан. Какие такие гарантии нужны в вебе (который весь к тому же про IO), что туда хаскель наворачивают еще и без нормального репла - clojure и даже js лучше выходит.

Ещё есть такое: https://github.com/tonyg/pi-nothing

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

Какие такие гарантии нужны в вебе

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

Я не нашёл. Примеры в https://github.com/tonyg/pi-nothing/tree/master/examples да и сама ОС в https://github.com/tonyg/pi-nothing/tree/master/baremetal фактически пример.

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

И при чем тут хаскель?

Если твоя позиция заключается в том, что «тут и JS достаточно», то разумеется вообще не причём.

Так проверка может проходить по контракту, как в кложе например. Зачем тут такая развесистая система статических типов? Дата все равно прилетает из IO.

Так проверка может проходить по контракту, как в кложе например.

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

Да, про статика vs динамика не интересно в сотый раз, но все же почему haskell, а не rust или go (ну ладно, go ненужен)? Я могу себе представить области где статика действительно полезная опция и даже хаскель, выше писал об этом. Но веб... в котором нам все прилетает откуда угодно в любых форматах, которые _статически_ вообще никак не чекаются, веб который сплошь про прототипы, некритичный к падению в определенных запчастях, если можем перезапустить.

но все же почему haskell, а не rust или go (ну ладно, go ненужен)?

Ну, разверни этот вопрос: почему Rust а не Haskell? Звучит так же тупо.

Но веб… в котором нам все прилетает откуда угодно в любых форматах, которые статически вообще никак не чекаются

Ты Рича Хикки обчитался? У него был похожий аргумент. Я открою тебе гигантскую тайну, которую Рыцари Ордена Святой Лямбды хранят многие поколения и скрывают от вас динамических: тайпчекер в языках со статической типизацией не проверяет данные. Вообще никак. Тайпчекер проверяет твой код на соответствие заявленным в типе инвариантам. А от мощности системы типов уже зависит, насколько сложные инварианты ты можешь этими типами закодировать. Вот и всё.

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

но все же почему haskell, а не rust или go (ну ладно, go ненужен)?

Ну, разверни этот вопрос: почему Rust а не Haskell? Звучит так же тупо.

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

Ты Рича Хикки обчитался? У него был похожий аргумент.

Нет.

тайпчекер в языках со статической типизацией не проверяет данные. Вообще никак.

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

проверяет твой код на соответствие заявленным в типе инвариантам.

И нахрен мне это надо, чтобы уловить класс ошибок размером в 0,2%? Вы сами себе проблему типов выдумали, чтобы потом с трудом ее преодолевать.

А от мощности системы типов уже зависит, насколько сложные инварианты ты можешь этими типами закодировать. Вот и всё.

Ясно, просто дрочь.

Я бы поставил вопрос иначе, зачем он вообще

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

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

Обычно программа - это сплошное IO и работа с внешними данным. И _кое_где_ нам нужен чистый красивый код без побочных эффектов, который про алгоритмы. Но даже там нам нужен способ нормально спуститься в императивный ад в целях оптимизации скорости выполнения.

Но веб… в котором нам все прилетает откуда угодно в любых форматах, которые статически вообще никак не чекаются,

Статически чекается не то, что прилетает, а код, который чекает то, что в него прилетает. Например, что функция parseJSON для любой строки возвращает валидный json либо ошибку, а не взрывается.

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

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

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

В JS самые совершенные типы. Зачем, что-то ещё придумывать