Что круче: Лисп или Хаскелль?

Монада - это один единственный простенький макрос.

К счастью, нет. Монада – это один тип и две функции.

> Это удобно.

Это вредно. Вывод типов- простоакадемическая приблуда, которая не имеет практического применения. Зато диссеры, диссеры.

Может быть, но хотелось бы ссылочек на авторитетные источники.

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

> Ага, только это не компайл-тайм, а рантайм.

Ну и что?

Не пойдёт.

Почему?

в том же лиспе несложно написать небольшой макрос, который вычислит 95% подобных вызовов.

Show me the code.

account.send_money_to(Account receiver, unsigned int money)

int выводится. А то, что вывод типов плохо совместим с сабтайпингом – ну да, плохо.

> Что ты понимаешь под словом «новое», анон?

Новые = не являющиеся перепевкой старых.

Да ну?

Ну да.

А. Я понял. Тебе, видимо, лет десять, и в твоём возрасте время воспринимается иначе. Пройдёт.

Идее АДТ не меньше 30-40 лет и с тех пор ничего нового в этой области не было. Только высасывание из пальца.

> Фу-у-у. Прямая работа со стеком и язык высокого уровня – вещи, ИМХО, вообще несовместные.

типичное заблуждение тех, кто не понял идеологию с++ (хотя он и не работает со стеком)

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

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

как минимум первые 5 из них мне интересны; остальные похоже из серии, к которой я присмотриваюсь, но профита пока не вижу

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

Именно по-этому ни в одном успешном статически типизированном языке нету полного вывода типов, лол.

>> Это удобно.

Это вредно. Вывод типов- простоакадемическая приблуда, которая не имеет практического применения. Зато диссеры, диссеры.

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

let f x y = x + y f 2 2.0 все корректно чекается а должен быть эррор

Он и будет.

Prelude> let f x y = x + y f 2 2.0

<interactive>:1:16:
    Occurs check: cannot construct the infinite type:
      t = (a -> t -> t1) -> t2 -> t3 -> a
    Probable cause: `y' is applied to too many arguments
    In the second argument of `(+)', namely `y f 2 2.0'
    In the expression: x + y f 2 2.0

В хаскеле конечно сабтайпинга нет

В расширениях, кстати, есть. У Int -> Int есть подтип forall a. a -> a. Нужно не слишком часто.

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

Бредишь. Тайпклассы – это то самое программирование на типах.

> Разумеется. Язык весьма практичен, если забыть про эту ересь со стеком.

Видимо, именно из-за его практичности на нем не написано ни одной практически полезной программы?

Другое дело, что алгоритм вывода типов устанавливает, может ли данное выражение ВООБЩЕ быть типизировано. И это оччень сильная проверка.

Он, однако, не может показать, что выражение типизировано быть НЕ МОЖЕТ. То есть практической пользы от этого алгоритма нет.

> К счастью, нет. Монада – это один тип и две функции.

Там о монадах шла речь в контексте ДСЛ, так что, видимо, имелась в виду do-нотация. Которая - 1 единственный макрос.

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

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

Вывод типов даже для обычного типизированного лямбда-исчисления с полиморфизмом неразрешим.

В смысле, для System F? Да, но это очень сильная система.

> Ну это не серьёзно, пример применения я привёл.

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

Ну и что?

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

Новые = не являющиеся перепевкой старых.

Перепевкой чего являются GADTы? Type families?

Идее АДТ не меньше 30-40 лет

А GADT – не ADT, им меньше.

>> Ну это не серьёзно, пример применения я привёл.

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

Вывод типа undefined в языке без вывода типов, да ещё и удобнее? Хмм.

типичное заблуждение тех, кто не понял идеологию с++

Я, как раз, понимаю. Хаскель, как я уже отмечал выше, очень помогает понять идеологию C++.

А насчёт заблуждений... как насчёт машин без стека вообще?

> Он и будет.

Ты же понял, что имело в виду, посто лор съел разметку let f x y = x + y

f 2 2.0

В расширениях, кстати, есть.

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

Нужно не слишком часто.

Конечно, тайпклассы значительную часть юзкейсов покрывают.

Тайпклассы – это то самое программирование на типах.

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

Именно по-этому ни в одном успешном статически типизированном языке нету полного вывода типов, лол.

«Поэтому» – почему именно? Потому что без вывода типов статическая типизация вредна?

Он, однако, не может показать, что выражение типизировано быть НЕ МОЖЕТ. То есть практической пользы от этого алгоритма нет.

Вообще-то, если некий алгоритм вычисляет предикат P, то почти тот же алгоритм вычисляет предикат «не P». Учи логику.

Там о монадах шла речь в контексте ДСЛ, так что, видимо, имелась в виду do-нотация.

Нет, конечно.

можно сделать и в языке без вывода типов

Show me the code.

> Он сокращает время разработки в разы

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

а в сочетании с программированием на типах

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

В смысле, для System F? Да, но это очень сильная система.

Что за бред? System F - самая слабая система. Слабее только простая типизированная лямбда. По выразительности она тоже на нуле.

> Без запуска и полномасштабного тестирования не узнаешь, не ёкнется ли где-нибудь этот «выбор» – раз.

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

В случае рекурсивных типов получаем линейную сложность

А еще - можно просто не писать на языке с динамической типизацией так, как на языке со статической. Зачем использовать костыли?

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

Нет, не понял. Я не собираюсь дешифровать за тебя, если ты не можешь освоить LORCODE.

let f x y = x + y
f 2 2.0

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

Что значит «нормальный»? Да, это сабтайпинг. Честный.

На деле тайплкассы - это просто костыль для реализации ограниченной квантификации и ad-hoc полиморфизма.

Ты опять бредишь. Тайпклассы – это вообще не ad-hoc, на самом деле. Ad-hoc – он в рантайме. Тайпклассы – это вполне себе параметрический полиморфизм плюс программирование на типах.

Ad-hoc начинается в existential types.

> Перепевкой чего являются GADTы? Type families?

Перепевкой ADT и полиморфизма.

А GADT – не ADT, им меньше.

В GADT нет ничего нового по сравнению с ADT.

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

Кто будет решать, что локальное, а что нет?

Мы уже выяснили

Вы пролили на это некоторое количество слюны, и всё.

System F - самая слабая система.

??? Мсье шизофреник?

> «Поэтому» – почему именно? Потому что без вывода типов статическая типизация вредна?

Ну, видимо да.

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

Бред несёшь, как обычно. Недаром сделано столько специализированных инструментов для тестирования, и всё равно ни один нормально не работает.

А еще - можно просто не писать на языке с динамической типизацией

Эта часть у тебя получилась правильно.

В GADT нет ничего нового по сравнению с ADT.

Бредишь. В который раз. Если бы не было ничего нового, их бы незачем было придумывать.

Ну, видимо да.

«Полного вывода типов нет, потому что без него плохо».

Сам понял, чего сказал?

> Вообще-то, если некий алгоритм вычисляет предикат P, то почти тот же алгоритм вычисляет предикат «не P». Учи логику.

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

> Нет, конечно.

Вообще-то да. Потому что монады сами по себе с ДСЛ никак не связаны.

Если алгоритм вычисляет, является ли P истиной, то в общем случае мы ничего не можем сказать о том, как он связан с алгоритмом, вычисляющим отрицание P.

function calculateNotP(arg) {return !calculateP(arg);}

Ты точно упоролся.

Почитай про полуразрешимые теории, например.

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

> И что этот кусок кода должен продемонстрировать?

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

Что значит «нормальный»? Да, это сабтайпинг. Честный.

«это» - это что?

Ты опять бредишь. Тайпклассы – это вообще не ad-hoc, на самом деле. Ad-hoc – он в рантайме.

Лол, икспертиза школьника хаскидебила. У тебя что, диспатч по типу в рантайме разрешается? Охренеть.

Тайпклассы – это вполне себе параметрический полиморфизм плюс программирование на типах.

Прежде чем следующий раз упоминать «программирование на типах» сперва скажи, что это такое. Ну а с параметрическим параморфизмом тайпклассы никак не связаны, да. Если тайпклассы убрать, то параметрический полиморфизм в хаскеле останется. А вот ad-hoc полиморфизма уже не будет.

Вообще-то да.

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

Потому что монады сами по себе с ДСЛ никак не связаны.

Нет. Но довольно часто оказывается удобным сделать DSL монадическим.

> Кто будет решать, что локальное, а что нет?

Никто. Зачем?

??? Мсье шизофреник?

Нет. А ты что, не знал что System F одна из самых слабых систем типов? Это для тебя новость была?

> Бред несёшь, как обычно. Недаром сделано столько специализированных инструментов для тестирования, и всё равно ни один нормально не работает.

В какой реальности? У всех все прекрасно работает. Только хаскидебилы кормят всех сказками о том, что без анальной ебли с тайпчекером программы писать нельзя.

> Бредишь. В который раз. Если бы не было ничего нового, их бы незачем было придумывать.

Придумывать всегда есть зачем - тема для диссера же. Делом заниматься мозги не позволяют, приходится высасывать из пальца GADT. Ну а кому легко? Если бы новое что-то было, то ты легко бы щас сказал, что именно - но ты же не сказал И не скажешь. Потому что нечего.

> Сам понял, чего сказал?

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

То, что есть - чекер из-за вывода типов пропустил некорректный код.

Почему некорректный?

«это» - это что?

forall a. a -> a – подтип Int -> Int.

У тебя что, диспатч по типу в рантайме разрешается?

Когда я пишу на C++ – конечно. Когда я использую existential types – конечно. А тайпклассы разрешаются в компайл-тайме, поскольку, не обессудь, не относятся к ad-hoc.

Прежде чем следующий раз упоминать «программирование на типах» сперва скажи, что это такое.

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

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

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

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

Да как раз-таки связаны. Или ты видишь принципиальную разницу между

class M a where m :: a -> a
instance M Integer where m x = x + 1
doMTwice :: M a => a -> a
doMTwice x = m (m x)

data M a = M {m :: a -> a}
instMInteger :: M Integer
instMInteger = M {m = \x -> x + 1}
doMTwice :: M a -> a -> a
doMTwice instMa x = m instMa (m instMa x)

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

Вот как раз с инструментами для тестирования – полнейший извращённый секс и происходит.

Придумывать всегда есть зачем - тема для диссера же.

Нет, эти люди уже давно защитились.

> function calculateNotP(arg) {return !calculateP(arg);}

Дебил, кто тебе гарантирует, что на arg, для которых предикат дает false, calculateNotP(arg) будет работать конечное время?

Читал, когда тебя ещё на свете не было. Только они тут не в тему.

Как раз в тему.

Алгоритмы вывода типов всегда завершаются.

Что, правда? Ну напиши мне алгоритм вывода типов для полиморфной типизированной лямбды 3 порядка. Я потом проверю, как твой алгоритм докажет за конечное время великую теорему Ферма.

Да, понял.

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

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

Ну, какой-то вывод типов там таки есть. Очень хреновый, но местами выручает.

Почему, например, когда делали сишку, не прикрутили вывод типов к ней? Ведь тогда уже весь теоретический бекграунд был.

Так это не у меня надо спрашивать. Моё предположение – тупо не знали (не понимали) этого «бэкграунда». Так же, как Маккарти лямбда-исчисления не понимал.

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

Не, школота до них ещё почти не добралась. Школота – это как раз те 99%, которые на динамике да на статике без вывода хреначат.

> Нет. То есть, я, конечно, не могу ручаться за автора того коммента, но подобное высказывание достаточно распространено в Haskell-среде, и имеет совершенно определённый смысл.

Ну в хаскель среде вообще любят придавать какой-то особый смысл чему-нибудь. По факту же, единственное, что связывает монады с ДСЛ - это do-нотация.

Нет. Но довольно часто оказывается удобным сделать DSL монадическим.

Вобщем-то нет, такого никогда не бывает. По крайней мере на данный момент ни одного подобного «монадического ДСЛ» не существует.

Что, правда?

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

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

Что не отменяет того факта, что он есть.

Вобщем-то нет, такого никогда не бывает.

Чем Parsec не DSEL, например?

Успешные статически типизированные языки это C, Pascal, С++ (и все его кривые продолжатели)? Да вы задолбали уже…