То есть я могу написать программу, которая все-таки упадет? Или таки не могу в принципе?

Можно и 500V на БП подать ;) Конечно, ты можешь поделить на 0.

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

Про типы. Если перечислить ещё раз:

• Типы произведения. Ассоциативны, некоммутативны. Т.е. ведётся контроль за порядком аргументов в любом конструкторе.
• Рекурсивные типы, вместе с некоммутативностью типов произведений, обеспечивают сохранение рекурсивных структур данных - устройство списков, деревьев, графов и т.п. будет ровно таким (помимо уже гарантированного порядка аргументов при конструкторах), как это задано в рекурсивном типе.
• Типы суммы. Ассоциативны, коммутативны. Ими представляется любой набор альтернативных друг другу вариантов в пути приложения - Nothing/Just, NotNull/Null и т.п. Чекер паттерн-матчинга гарантирует, что все возможные альтернативы в пути приложения покрыты кодом.
• Каррированные функции с правилом типизации для доменов и ко-доменов. Вместе эти три составляют простейшую арифметику (или логику) типов. Она, на самом деле, фундаментальна, как ни посмотри - в той или иной форме изоморфна простейшим формам формальной логики и декартово-замкнутым категориям разного вида.
• Параметрически полиморфные типы - комбинаторы, generic программирование.
• (1-)параметрические конструкторы типов - разделение слоёв приложения которые не могут смешиваться (Either, IO, STM). Плюс переход по слоям с помощью стека монадических трансформеров.
• Классы типов - общие интерфейсы к разным ADT, наследование контекстов.

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

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

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

Как это будет выглядеть?

Попытка помирить

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

Строго говоря, «0.000001%», при условии входных данных, «похожих» на использованные при тестировании (другими словами, «нашей фантазии хватило на 10 миллионов проверок, и оно отработало правильно»). Но в случае данных с какой-ни-какой структурой, возможных вариантов больше в дофигалеф раз. Статическое доказательство ограничивает их кол-во условно правильными, т.ч. этот же «0.000001%» гораздо ближе к настоящей вероятности.

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

Нет, конечно, это снова жирафы с носорогами.

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

То есть может сложиться ситуация, когда система типов подобного профита не дает? Ну, раз необязательно?

Она гарантирует отсутствие определённых видов ошибок.

Которые ты не забыл покрыть системой типов.

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

При чем тут твой петушиный quickcheck? Еще раз - мы не о тестах.

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

При чем тут ебля с тестами? Еще раз - мы говорим о проектировании программ, а не о дебаге, хули ты в свои тесты уперся?

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

«Корректно» - это значит, что «программа работает». Никаких других определений корректности ИРЛ не используется.

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

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

Можно и 500V на БП подать

понятное дело - имелось ввиду без подобных изъебств.

Конечно, ты можешь поделить на 0.

Ну раз могу - то никаких гарантий нет, так?

В основе «хорошо-типизируемости» (как дисциплины) лежит идея использования ADT и тотальных функций с покрытием (в паттерн-матчинге) всех вариантов ADT.

Но тебе никто не гарантирует, что АДТ будут написаны так, что отловят нужные ошибки. Фактически, задача написания подобных АДТ эквивалентна задаче написания кода, в котором таких ошибок нет.

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

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

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

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

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

как обычно, ничего кроме как оскорблений ты сказать не можешь.

Как буд-то Miguel хоть в одном треде что-то кроме оскорблений сумел сказать.

Например, в этом треде.

Серьезно? Это где же?

Ну раз могу - то никаких гарантий нет, так?

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

Но тебе никто не гарантирует, что АДТ будут написаны так, что отловят нужные ошибки. Фактически, задача написания подобных АДТ эквивалентна задаче написания кода, в котором таких ошибок нет.

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

Давай будем писать ДСЛ, семантика которого естественна и ясна.

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

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

Ты так и не написал пруфа.

Давай будем писать ДСЛ, семантика которого естественна и ясна.

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

А как ты собрался обеспечивать целостность DSL? Сугубо синтаксическими мерами? Каким образом ты собираешься бороться с неверными высказываниями на этом DSL? Опять «синтаксис»?

У тебя появилась потребность объяснить другим (тем же членам команды) твой DSL. Как ты поступишь?

там весь код тотальный

и терминируемый

Это разные вещи?

Гарантий того что пользователь не захочет отстрелить себе ногу нет

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

ADT (АТД) могут быть любыми, как и код их обрабатывающий - в первом случае «кривых» ADT не может быть в принципе

Речь идет о том, что мы можем и не описать при помощи АДТ какую-то особенность данных и тогда связанные с ними ошибки отлавливаться не будут. Ну как деление на 0 в обычных арифметических ф-ях в хаскеле. То есть мы можем банально ошибиться в спецификациях. И все - программа не работает.

но тогда это может быть что угодно

В каком смысле «что угодно»?

Ты так и не написал пруфа.

банальное >>= f x = f $ unsafePerformIO x - нет?

А как ты собрался обеспечивать целостность DSL? Сугубо синтаксическими мерами?

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

У тебя появилась потребность объяснить другим (тем же членам команды) твой DSL. Как ты поступишь?

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

Это разные вещи?

К примеру, такая тотальная но не терминируемая функция:

f :: t
f = f

в хаскеле позволительна, в agda:

f : Set
f = f

приводит к такому сообщению:

You can only compile modules without unsolved metavariables or termination checking problems.

Короче, в agda в добавок к другим чекерам (types, metas) есть ещё termination checker.

Я там сказал «код только терминируемый» - это может быть и не правда (не знаю точно), но то что только тотальный и чистый (= детерминированный = отделённый от IO) это правда.

И разница между типизацией/тестами из качественной становится максимум количественной, так?

Она качественная, потому что в хаскелях такой подход можно обозвать type driven development (тоже TDD). Он предполагает, что мы форсим отношения «объекты предметной области (ОПО)» ~ «типы», «работа с такими объектами» ~ «функции», «общие для разных объектов интерфейсы» ~ «классы типов», «модульность» ~ «система модулей». То есть, в любом случае, мозги должны быть повёрнуты (или их нужно повернуть) определённым образом, но это сознательный выбор определённой парадигмы программирования. А обычное TDD (test driven development) это просто способ сразу дать определение UI и подобраться к этим самым ОПО. Такое TestDD может вполне уживаться с TypeDD и их не нужно противопоставлять (по крайней мере в случае статически-типизируемых языков). Насчёт «дать определение UI» - это основной момент. До тех пор пока мы видим, что приложение (как чёрный ящик) работает так как мы (пользователи вообще) хотим - всё хорошо. Например, веб-приложение - если оно выглядит так как нам нужно и делает то что нам нужно (чисто статистически) это значит, что «всё хорошо», _даже_ если под капотом там полно ill-typed кода. В случае динамически-типизированных языков и подобного критерия «всё хорошо» типы действительно, вроде бы, и не нужны. Но возникает вопрос - когда ОПО, наконец, прояснятся (или когда они очерчены заранее), как их «засунуть» в приложение? Обычно этой цели служит разного рода ООП - классическое (тут может случиться fail - принято начинать с классов и ими же заканчивать, если представление об ОПО изменилось, то нужно менять схему классов с одной на другую, и если на мало похожую, то, считай, нужно всё переписывать с начала), прототипное или CLOS-подобное. При этом, в случае CLOS-подобного ООП, классы и методы это (с точность до) типы (ADT) и методы в смысле хаскеля (тут описанный fail имеет меньше последствий, так как ADT реализуются отдельно, агрегация - отдельно, функции и методы - тоже отдельно, так же, как и видимость имён). Прототипный ООП тоже недалёк от модели «ADT + функции и методы», достаточно заметить, что можно добавить к ADT любого объекта поле «proto» которому присваивать объект-прототип, при применении методов на объекте не учитывать это поле, а при применении на объекте-прототипе элементарно применять на таком поле (всё сводится к определённой автоматической схеме агрегации).

Итог таков, что динамика + TestDD лучше подходят для задач с туманной спецификацией, в то время как статика + любая модель отображения ОПО в структуры языка (различные структуры данных в структурном программировании, классы в классическом ООП, классы в CLOS-подобном ООП, ADT в ML и его преемниках, ну и т.д.) - для задач с более чёткой. В этом смысле хаскель отличается от С++ только тем, что он отвергает формулу «ОПО = классы», и вводит другую - «ОПО = ADT».

В каком смысле «что угодно»?

А в каком что-то конкретное? Вот есть #lang racket и есть #lang typed/racket - просто два разных языка, и это не DSL-и (это же языки общего назначения). Других примеров нет - вроде (with-linear-typing кусок), (with-effectless-typing кусок), (with-unrestricted-typing кусок) и т.п. При этом типизация DSL-ей как раз не представляет особого интереса и её даже не трудно делать (и так делают), интерес представляет типизация _основного языка_.

банальное >>= f x = f $ unsafePerformIO x - нет?

Т.е. без типов ((>>=) с контрактом (a (a -> b)) -> b)? В этом случае unsafePerformIO = safePerformIO = id и тогда (>>=) = ($). Reductio ad absurdum :) unsafePerformIO имеет смысл только тогда, когда есть разделение на типы (forall a. a) и (forall a. IO a), в этом случае (>>=) /= ($). Короче, без типов (без разделения IO / не-IO), никакого unsafePerformIO нет и прятать нечего.

как их «засунуть» в приложение?

Ну то есть оптимальным вариантом, в итоге, была бы опциональная статика? То есть - добавляем типы, когда это можно/нужно/удобно/спецификация прояснилась и т.п. (воможно - и в самом начале, если это можно/нужно/удобно вначале)?

А в каком что-то конкретное? Вот есть #lang racket и есть #lang typed/racket

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

Других примеров нет - вроде (with-linear-typing кусок), (with-effectless-typing кусок), (with-unrestricted-typing кусок) и т.п.

Их, конечно, нет, но вот примерно они и были бы интересны. То есть если их нет - разве это значит, что их и быть не может?

Т.е. без типов ((>>=) с контрактом (a (a -> b)) -> b)?

Да можно и без контрактов, зачем контракты? Нам же надо только фиксировать применение uPIO, мы его биндом и фиксируем так, что у нас будет единственная ветка вычисления вида f1 . uPIO $ f2 . uPIO $ f3 . uPIO $ ... x и никакого другого IO нет. А значит исполнение будет корректным. То есть мы не сможем написать нечто вроде [uPIO read, uPIO read], каковое и вызывает проблемы - у нас всегда при применении IO вызывается внешний fn-враппер, который не дает зафорсить аргумент во время применения бинда. В результате вся цепь зафорсится только в main в нужном порядке - как и при обычном исполнении хаски-кода. И корректность гарантирована - хотя типов тут и не пробегало. Да, в ленивом ЯП можно return = id, uPIO = id, bind = $ и все будет работать причем без типов (у нас те же return просто тупо будут лениво откладываться до возвращения в main), в энергичном надо будет какой-то враппер типа return x = (lambda () x), uPIO f = (f).

Короче, без типов (без разделения IO / не-IO), никакого unsafePerformIO нет и прятать нечего.

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

Динамическая типизация __невыносимо__ более технологически продвинута

да-да, именно что невыносимо :)

Ну то есть оптимальным вариантом, в итоге, была бы опциональная статика?

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

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

То есть если их нет - разве это значит, что их и быть не может?

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

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

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

Для статики рантайм может быть устроен по-другому (то что сферическая статика в вакууме эффективнее такой же динамики - тоже факт)

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

Только это не статика совсем.

Ну никто это статикой и не называл.

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

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

x = uPIO read
y = uPIO read
main = return . concat $ x y

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

Да, как у SBCL. А встроенный ассемблер SBCL может быть так же эффективен как и нативный (с точностью до остановок на stop-and-copy GC), но это не отменяет того факта, что рядом висит немаленький лисповый рантайм (который больше, например, хаскельного или окамлового где-то на порядок).

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

• Гарантий ссылочной прозрачности нет (x и y не ссылочно-прозрачные, следовательно, main не ссылочно-прозрачная).
• Гарантий того, что concat не начнёт соединять ворон нет.
• Гарантий упорядоченности операций IO во времени (в соответсвии с определённой наперёд структурой кода) нет.

Короче, мы потеряли все те гарантии которые есть в haskell (одно исключение - гарантия ссылочной-прозрачности для чистых функций использующих unsafe* функции в хаскеле не автоматическая - её должен обеспечить программист, на основе того, что для данного кода она будет «очевидна», у хаскельной системы типов нет средств выявления этой очевидности). Это при том, что в динамике uPIO = id и вообще не нужен - будет у нас просто ленивая или энергичная схема, тема того как изобрести слой со ссылочной прозрачность, отделить его от слоя без таковой, осуществлять безопасный переход между этими слоями (return / uPIO) и всё это с гарантиями, но без типов... тема не раскрыта.

Динамическая типизация __невыносимо__ более технологически продвинута

Боксёр невыносимо более технически продвинут, чем кандидат наук :)

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

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

Гарантий ссылочной прозрачности нет

Нам и не надо было.

Гарантий того, что concat не начнёт соединять ворон нет.

Нам и не надо было.

Гарантий упорядоченности операций IO во времени (в соответсвии с определённой наперёд структурой кода) нет.

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

Это при том, что в динамике uPIO = id и вообще не нужен

Да с чего вдруг он id и не нужен? Следуя твоей логике в динамике вообще любая функция - id и не нужна.

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

Ну как это не раскрыта? Мы, определив бинд, безо всяких типов получили гарантии корректности кода с ИО. Так? Так. Задача решена, тема раскрыта.

Ну, во-первых - это у sbcl рантайм такой особо жирный.

http://shootout.alioth.debian.org/u64q/benchmark.php?test=all&lang=racket...

OH SHIT! Racket ещё толще! Правда там низкоуровневых хаков у рэкета вроде поменьше.

Да с чего вдруг он id и не нужен?

uPIO :: forall a. IO a -> a
uPIO (IO x) = x

return :: forall a. a -> IO a
return = IO

вот поэтому. Нет IO-обвёрток - return и uPIO просто нечего делать (не нужно оборачивать и разворачивать), (>>=) - обычная аппликация, (>>) - её частный случай.

Ну как это не раскрыта? Мы, определив бинд, безо всяких типов получили гарантии корректности кода с ИО. Так?

Т.е. из трёх инвариантов тут гарантия только одного (остальные два нам «не нужны»)? Этот один - порядок выполнения операций IO. Всю дорогу он обеспечивался тем, что prog* / begin были специальными формами с определёнными правилами трансляции. При чём тут uPIO, которого нет без типов, - короче, я потерял нить обсуждения.

Обычная последовательность операций IO в том же порядке что и последовательность энергичных вызовов это:

> ((lambda (_) ((lambda (_) (print 3)) (print 2))) (print 1))
123

> (define (bind x f) (f x))

> (bind (print 1) (lambda (_) (bind (print 2) (lambda (_) (print 3)))))
123

OH SHIT! Racket ещё толще!

что-то я не понял, о чем речь - о размере рантайма самого по себе (бинарник, тут sbcl больше на порядок) о размере чистого рантайма в оперативной памяти (неизвестно как мерить, но если просто запустить repl то 19мб racket/27мб sbcl) или о том, сколько памяти требуется приложению (не имеет отношения к рантайму вообще, существенно зависит от задачи)?

вот поэтому. Нет IO-обвёрток

Да с чего вдруг их нету-то? Это ты сам придумал, что их нет.

Т.е. из трёх инвариантов тут гарантия только одного (остальные два нам «не нужны»)? Этот один - порядок выполнения операций IO. Всю дорогу он обеспечивался тем, что prog* / begin были специальными формами с определёнными правилами трансляции. При чём тут uPIO, которого нет без типов, - короче, я потерял нить обсуждения.

Речь шла о том, как при помощи альтернативных типам средств легко и просто можно поддерживать инварианты, которые даже при помощи достаточно сильной системы типов поддержать нельзя/очень сложно. Как пример такого инварианта - консистентность исполнения сайд-эффектов в IO, который (в отличии от ряда других, более примитивных и не столь принципиальных инвариантов) в хаскеле поддерживается именно за счет синтаксиса и инкапсуляции, безо всякого использования типов. И тут вот дело в том, что «мы concat'у скормили что-то не то» - это ничего страшного. Потому что на первом же тесте грохнется, тривиально ищется и тривиально исправляется. Опечатка, по сути. И особого профита от исключения этой ошибки нет. А вот ошибку в порядке сайд-эффектов хрен отловишь, если вообще отловишь - может вылезти совершенно ВНЕЗАПНО, причем вылезет на уровне «что-то где-то поломалось». И так вот со всеми «интересными» инвариантами - система типов их не поддерживает.

При чём тут uPIO, которого нет без типов

А почему его нет без типов? Еще раз - если у нас нет типов, то, следуя твоей логике, любая функция - это просто id? То есть раз любая ф-я имеет тип a -> a, а какая функция еще может иметь такой тип... :)

Обычная последовательность операций IO в том же порядке что и последовательность энергичных вызовов это:

Не, надо так (это аналог с uPIO, где uPIO - просто форсирование санки, вообще для реализации IO лучше представлять вычисление лямбдой, которая протаскивает через себя аргументов world): (define (bind f x) (f (x)))

а у тебя вообще >> а не >>=.

что-то я не понял, о чем речь

«о том, сколько памяти требуется приложению».

Да с чего вдруг их нету-то?

Есть ADT для IO? С конструкторами и геттерами? Есть термы IO (под-термы языка, или, если угодно, под-язык)? В динамике нет параметрического типа IO :: * -> * и вообще какого-то типа IO, есть просто effectfull функции - read-integer-from-stream имеет верхний тип возвращаемого значения просто integer, никакое не (io integer) и т.п. обвёртка вокруг integer.

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

Но при этом был намёк (справедливый) только на то как организовать последовательность операций без prog* / begin - на голых лямбдах и аппликациях. Надо же - мы можем сначало открыть сокет и потом в него писать, а не наоборот, да и вообще - всё наше ИО последовательно а не перетасовывается случайным образом. Элементращина о которой даже говорить не стоит (везде IO это нечто связанное с линией времени). А вот про более интересное - отделение ссылочно-прозрачного кода от эффектного ничего сказано не было.

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

Синтаксис do - да. Инкапсуляция - параметрический *тип* IO. Интерфейс - instance Monad IO. И не отбрасываем из рассмотрения никакую из частей (а то ты сразу скажешь «IO :: * -> * не нужен, только синтаксис и интерфейс», а он нужен - нет другого средства поддерживать разделение чистого и грязного кода, функции типизированы и не-IO / IO типы при аргументах взаимоисключают друг друга).

И так вот со всеми «интересными» инвариантами - система типов их не поддерживает.

Слава богу, что она хоть что-то умеет кроме банального «{ x; y; z } выполняется в указанном порядке».

Еще раз - если у нас нет типов, то, следуя твоей логике, любая функция - это просто id?

Насчёт логики и здравого смысла - если я говорю «за опусканием типов, uPIO и return равнозначны id», то видимо я имею ввиду именно это. При чём тут вообще все остальные функции?

То есть раз любая ф-я имеет тип a -> a, а какая функция еще может иметь такой тип... :)

Я же уже написал и тип, и определение. Тип из (IO a -> a) в случае неразделения pure/unpure редуцируется до (a -> a), определение - из (uPIO (IO x) = x) сводится к (uPIO x = x), т.е. id. Тоже самое про return (в качестве упражнения, блин :)).

«о том, сколько памяти требуется приложению».

И при чем тут рантайм и динамичность?

Есть ADT для IO? С конструкторами и геттерами? Есть термы IO (под-термы языка, или, если угодно, под-язык)?

Нет. А зачем?

В динамике нет параметрического типа IO :: * -> * и вообще какого-то типа IO, есть просто effectfull функции - read-integer-from-stream имеет верхний тип возвращаемого значения просто integer, никакое не (io integer) и т.п. обвёртка вокруг integer.

С чего вдруг? (io integer) у нее (если мы говорим о реализации сайд-эффектов через io).

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

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

Синтаксис do - да.

Да нет, не синтаксис do, синтаксис бинда.

Инкапсуляция - параметрический *тип* IO.

Да не тип ИО (тип - не важен, мы можем ИО реализовать в динамике, безо всяких типов), а инкапсуляци uPIO внутри бинда, которая гарантирует корректность. Еще раз - корректность гарантируют не типы, а то, что uPIO кроме как внутри бинда нигде не используется. Так понятно?

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

Типы для этого разделения не нужны.

Слава богу, что она хоть что-то умеет кроме банального «{ x; y; z } выполняется в указанном порядке».

Так «x, y, z выполняется в указанном порядке» она как раз и не умеет, это снова тема для Ph.D (если типами выражать).

Насчёт логики и здравого смысла - если я говорю «за опусканием типов, uPIO и return равнозначны id», то видимо я имею ввиду именно это. При чём тут вообще все остальные функции?

Потому что из утверждения «за опусканием типов, uPIO и return равнозначны id» следует утверждение «за опусканием типов, любая ф-я равнозначна id». Потому что в этом плане uPIO/return ничем не отличаются от любой другой ф-и.

Тип из (IO a -> a) в случае неразделения pure/unpure редуцируется до (a -> a)

У него нет никакого типа. Вообще. Что и до чего редуцируется, собственно говоря?

определение - из (uPIO (IO x) = x) сводится к (uPIO x = x)

Не сводится. (IO x) = (lambda () x), uPIO x = (x). Вперед, своди. В качестве упражнения, блин :)

Да, как у SBCL. А встроенный ассемблер SBCL может быть так же эффективен как и нативный (с точностью до остановок на stop-and-copy GC)

Какие такие остановки, и при чём здесь эффективность ассемблера?

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

И тому есть причины.

Программа, сконпелированная SBCL, является, по-сути, SBCL с пришлёпнутым сверху твоим кодом. Выброса ненужных вещей и tree shaker'а в SBCL нет, а в том же LW после шейкера программа усыхает до нормальных размеров.

Менеджер памяти (аллокатор/сборщик мусора), применяемый в частности на x86, дюже расточительный. Особенно расточительность заметна на x86-64: минимальный чанк памяти - 16 байт. При наличии большого количества мелких объектов образ бодро вырастает 40-60 мб.

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

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

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

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

Всегда прикалывали такие чуваки. Ты что, думаешь CS - это что-то что другие дядьки делают для тебя? Нет, это то что они делают для себя. А потом - у тебя самого то какая тема была (если была вообще)?

Реализаций, как не было приличных, так и нет.

ну, строго говоря - таки есть (ACL, LW), но они стоят столько и у них такая упоротая лицензия, что - да, почитай что и нету

Итог таков, что динамика + TestDD лучше подходят для задач с туманной спецификацией, в то время как статика + любая модель отображения ОПО в структуры языка (различные структуры данных в структурном программировании, классы в классическом ООП, классы в CLOS-подобном ООП, ADT в ML и его преемниках, ну и т.д.) - для задач с более чёткой.

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

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

Ты что-то проглядел, это твои «дядьки с суровыми усами» лезут в тред и начинают срать на тему «без типов писать нельзя». Когда же ставишь вопрос ребром - какой смысл от этих ваших «типов»? То либо начинается визгливое кукареканье в стиле мигеля с занимательными эссе о сортах блевоты, либо выясняется в итоге, что уже и не все так однозначно, и вот есть задачи такие, а есть - и эдакие. Так что никаких «от повторения мантры „lisp-lisp-lisp“ программы начинают резко круче работать» нет, не было и не будет, здесь мы имеем дело с «я пишу на %lang_name% и мои программы работают, будет ли мне проще писать работающие программы, если я буду читать мантру well-typedness?». А конкретно лисп в качестве %lang_name% выбран просто в роли прямого антагониста.

Ты что, думаешь CS - это что-то что другие дядьки делают для тебя?

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

А потом - у тебя самого то какая тема была (если была вообще)?

Я не на CS учился. Дипломная была по гидродинамике океана (вихревые течения), точного названия уже, увы, не помню.

Раз мы говорим про IO - я знаю только один способ сегрегации IO от всего остального кода с предоставлением каких-то гарантий. Это monadic IO - то что принято в Haskell и Agda (на эту тему есть публикации - SPJ с соавторами и другие). И тут есть своя терминология - параметрический тип IO, конструкторы IO (IO-термы), монадический интрефейс который прячет конструкторы IO и строит всегда правильные IO-термы (засчёт правил типизации).

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

Так «x, y, z выполняется в указанном порядке» она как раз и не умеет, это снова тема для Ph.D (если типами выражать).

Да ну.

{-# LANGUAGE ExistentialQuantification #-}

import Data.Default
import Prelude hiding ( IO, putChar, getChar, putStr, putStrLn, getLine )
import Control.Applicative
import Control.Monad

-- -----------------------------------------------------------------------------
-- * IO terms.

data IO a
  = Pure a                                  -- ^ Pure value inside the IO term.
  | forall t. Show t => Write t (IO a)      -- ^ Perform a write operation.
  | forall t. Default t => Read (t -> IO a) -- ^ Perform a read operation.

-- -----------------------------------------------------------------------------
-- * Functorial, applicative and monadic interfaces for IO.

instance Functor IO where
  fmap f (Pure x)    = Pure $ f x
  fmap f (Write z x) = Write z $ fmap f x
  fmap f (Read g)    = Read $ \z -> fmap f $ g z

instance Applicative IO where
  pure  = return
  (<*>) = ap

instance Monad IO where
  return          = Pure
  Pure x    >>= f = f x
  Write z x >>= f = Write z $ x >>= f
  Read g    >>= f = Read $ \z -> g z >>= f

-- -----------------------------------------------------------------------------
-- * Run for IO (a.k.a. unsafePerformIO).

class Run t where
  run :: t a -> a

instance Run IO where
  run (Pure x) = x
  run (Write _ x) = run x
  run (Read g) = run $ g def

-- -----------------------------------------------------------------------------
-- * Pretty printer for IO.

instance Show a => Show (IO a) where
  show (Pure x)    = show x
  show (Write z x) = "write handle " ++ show z ++ "\n" ++ show x
  show (Read g)    = "read handle buffer\n" ++ show (g def)

-- -----------------------------------------------------------------------------
-- * Basic IO functions. Characters and strings.

instance Default Char where
  def = '*'

putChar :: Char -> IO ()
putChar x = Write x $ return ()

getChar :: IO Char
getChar = Read return

putStr :: String -> IO ()
putStr = mapM_ putChar

putStrLn :: String -> IO ()
putStrLn xs = putStr xs >> putChar '\n'

getLine :: IO String
getLine = do
  c <- getChar
  if c == '\n'
  then return [c]
  else fmap (c :) getLine

getNLine :: Int -> IO String
getNLine n
  | n <= 0 = return ""
  | otherwise = do
    c <- getChar 
    fmap (c :) $ getNLine (n - 1)

Тут только ленивый код. На монадический интерфейс (скрытый за do-сахаром) накладывается обязанность построить правильный IO терм:

test :: IO ()
test = do
  name <- getNLine 5
  putStrLn $ "Hi, " ++ name

*Main> test
read handle buffer
read handle buffer
read handle buffer
read handle buffer
read handle buffer
write handle 'H'
write handle 'i'
write handle ','
write handle ' '
write handle '*'
write handle '*'
write handle '*'
write handle '*'
write handle '*'
write handle '\n'
()
*Main> run test
()
*Main> run getChar
'*'

test имеет тип IO (), это просто некий терм, и видно (за счёт pretty printer), что никаких проблем с тем чтобы операции IO были в правильном порядке нет. Компилятору остаётся только подхватить IO терм и превратить его в удобную для VM форму (аллоцировать буфер, расставить адреса, заменить read/write на нужные системные вызовы и т.п.).

«за опусканием типов, uPIO и return равнозначны id» следует утверждение «за опусканием типов, любая ф-я равнозначна id»

[Я спокоен, я спокоен :)] Т.е. ты считаешь, что функция с определением (f (Con x) = x) и функция с определением (f' x = Con x) и вообще любая функция g это одно и тоже (а мы рассматриваем переход, когда конструкторы Con исчезают, т.е. когда пропадает разделение inside/outside IO).

Программа, сконпелированная SBCL, является, по-сути, SBCL с пришлёпнутым сверху твоим кодом.

А программа, собранная gcc, является по сути libc с пришлёпнутым сверху моим кодом. Разница, конечно, есть - в libc нет компилятора.

Выброса ненужных вещей и tree shaker'а в SBCL нет, а в том же LW после шейкера программа усыхает до нормальных размеров.

Лучше бы они делали lisprt.so и умели нормальную раздельную компиляцию в ELF-ы. ELF приложения может вызвать start из .so рантайма, тот запустит главную функцию приложения, но до этого настроит треды и сигналы GC. Тогда в памяти будет висеть только одна версия рантайма. При этом классический подход с образами и разными рантаймами тоже можно использовать - достаточно собрать приложение статически.

Раз мы говорим про IO - я знаю только один способ сегрегации IO от всего остального кода с предоставлением каких-то гарантий. Это monadic IO - то что принято в Haskell и Agda (на эту тему есть публикации - SPJ с соавторами и другие). И тут есть своя терминология - параметрический тип IO, конструкторы IO (IO-термы), монадический интрефейс который прячет конструкторы IO и строит всегда правильные IO-термы (засчёт правил типизации).

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

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

Любая реализация монады IO в динамическом ЯП. Ну вот, например: http://dorophone.blogspot.com/2011/11/understanding-haskell-io-monad.html Типов нет? Нет. Все работает? Работает. Написать ппрограмму с некорректным порядком сайд-эффектом, используя бинд, принципиально невозможно. И дело не в типах - дело в определении бинда.

Да ну.

Ну да. Вот у меня есть ф-я uPIO, которая форсит вычисление. Теперь напиши мне для нее тип такой, чтобы я не мог при использовании uPIO получить неоднозначность/некорректность в исполнении сайд-эффектов типа [uPIO gechar, uPIO getchar] (то есть вышеприведенный код не должен быть тайпчекнут). Жду реализации.

Тут только ленивый код. На монадический интерфейс (скрытый за do-сахаром) накладывается обязанность построить правильный IO терм:

Нет, не так. Монадический интерфейс ИО так определен (вне зависимости от типов), что некорректный ИО-терм за счет применения бинда просто _не может быть построен_. Не важно какой тип ты присвоишь бинду. Результат применения бинда - всегда корректный ИО-терм. Какой бы тип ты не подставил. Строить некорректный терм бинд просто не умеет :) То есть в приведенном тобой коде корректность ИО лежит исключительно на монадическом интерфейсе, а типы - по боку. Гарантировать корректность сайд-эффектов система типов хаскеля не может никак (нельзя для uPIO присвоить нужный тип).

test имеет тип IO ()

А тип ни на что не влияет тут.

что никаких проблем с тем чтобы операции IO были в правильном порядке нет.

Но типы опять ни на что не повлияли и ничего не гарантировали :)

Т.е. ты считаешь, что функция с определением (f (Con x) = x) и функция с определением (f' x = Con x) и вообще любая функция g это одно и тоже

Это не я так считаю - это ты так утверждаешь :)

(а мы рассматриваем переход, когда конструкторы Con исчезают, т.е. когда пропадает разделение inside/outside IO).

Почему исчезают? Куда они исчезают? Конструктор - это просто функция. Если мы убрали из ЯП систему типов, то семантика ф-й никак не меняется, и если ф-я Con != id с типами, то Con != id и без типов. По-этому return x = IO x != id хоть с типами хоть без.

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

Вот, кстати, тоже не совсем правда - на основе return/bind можно написать lift-еры.

И вместо такого:

> (string-append (read) (read))
"123"
"456"
"123456"

(повезло? или оно и должно слева направо вычисляться?).

В хаскеле будет:

> liftM2 (++) getLine getLine
123
456
"123456"

или так:

import Control.Monad

class Identity t where
  e :: t

class Identity t => Monoid t where
  (∘) :: t -> t -> t

{-# RULES
"Left/Identity/Monoid"  forall f. e ∘ f = f
"Right/Identity/Monoid" forall f. f ∘ e = f
"Monoid"                forall f g h. f ∘ (g ∘ h) = (f ∘ g) ∘ h
  #-}

instance Identity [a] where
  e = []

instance Monoid [a] where
  (∘) = (++)

instance (Identity a) => Identity (IO a) where
  e = return e

instance (Monoid a) => Monoid (IO a) where
  (∘) = liftM2 (∘)

и тогда:

> "123" ∘ "456"
"123456"
> e ∘ "123" ∘ "456" ∘ e
"123456"
> getLine ∘ getLine
123
456
"123456"
> e ∘ getLine ∘ e ∘ getLine
123
456
"123456"

Ну а то что применение лево-ассоциативно это фундаментальное свойство каррированных функций.

Ты упорно не хочешь понимать, что для реализации монад (и ИО в том числе) типы _не нужны_.

Ну да, я не вижу никакого смысла в монадах и отдельном IO в динамических языках - там и без них прекрасно живётся. Почему? Потому что если нет типов и выделения IO, то (>>=) = flip ($), return = uPIO = id. Так что серьёзно смотреть на все эти реализации монад в CL и Racket я не могу (нафига монады? интерфейс к чему, если термов IO нет? какой return и bind если оборачивать не во что и есть обычная динамическая аппликация?).

Монадический интерфейс в частности и выделенное IO вообще нужны только в pure языках - в таких языках этот подход, собственно, и возник.

Типы в построении правильных ИО-термов никак не участвуют.

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

Но я кажется понял, ты говоришь именно о том, что можно написать интерпретатор IO с функций run (без типов). Т.к. есть макросы можно даже написать компилятор IO (тоже без типов, но с неким DSL задаваемым case-ми макросов). При этом run (аналог uPIO, но уже вполне safe) будет полностью законным, т.к. за ссылочно-прозрачный код трястись не надо.

Жду реализации.

Я не понял, в моём стандарте нет никакого uPIO, если что :)

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

я не про данный тред, а пр общую тенденцию, есличо

Когда же ставишь вопрос ребром - какой смысл от этих ваших «типов»?

ну тут первый, и очевидный, ответ - тупо быстрее работает

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

Ты не совсем понял мой поинт.

как раз понял, но он неверен имхо

Я говорил о том, что, все же, развиваемые темы _в общем_ хоть несколько должны отражать и требования отрасли,

фигасе :) если отрасль хочет - она финансирует (чай не бедная), раз такого не происходит - значит не особо то и хочет, ну или её и так устраивает всё

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

на то она и наука, чтобы исследовать всяку неведому хухню с серьёзным видом :)

Опять у lovesan'а баззворд-понос.

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

Тысячам энтерпрайз приложениям на java и C++ посрать на твои комбинаторы.

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

Ну ё-моё, как маленький, честное слово.

newtype Y a = Y {(|$) :: Y a -> a};
y = let z w f = f $ (w |$ w) f in Y z |$ Y z

Всё. Ушёл.

Тысячам энтерпрайз приложениям на java и C++ посрать на твои комбинаторы.

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

; fixed for the greater good

это не настоящий. Настоящий это лямбда. Безымянная. В этом и фишка. И к тому же, работает не с a->a, а с *->*

вот Z например:

(lambda (f)
  ((lambda (x) (funcall f (lambda (y) (funcall (funcall x x) y))))
   (lambda (x) (funcall f (lambda (y) (funcall (funcall x x) y))))))

lovesan

Настоящий это лямбда. Безымянная. В этом и фишка.

Уговорил.

newtype Y a = Y {(|$) :: Y a -> a}
y = \h -> let z w f = f $ (w |$ w) f in (Y z |$ Y z) h

Легче?

И к тому же, работает не с a->a, а с *->*

Частный случай, при a=*.

Уговорил.

Это как бы подтверждение моих слов, да?
Все понятно.

Частный случай, при a=*.

Сказки то не рассказывай.

Это как бы подтверждение моих слов, да?

Смотря каких. Ты просил лямбду — получи и распишись.

Сказки то не рассказывай.

Какое слово не понятно?