\x -> (x x)

Скима выводит типы в рантайме.

Что значит «выводит»?

Нет в рантайме никакого вывода типов.

Потому что ничего не надо выводить в рантайме - потому что у всего и так уже есть тип.

lovesan

s/выводит/проверяет/

Зачем тут что-то проверять?

Ты не понимаешь динамическую типизация, совершенно.

ORLY?

«Работать» и «проходить проверку типов» это абсолютно, совершенно, и полностью, ортогональные концепции.

Но, я, например всегда и говорю - в лиспе всегда все именно работает.
А в хаскеле только проверки типов проходятся, да и то не все. И не работает нихрена.

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

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

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

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

lovesan

\x -> x x

в каких системах типизации указанное выражение будет корректным?

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

Можно, например, написать так:

newtype Rec a = Rec (a -> (a, Rec a))

w :: Rec a -> a -> (a, Rec a)
w (Rec f) = f . fst . f

Система в которой можно опускать подобную Rec обвёртку для рекрсивных типов это System Fω extended with equi-recursive (infinite) types.

System Fω extended with equi-recursive (infinite) types

Есть про в TAPL. Говорят, реализовано что-то подобное в OCaml через -rectypes. А Agda (2.8.8) тоже есть про бесконечные типы, но там, как я понял, как и в хаскеле - через обвёртки.

Agda (2.8.8)

2.2.8.

контексте динамической типизации такого понятия как «ошибка типов» нет

Т.е. там, где даже самая примитивная С-подобная система типов страшно заверищит, в бедное вычисление на динамическом языке будут пихать неверные данные, пока оно не проблюется. А полученный «дамп» можно невозбранно анализировать. Проблема только в том, что на практике, проблюется совсем не то вычисление, ИЧСХ, свосем не в тот момент, когда ошибка произошла, да и «дамп» будет релевантен только внутренним структурам и стратегии обработки ошибки. Т.е. будет примерно так: «Ням-ням... Ну что за херовые данные... Блюээээээ!»

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

А полученный «дамп» можно невозбранно анализировать.

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

Проблема только в том, что на практике, проблюется совсем не то вычисление, ИЧСХ, свосем не в тот момент, когда ошибка произошла

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

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

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

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

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

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

А насчет частоты - бывают они примерно так же часто, как бывает использование совершенно не тех функций не в тех местах. То есть, ошибиться с типами это все равно что перепутать имена функций или операторов, и вместо, скажем, make-string сделать make-rational, а последнее бывает исключительно редко, у всех вменяемых разработчиков - у невменяемых может и часто бывает, но так ведь почему хаскель и прочая статика изначально не позиционируется как языки для невменяемых?

В хаскелях мы получаем бессмысленный отблев тайпчекера

t = map [1,2] id

/tmp/t.hs:3:9:
    Couldn't match expected type `a0 -> b0' with actual type `[t0]'
    In the first argument of `map', namely `[1, 2]'
    In the expression: map [1, 2] id
    In an equation for `t': t = map [1, 2] id
Failed, modules loaded: none.

видишь - указал строчку и отступ ошибки, более того, на «/tmp/t.hs:3:9:» можно нажать и сразу попасть на место где перепутаны местами аргументы функции map. Хватит уже сказки рассказывать.

То есть, ошибиться с типами это все равно что перепутать имена функций или операторов

Нет, есть же ещё вариантные типы, полиморфные типы, классы и семейства типов - можно сделать довольно много по ограничению логики программы с любой (как в динамике) к конкретной. Так, например, инварианты обращения с IO и STM это исключительно типы (IO, STM, и функций для них), тоже самое про стек монадических трансформиров приложения - типы это логика приложения (даже буквально можно так сказать, следуя изоморфизму CH).

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

Да. Дебаггер. На компе конечного пользователя. Но я не про это.

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

Вот эта картина реалистичнее.

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

Ты совершенно не в курсе реального положения вещей. Но для лиспера это простительно.

смотрим стектрейс

К слову, Get-PSCallStack в powershell-е на чих давал что-то около 140 кб текста. В общем, обходились без стектрейса :)

видишь - указал строчку и отступ ошибки

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

Нет, есть же ещё вариантные типы, полиморфные типы, классы и семейства типов - можно сделать довольно много по ограничению логики программы

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

Так, например, инварианты обращения с IO и STM это исключительно типы

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

Да. Дебаггер. На компе конечного пользователя. Но я не про это.

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

И что же мы видим? блаблабла

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

и наконец, выясняем что вот в этом вычислении мы перепутали местами переменные и оно пишет не в тот буфер.

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

Максимум - не дать сложить жирафов с носорогами

Вообще - применять несовместимые функции к друг другу, учитывая, что применение это основная операция в ФЯП это уже достаточно много. Ну, например, в do-блоке IO могут быть только IO операции, а в do-блоке STM - только STM. Смешать их никак не получится, так что мы получаем comile-time гарантию атомичности обращений с STM (с учётом того как компилируются IO и STM, но это можно и не знать). Таких примеров может быть сколько угодно.

А вот это, кстати, неверно.

Я слово не то использовал, пусть не «инварианты», а «паттерны» или как это лучше обозвать. Короче, очевидно же, что типы _весьма_ ограничивают свободу выражений, отсекая лишнее, и фиксируя логику программы к какой-то конкретной. Можно утверждать что это не нужно, но это всё-таки так.

Вообще - применять несовместимые функции к друг другу

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

Ну, например, в do-блоке IO могут быть только IO операции, а в do-блоке STM - только STM.

Как я и сказал - жирафы с носорогами. А вот гарантировать на уровне типов, что применение ф-и unsafePerformIO не приведет к некорректной работе - слабенькая система типов хаскеля уже не в состоянии. То есть даже такие элементарные инварианты - не в состоянии. А если говорить о чем-то более серьезном, о инвариантах, которые как раз нам на практике и хочется исполнять? То есть до тех пор пока мы находимся в смысловом поле написания факториалов - все хорошо. Но как только шаг вправо/влево - все, пропасть.

Короче, очевидно же, что типы _весьма_ ограничивают свободу выражений

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

Обоюдотупой разговор получается, голословно же всё. Ты просто высказываешь своё ИМХО - что это, мол, всё в теории, в факториалах и т.п. Я точно также могу начать говорить - что нет, мол, на практике, в реальных программах™, но если сам не попробуешь всё равно ведь мне не поверишь.

Возьми обычные полиморфные ADT + паттерн-матчинг + обычные хорошо-типизированные функцие + классы типов для интерфейсов. Ты можешь с помощью этой примитивщины моделировать что угодно, и для всего моделируемого будет справедливо свойство well-typedness. Get? Ну а нетотальные функции, unsafePerformIO и прочая - это да, плохо, но, с другой стороны, это просто (как избавиться от unsafePerformIO и сделать, например, числа ADT с тотальными функциями - очевидно так, что порог вхождения повысится на чувствительную величину).

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

однако на практике этого не происходит

В ХАСКЕЛЕ не практике не происходит. В Agda, Coq, Epigram - происходит. И собственно? Так потому хаскель и существует, что обеспечивает некий баланс между сложностью и уровнем гарантий.

А уж аргумент, раз не гарантирует ПОЛНОСТЬЮ, так значит не нужна ВООБЩЕ, он, простите, совершенно детский. Хотя бы потому что помимо гарантии корректности у системы типов есть еще и конструктивистская функция. Но для адептов динамики это просто не понятно.

В Agda, Coq, Epigram - происходит.

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

А уж аргумент, раз не гарантирует ПОЛНОСТЬЮ, так значит не нужна ВООБЩЕ, он, простите, совершенно детский.

Аргумент не в том, аргумент, полностью, в следующем:

1. примитивные системы типов (навроде как в хаскеле) могут отловить лишь примитивные ошибки, логика все равно тестируется.

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

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

4. Из-за типодрочесртва CS последние десятилетия не развивается вообще никак - вместо поиска и развития альтернативных подходов легче написать диссер про никому не нужное расширение лямбда-хуямбда-омега-стрелки зигохистоморфическими препроморфизмами. Вообще, сложилось мнение, будто CS = исследования в области систем типов и больше исследовать нечего. Тупик, как есть. То есть, понятно, системы типов исследовать тупо _удобно_, но хотя бы в некоторой мере наука должна идти и от требований практики в том числе, потому что, блять, оно так всегда - полезные для практики задачи обычно неудобны.

Хотя бы потому что помимо гарантии корректности у системы типов есть еще и конструктивистская функция. Но для адептов динамики это просто не понятно.

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

Ты можешь с помощью этой примитивщины моделировать что угодно, и для всего моделируемого будет справедливо свойство well-typedness.

А какой это дает профит? Мне не надо well-typedness. Мне надо, чтобы программа работала, решала определенные задачи. От того, что я буду повторять мантру «well-typedness» у меня задачи решатся? Да вроде нет.

Некоторые расширения даже позволяют моделировать какие-то специальные вещи - вроде линейных типов с помощью классов типов.

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

(как избавиться от unsafePerformIO и сделать

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

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

Определение «примитивной ошибки» в студию. Если подразумевается общепринятое понимание этих слов - то утверждение неверно.

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

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

Ну, во-первых, в самих тестах ошибки тоже бывают. Во-вторых, тестирование НИКОГДА не говорит о том, что какого-то вида ошибок нет вообще, оно лишь говорит, что на тестовых примерах они не обнаружены. В отличие от системы типов.

Кстати, наличие системы типов само по себе упрощает написание тестов на порядок (см. QuickCheck).

Из-за типодрочесртва CS последние десятилетия не развивается вообще никак

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

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

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

который сразу гарантирует, что unsafePerformIO всегда вызывается корректно.

Использование unsafe-функций a priori некорректно. А монадический интерфейс в хаскеле есть, называется IO.

Если подразумевается общепринятое понимание этих слов - то утверждение неверно.

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

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

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

Ну, во-первых, в самих тестах ошибки тоже бывают.

В спецификациях - тоже.

Во-вторых, тестирование НИКОГДА не говорит о том, что какого-то вида ошибок нет вообще, оно лишь говорит, что на тестовых примерах они не обнаружены. В отличие от системы типов.

Система типов так же не гарантирует, что ошибки НИКОГДА не будет, потому что никто не гарантирует ошибки в тайпчекере, железе и т.п.. Это первое. Второе - на практике никому не нужны гарантии отсутствия ошибок, на практике нужно, чтобы вероятность наличия ошибки была меньше определенного предела (который зависит от задачи, понятное дело). Кроме того, система типов не гарантирует отсутствия ошибок _в принципе_, она гарантирует только отсутствие ошибок, которые мы покрыли (не говоря о том, что не всякая система типов в состоянии покрыть всякий класс ошибок). Если мы некоторый класс ошибок типами не покрывали (тупо профукав), то тайпчекер его и искать не будет, даже если теоретически система типов позволяет это класс ошибок покрыть.

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

Повод утверждать, что таковое отсутствует - это отсутствие каких-либо результатов. Есть результаты? Нет результатов. Значит - развитие отсутствует.

Да, ебля с тестами.

При чем тут ебля с тестами? Мы сейчас говорили не о ловле ошибок, а о разработке программ (то самое «система типов нужна не только для упрощения дебага»). есть альтернативные подходы и в случае их использования система типов не только не приносит «недебажной» пользы, но и мешает.

Использование unsafe-функций a priori некорректно.

Нет, не обязательно. Если функция unsafe - значит ее _можно_ использовать некорректно, но это не значит, что некорректным будет любое использование. Например внутри бинда - оно вполне корректно.

А монадический интерфейс в хаскеле есть, называется IO.

Я в курсе. И этот интерфейс гарантирует корректность использования. Но не за счет системы типов - заметь.

А какой это дает профит?

Надо у ребят из Galois, Inc. спросить :)

Мне не надо well-typedness. Мне надо, чтобы программа работала, решала определенные задачи. От того, что я буду повторять мантру «well-typedness» у меня задачи решатся?

well-typedness = «программа не падает», если при этом, например, ты вместо pi вернёшь sin(pi) (- оба :: double), то это проблема в логике, её отлаживает тестирование, но ещё прежде этого (_до_ тестов), ты знаешь, что «программа не падает».

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

Да, lisp way - это значит, буквально, что у нас не один фиксированный язык (языки с разными системами типов - разные языки), а столько _разных_ языков (причем не DSL-ей, а общего назначения) сколько таких кусков. Та же история что и с макросами - это несколько «взрывает» сложность понимания программы за счёт того, что, смотря в конкретный код, кроме семантики языка нужно освоить и семантику макросов поднимаемых для данного кода.

И средства доказательства - свои.

Ну дык, way to go! Можно зацитировать точечные пары и натравить на них абсолютно произвольный обрабатывающий код, в том числе чекер абсолютно произвольной системы типов - метавычисления... И обвернуть это в макросы для декларативного подключения абсолютно произвольных чекеров (макросы для DSL для определения таких чекеров).

Потому что все захардкожено.

Ну да, у нас есть такой-то строго определённый язык, который использует такую-то метатеорию. Пусть кому-то не нравится SystemF как метатеория. LF или category theory - достаточные метатеории для того чтобы не привлекать сторонних построений («подключаемых типов»), но их пока невозможно использовать в ЯП общего назначения (нет таких реализаций).

Я из этого делаю совершенно очевидный вывод - а ты?

Я не понял «этого». Если бы был код в «пару строк, ... средствами альтернативными типизации» (на каком языке, в какой его реализации?), тогда можно было сравнивать с хаскелем, где unsafePerformIO активно используется и тоже так прячется за типами, что ничего сломать не может (то же про unsafeCoerce (как в safe casting из Data.Typeable) и т.п. unsafe*).

Как я и сказал - жирафы с носорогами. А вот гарантировать на уровне типов, что применение ф-и unsafePerformIO не приведет к некорректной работе - слабенькая система типов хаскеля уже не в состоянии. То есть даже такие элементарные инварианты - не в состоянии. А если говорить о чем-то более серьезном, о инвариантах, которые как раз нам на практике и хочется исполнять? То есть до тех пор пока мы находимся в смысловом поле написания факториалов - все хорошо. Но как только шаг вправо/влево - все, пропасть.

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

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

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

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

Когда ты перестанешь писать посты как говно?

А какой это дает профит?

А такой, что я знаю, что определенных ошибок в принципе быть не может. А то можно и про Си говорить. «утечака памяти? Это же очевидно как ее решить!». Но тебе же удобно, когда ты пишешь на лиспе даже не думать, о том, что какая-то там память может течь?

well-typedness = «программа не падает»

Что значит «не падает»? А если я на 0 поделю - тоже не упадет?

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

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

причем не DSL-ей

Почему же? Именно их.

Можно

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

Я не понял «этого». Если бы был код в «пару строк, ... средствами альтернативными типизации» (на каком языке, в какой его реализации?),

Я как раз про хаскель и говорю.

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

А ее не надо прятать за типами. Достаточно спрятать ее внутри >>=.

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

Чем это на практике отличаются от знания того, что вероятность встретить эти ошибки - 0.000001%?

Чем это на практике отличаются от знания того, что вероятность встретить эти ошибки - 0.000001%?

Кто тебе дает такие знания?

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

Не нужно.

пройденные тесты.

Охренеть. И как же ты узнаешь, что делает ф-я тайпкласса, если ты не знаешь, к какому инстансу она применена?

Это для адептов статики непонятно

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

Короче говоря, типичный лиспер.

Даже понятно, откуда такая лютая попаболь. Слишком высокое ЧСВ до добра не довело. Пока лисперы думали в каком же направлении им развиваться, ситуация поменялась: с одной стороны поджимает самый обычный ява-скрипт с ерлангом, с другой - Хаскель, Скала, F#. Уже выросло поколение программистов о лиспе не слышавшее ВООБЩЕ НИЧЕГО. Реализаций, как не было приличных, так и нет. Тема макрошаблонов - сугубо специфичная. Поддержка мейнстрим-технологий как была через ж..., так и осталась.

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

сделать монадический интерфейс (это как пример, на деле нам просто достаточно определить пару ф-й)

Даже не смешно. А ничего, что монадический интерфейс УНИВЕРСАЛЕН? Т.е. у очень и очень многих сущностей он присутствует, начиная от обычного Maybe.

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

Такое ощущение, что все знание о монадических интерфейсах у тебя почерпнуто из дерьмовых мануалов 7-8 летней давности, поскольку ничего кроме IO и unsafePerformIO я от тебя и не слышал.

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

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

Даже понятно, откуда такая лютая попаболь.

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

Даже не смешно. А ничего, что монадический интерфейс УНИВЕРСАЛЕН?

А вот мне как раз смешно. От того, что такой иксперт, как ты, даже не понимает, ПОЧЕМУ он УНИВЕРСАЛЕН, и что это означает.

поскольку ничего кроме IO и unsafePerformIO я от тебя и не слышал.

Наверное, потому что речь шла не о монадических интерфейсах, а, как раз, об ИО? Но это только предположение.

А если я на 0 поделю - тоже не упадет?

0 :: ?

Если ? - ADT, то не упадёт (у тебя конструктор Zero будет), если примитив (Int, Integer, ...), то деление на 0 вне стека твоего приложения (0 - терм не алг. типа, (/) - не тотальная функция). Весь стек твоего приложения («от сих до сих» + «доверяемые библиотеки») это ADT и функции с полным покрытием, там где начинается работа с примитивными не алг. типа вроде чисел или где начинается IO ты уже передаёшь управление стеку рантайма, ОС и т.д. - оно может упасть, да. То что происходит в языках для 1% процента случаев (Agda2, etc.) это как раз попытка протащить тотальность в числа, массивы, указатели, кучу и стек, IO и т.д. Но пока только академия.

то аннотации типа в хаскеле не всегда перед глазами наличествуют.

Если top-level, то всегда (правила хорошего тона), если просто видим вызов непонятной функции в коде, то всё как в C, Java и другой статике - «знаем, что за $foo» = «знаем тип $foo». В динамике - предполагаем (parse-integer - контракт string -> integer).

Почему же? Именно их.

(define foo (x) (lambda (y) (+ x y)) - обычный код на scheme, не DSL, если подключаем unrestricted систему типов - всё Ok, если linear - не проходит (линейный код свободен от GC).

А ее не надо прятать за типами. Достаточно спрятать ее внутри >>=.

А у всех функций есть типы. Ну и, как бы, с чего ты взял, что в определении >>= используется unsafePerformIO? (не использует, было уже в подобных тредах определение IO и интерфейсов, и в разных формулировках даже).

То есть когда ты прыгаешь по тредам, разбрасывая жир

Дык, батенька, если вам уже всюду заговоры мерещатся, то это не к нам. Это уже к психиатрам. Вообще, воздержитесь хоят бы не время от посещения интернета вообще, и ЛОРа в частности. Ибо, не для расшатанной нервной системы занятия сии. А то ведь нервные болезни тяжело и долго (и дорого) лечатся.

Если ? - ADT, то не упадёт (у тебя конструктор Zero будет), если примитив (Int, Integer, ...), то деление на 0 вне стека твоего приложения (0 - терм не алг. типа, (/) - не тотальная функция).

Подожди, я не понял. Твоя well-typed гарантирует, что моя программа при делении на ноль не упадет или не гарантирует? Да или нет? То есть я могу написать программу, которая все-таки упадет? Или таки не могу в принципе?

то всё как в C, Java и другой статике - «знаем, что за $foo» = «знаем тип $foo». В динамике - предполагаем (parse-integer - контракт string -> integer).

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

обычный код на scheme, не DSL, если подключаем unrestricted систему типов - всё Ok, если linear - не проходит (линейный код свободен от GC).

Ну а кто сказал, что мы систему типов переключаем какой-то там галочкой, а не использованием соответствующего этой системе типов ДСЛ?

А у всех функций есть типы.

Ну и? Можно ее и в динамике внутри бинда спрятать :)

Ну и, как бы, с чего ты взял, что в определении >>= используется unsafePerformIO?

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

Подожди, я не понял. Твоя well-typed гарантирует, что моя программа при делении на ноль не упадет или не гарантирует?

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

Целое число представляется обычно как Число = Ноль ИЛИ Следующее(Число). Т.е. число 1 будет представлено как Следующее(Ноль), число 2 как Следующее(Следующее(Ноль)). Причем, это положения не из теории типов, это самая обычная математика.

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

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

Ошибка запуска ракет в STM-транзакции подойдёт?

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

никто не выдвигал. Не увиливай.

В спецификациях - тоже.

Ещё бы.

Система типов так же не гарантирует, что ошибки НИКОГДА не будет

Она гарантирует отсутствие определённых видов ошибок. Или ты опять за своё «не ловит все ошибки, значит нафиг не надо»?

Нет результатов.

Бредишь.

есть альтернативные подходы

То есть, ебля с тестами.

система типов не только не приносит «недебажной» пользы, но и мешает.

Бредишь. QuickCheck основан именно на использовании системы типов.

Если функция unsafe - значит ее _можно_ использовать некорректно, но это не значит, что некорректным будет любое использование.

Зависит от определения слова «корректно».

Например внутри бинда - оно вполне корректно.

Опять-таки. Зависит от.

И этот интерфейс гарантирует корректность использования. Но не за счет системы типов

Здрасьте. Именно за счёт системы типов.