ну для 1/x нету же спецсинтаксиса, и как-то живут. а для 0-x почему-то нужен.

Што

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

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

ну для 1/x нету же спецсинтаксиса, и как-то живут. а для 0-x почему-то нужен.

Прямо как в математике

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

а для продакшена нет

ну для 1/x нету же спецсинтаксиса, и как-то живут. а для 0-x почему-то нужен.

Это не синтаксис для 0-x, это литерал для отрицательных чисел

Без -x можно обойтись, а без -2 нельзя

negate 2

не благодари)

это не литерал

а для продакшена нет

от ATS до Isabelle, и сбоку где-то военный Spark. есть.

(_ - 2) пурсовое решение норм

((flip (-)) 2)

чем вычитать двойку, не проще прибавить -2?

Че ты усложнил

(`(-)` 2)

надо ввести синтаксис (-)' для флипнутого оператора

(`(-)` 2)

это работает?

(`(-)` 2)

Хз

не парсит

Все же знают, что -2^31 без литерала не записать нормально?

Ну или -2^63

(Prelude.- 2)

не, я понимаю. pointfree. но звучит все равно неплохо - хаскеллисты не любят лямбды! а на эмблеме что?

ещё древнейшие хаскеллисты говорили — не поминай всуе лямбду свою!

Ну или -2^63

почему? неявный fromInteger везде же

((flip (-)) 2)

subtract = flip (-)

неинтересно

ещё и все скобки лишние, кроме тех, что вокруг минуса

мы тут не за интерес, а за уменьшение синтаксического мусора!

Все же знают, что -2^31 без литерала не записать нормально?

есть шероховатости, но всё равно можно λ> -128 :: Int8 <interactive>:3:2: warning: [-Woverflowed-literals] Literal 128 is out of the Int8 range -128..127 If you are trying to write a large negative literal, use NegativeLiterals -128 λ> :set -XNegativeLiterals λ> -128 :: Int8 -128

от ATS до Isabelle, и сбоку где-то военный Spark. есть.

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

а, блин, это унарный минус, а не литерал, торможу

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

а когда эти языки стали для production готовыми?

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

вроде в 95% там ручное переписывание как у se4L, в 5% экспорт

Мое мышление ограничено идрисом и леаном, полную спеку мартина лёфа я не читал, но мне как-то очень сложно представить, как в хаскель можно ввести завтипы, слишком кардинальное изменение

не очень интуитивно

{-# LANGUAGE NegativeLiterals #-}

как это поможет?

Позволит писать -10 и иметь в виду отрицательное число, а не применение унарного оператора к положительному

ну

Мое мышление ограничено идрисом и леаном, полную спеку мартина лёфа я не читал, но мне как-то очень сложно представить, как в хаскель можно ввести завтипы, слишком кардинальное изменение

Как-то так: https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf

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

там много “необычных” решений, но как 1-е приближение…

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

при этом не убивая хорошую возможность рефакторинга

которая страдает у языков с зав типами

Мое мышление ограничено идрисом и леаном, полную спеку мартина лёфа я не читал, но мне как-то очень сложно представить, как в хаскель можно ввести завтипы, слишком кардинальное изменение

В ghc практически невозможно, конечно, но так я особых проблем не вижу. Какой-нибудь haskell 2010 достаточно тупой, что всунуть зависимые типы в него. Когда я впервые услышал про хаскель и пробовал написать свой первый факториал юзать хугс считалось норм. А кто последний раз про него слышал? Не удивлен, если через 3-4 года кто-нибудь запилит новый недокомпилятор в соответствии с требованиями времени

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

ну и непонятно, как воспоминания о хагсе приводят к надеждам на появление новой нормальной хаскельной имплементации

Хз

(pred . pred)

mconcat . flip replicate pred

mconcat . flip replicate pred

что это?

(pred . pred)

Обобщенный код для этого же

вычисление -n?

Создание декремента на n скорее

а да ок

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

но нет

только через Endo

для функций определён, и делает совсем другие вещи

потому твой код читается не так, как ты хотел

Как на русский перевести thunk адекватно?

Ну заменить mconcat на getEndo . foldMap Endo

Как на русский перевести thunk адекватно?

В редакс-сообществе никак не переводят. Полагаю, популярного перевода нет

мне что-то подсказывает, что либо опечатка, либо типа "тук"

predN n x = x & (appEndo $ Prelude.foldMap Endo (replicate n pred))

так да

вроде в 95% там ручное переписывание как у se4L, в 5% экспорт

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

В редакс-сообществе никак не переводят. Полагаю, популярного перевода нет

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

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

вопрос не про это был

Как на русский перевести thunk адекватно?

не надо его переводить имхо

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

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

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

как бы намекает о сообществе жс и редакс

поехавший

поехавший

+

вопрос не про это был

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

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

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

это, скорее, ответ ;) если бы Х-ь был цельным языком, я бы полностью согласиля. а так - не язык, а "тысяча и одно" расширение, которые еще и как-то взаимодействуют между собой. вавилонская башня вместо одного языка. так что если сравнивать с уже упомянутым Идрисом, то Х-ь сложнее без выгоды от это сложности. тем, кто пишет на Х-е ежедневно, это может быть незаметно, ибо "глаз замылен" привычкой. лично я бы поставил на Идрис.

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

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