О чистоте и нечистотах

[thedeemon]

Уважаемый thesz написал у себя:
Для чистоты требуется 1) нормальный порядок упрощения (call-by-need или call-by-name, чтобы убрать зависимость от порядка вычисления) и 2) типы, чтобы ++i не пролезло в чистый код.
но, кажется, перепутал чистоту с хаскелем.

Ибо: 1) есть замечательный чистый функциональный язык Idris (даже проверяемо тотальный большей частью), в котором порядок вычислений строгий. Т.е. я бы заметил, что call-by-need требует чистоты, но чистота в общем случае не требует call-by-need.
То, что "есть классы программ, которые в нормальном порядке выразимы, в энергичном нет" - это правда, конечно, но к чистоте отношения не имеет.
Касательно 2) - бестиповое лямбда-исчисление тоже совершенно чистое, и для чистоты своей типов не требует. Чтобы ++i не пролезло в чистый код таки достаточно убрать из языка ++i и другие нечистоты.

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

Comments

[nivanych.livejournal.com]

> четкого определения чистоты

Всё, что записано в какой-нибудь из лямбд — чистое.

[nivanych.livejournal.com]

Можно ещё чуть не так сказать — всё, что описано определёнными 'сортами' интуиционистских логик.
Если добавить всякие ++i в язык, нууу, вряд ли это кто назовёт "лямбдой". Какой-то глобальный State можно, конечно, но типы будут "немного" специфическими.
Правила редукции тут вообще ни к чему.
Хотя и конечно, могут быть и такие правила, когда вообще ничего не вычислится ;-)

[thedeemon.livejournal.com]

Тут рядом дали ссылку на манускрипт по теме. Там так предлагают определять purely functional language:
1. Он включает в себя simply typed lambda calculus.
2. Для него реализованы call-by-value, call-by-name и call-by-need вычисляющие Функции, и
3. Эти реализации weakly equivalent (когда если одна возвращает нечто, то другая или возвращает то же самое, или не определена).

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

Как добавить ++i и сохранить или не сохранить чистоту там как раз показывается.

[theiced.livejournal.com]

1. ни разу не уважаемый
2. хаскелисты - они такие, да

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

[gds.livejournal.com]

первый твой камент, с которым я согласен по всем пунктам.

[metaclass.livejournal.com]

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

[theiced.livejournal.com]

да как его не решай - зависимые типы от отгнивания сети никак не защищают.

[thesz.livejournal.com]

>Придут псы, сделают alter table и вся чудесная статически типизированая прога сдохнет.

И что, есть опыт? И программа на Хаскеле была? Или это художественное преувеличение, как обычно?

[juan-gandhi.livejournal.com]

Понравился последний вопрос.
Она чистая в одной категории, и нечистая в другой.

[zelych.livejournal.com]

Это про λ-исчисление? Можно чуть подробнее?

[juan-gandhi.livejournal.com]

Это про свободные переменные.

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

[chaource.livejournal.com]

А вотъ посовѣтуйте. Я понемногу знаю ML, Haskell, Coq, Scala. Стоитъ ли тратить время на изученiе и попытки использовать Idris для реальныхъ задачъ? Примѣръ реальной задачи - сдѣлать небольшой вебъ-серверъ съ небольшой локальной базой данныхъ и нехитрыми функцiями (сгенерировать въ html списокъ результатовъ поиска по БД, обновить БД, или запустить внѣшнюю программу и распарсить STDOUT, полученный отъ нея). Причемъ мнѣ хотѣлось-бы рѣшать эту задачу "съ пользой", т.е. одновременно изучая какой-то новый языкъ или парадигму. Вы бы посовѣтовали дѣлать это на Haskell/Yesod, Scala/Scalatra, SML, OCaml, Idris, Agda?

[thedeemon.livejournal.com]

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

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

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

[chaource.livejournal.com]

Спасибо за совѣты! Вотъ Haskell/Yesod выглядитъ какъ такой добротный full-service framework, эдакой Haskell On Rails. Попробую на досугѣ.

[nivanych.livejournal.com]

> Для реальных задач Idris я не советую

А ты его трансляцию в джавоскрипт не пробовал, как оно?

What is a Purely Functional Language?

[occurs-check.livejournal.com]

"Functional programming languages are informally classified into _pure_ and _impure_ languages. The precise meaning of this distinction has bett a matter of controversy. We therefore investigate a formal definition of purity."

http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps

Re: What is a Purely Functional Language?

[thedeemon.livejournal.com]

Спасибо!

Go

[occurs-check.livejournal.com]

> Так и будут на Goвне всяком продолжать.

Это вы не туда смотрите, когда думаете такое про Go (понимая Go как язык+компилятор+спек_на_стдлибу+либы). Надо смотреть на него не с точки зрения CS & PLT, а с точки зрения "современной практичной замены Си для ширнармасс", и он уже вполне нашел свою нишу для серверного и административного софта: Docker (www.docker.com), например, написан целиком на Go. Go позволяет делать маленькие статические бинарники без зависимостей (и задачи типа вашей недавней про маленькую гуявую апп тоже будет можно на нем решать, когда ему приделают гуй ;)) А ещё у него typed CSP-style interthread communication, очень неплохо, и перспективный подход к ООП (оно явно некоторе время ещё не сойдет в могилу, так что пусть лучше уж так.)

Re: Go

[thedeemon.livejournal.com]

Да, я в курсе. Однако перенесу свой коммент с реддита:
Noticed the trend? People marching to Go come mostly from Node.js, Python and some other languages for intellectual majority simplistic languages. It's like switching from cheeseburgers to BigMacs. You'll have some more lettuce but it's still junk food. You won't see many people switching to Go from languages like Haskell, Scala or Erlang.

Go - это такой JS в мире Си-подобных. Как язык полное Vno, но своей простотой привлекает широкие массы.

[valentin budaev (from livejournal.com)]

> То, что "есть классы программ, которые в нормальном порядке выразимы, в энергичном нет" - это правда

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

[thedeemon.livejournal.com]

Конкретный выбор слов в той фразе может быть не идеальный, но я думаю, понятно, что имелось в виду. Как пример Сергей любит приводить описание своих конструкций вроде if, unless и подобных, которые в строгих языках приходится делать частью языка (или сильно приседать с макросами), а в ленивых это простые функции получаются.

[ddzhus.ya.ru (from livejournal.com)]

> 2) типы, чтобы ++i не пролезло в чистый код.

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

> бестиповое лямбда-исчисление тоже совершенно чистое

Пример бессмысленный, так как в нём и эффектов нет.

[valentin budaev (from livejournal.com)]

> Пример бессмысленный, так как в нём и эффектов нет.

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

[geniepro.livejournal.com]

В тотальном ФП не имеет значения -- энергичные вычисления или ленивые, результаты они дают одинаковые.

[thedeemon.livejournal.com]

Да. Автор Идриса так и объясняет выбор: если результат одинаковый, а о потреблении ресурсов рассуждать проще, нафига тут ленивость?