Кто эффективней?

маги, чем комитет

результат примерно один и тот же, а время разрабов не тратится

хотя если в 2020 включат хотя бы одно расширение то честь им и хвала

Комитет-то вообще неэффективен. А прагмы позволяют включать новые фичи в язык не дожидаясь свистка рака на горе.

ну да

поэтому наличие прагм это весьма хорошая вещь

в расте так же поступили, если я правильно понял

можно юзать новые фичи не дожидаясь включения в stable

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

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

нет, в С++ другая ситуация

в С++ ситуация примерно как предлагаете вы изменить в лучшую сторону

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

я не вижу ни одного сильно отличающегося варианта, который не хуже

единственный путь вперёт это стандартизация и включение фич в язык постепенный и параллельный процесс

*вперёд

примерно то, чем занимается комитет сейчас

но если воспринимать реальность серьёзно, то затея это немного бесперспективная

нет, в С++ другая ситуация

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

извините, но перевернутым видите вы

говорить, что опциональные прагмы и периодические стандарты включаетмые через —std это одно и тоже это минимум глупо

так я как раз так не говорю.

добавление того, что предлагает эйзенберг не сделает haskell тотальным

но а зачем делать его полностью тотальным

что я сравнивал, я написал.

мне ещё один бесполезный язык не нужен

он позволит получить зависимые типы в ограниченных частях программы

но а зачем делать его полностью тотальным

да незачем делать его тотальным. точно так же, как незачем делать С++ ФП. нужно просто делать новые языки.

собственно haskell движется в сторону более мощных типов с другой стороны

пока получается лучше, чем у языков с зависимыми типами двигаться в сторону general purpose языка

я вижу как получить, то что мне нужно в работе в haskell

общаться с хаскеллистом - все равно, что разговаривать со свидетелями Иеговы. :)

только наоборот

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

а не обращаться к нему о том как тебя не понимают

твой Бог тебя тут не слышит

о как. вчера Вы говорили, что я не умею читать.

это не отменяет то, что в какой-то момент аргументы от вас сформировались в более-менее нормальные

например когда говорили, про Hask не категорию и денотационную семантику

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

а всякие высказывания какие haskell-листы дураки и т.п. оставьте для соседнего чатика

там они находят понимание

давайте начнем с начала. можно допиливать фичами существующий язык, можно пытаться запилить новый. успешные языки, вроде С++ или Х-я, начинают в какой-то момент страдать первым. но движение языкостроения определяется не первым, а вторым. (исправил) когда-то было важно, что Х-ь стал площадкой для обкатки идей ФП. тут у него все получилось, и отдельные фичи экспортируют в другие языки, в том числе инерционные. но сейчас прошло время, и сейчас нужно обкатывать новое. Вы уже не передний край разработки, Вы мейнстрим. если бы содатели Х-я когда-то думали инерционно, они бы не заняли созданием Х-я, а пилили бы Фортран-9000. но они не совершили эту ошибку, и в результате у нас есть Х-ь. давайте и сейчас не совершать ошибку. Есть прогрессивные языки вроде Идриса, за ними будущее (там посмотрим, конечно). Важно вкладывать силы в них, на тех же основаниях, на которых когда-то было важно вкладывать силы в Х-ь.

стоп, Haskell проектировался как площадка для обкатки идей ФП, в этом суть языка. Т.е. он сделан именно для этого и задачу выполняет. Haskell все ещё является передним краем по многим направлениям, зависимые типы туда не входят. Для таких направлений можно смотреть на языки. Idris вроде нигде не декларируется языком для обкатки идей. Я могу прийти туда со своей статьей по polyhedral compilation, или метапрограммированю, аспекту линейных типов и получить расширение в язык (или расширение языка) в следующем релизе, который будет меньше, чем через год? Если нет, то нишу Haskell идрис не занимает. Могу ли я написать программу эффективную программу не вложив в idris десяток другой человеколет? Я крайне сомневаюсь, может за последний год что-то и изменилось, но тогда хоть как-то разумно работающих бекендов не было. И инвестиции в idris тут просто огромные. Если я хочу сделать типы в части моей программы на Haskell более выразительными не потеряв то, что есть, то я должен смотреть в сторону F-omega-with-coercions, понимая до какого момента это будет работать. Смотреть на Idris мне смысла нет. Если я хочу доказывать модели, вести исследования в области "настоящего" программирования с зависимыми типами, или просто получить репутацию или опыт работы с компиляторами для резюме, или есть для всей программы нужны большие гарантии. То смотреть на идрис имеет смысл, но тут вопрос уже с другой стороны, на идрис или на пруверы?

Прямо сейчас haskell это язык с достаточно сильным для применения в индустрии компилятором, idris это игровая площадка товарища Бреди и еще пары товарищей. Чего тут дальше то разглагольствовать? Все заинтересованные в применении в индустрии в ближайшие 5-10 лет будут развивать GHC, это разумно. Теоретики(тут спорно кстати) и диванные эксперты могут за идрис топить и уже топят.

Сама полезность концепции idris еще не проверена. Вроде и не прувер, а вроде и как ЯП для программистов. Норм ли будет программистам? А хрен их знает. Можно ли нормально доказывать как в Coq/Isabelle HOL? Скорее нет.

В общем если готовы много лет вложить за идею и это в кайф - почему бы нет.

> polyhedral compilation воу, это еще что

я лично idris рассматриваю как компилятор для примеров из книжки Бреди

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

т.е. автоматическое переписывание программы так чтобы было эффективно

(естественно у меня статей по этому нет)

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

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

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

в общем для dep types в haskell придётся страдать больше чем сейчас в идрисе

и они будут другие

в плане что все равно как прувер использовать не получится

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

синглтоны кстати попроще для использования стали с TypeInType и восьмеркой

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

все так, я поэтому все еще считаю себя маргиналом

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

конечно

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

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

если ради прувера что-то и выкидывать, то не ради idris

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

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

хм.. инетерсно нас все ещё не обсуждают на соседнем канале..

в смысле кок какойнибудь? Из него же какой-то адовый хаскель экстрактится

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

получается простынка из unsafeCoerce и потом ничего не реврайтится

вон когда мы promela использовали мы тупо модель кода переносили

да, она в хаскель компилируется (тоже адовый, понятно, весь в ансейфкоэрсах)

в смысле кок какойнибудь? Из него же какой-то адовый хаскель экстрактится

а из агды не адовый чтоли?!

но это другое направление

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

ладно я пока logical foundation даже не осилил, мне рано о всем этом

я его не осилил еще когда он был software foundations

т.е. в идеале пишешь в хаскельном проекте модуль на агде