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

[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]

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

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

[theiced.livejournal.com]

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

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

[gds.livejournal.com]

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

[metaclass.livejournal.com]

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

[theiced.livejournal.com]

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

[wizzard]

Ну да, там другие слова нужны. Futures, leases, intercession и т.д. Линейные типы самую малость помогают, но их недостаточно.

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

[juan-gandhi.livejournal.com]

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

[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. Попробую на досугѣ.

[zelych.livejournal.com]

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

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

Go

[occurs-check.livejournal.com]

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

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

[juan-gandhi.livejournal.com]

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

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

[nivanych.livejournal.com]

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

[valentin budaev (from livejournal.com)]

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

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

[zelych.livejournal.com]

Понятно, спасибо.
А если это что-то, что доступно через свободные переменные, всегда referentially transparent, то даже со свободными перменными функция будет всегда чистой?

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, но своей простотой привлекает широкие массы.

[thedeemon.livejournal.com]

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

Re: What is a Purely Functional Language?

[thedeemon.livejournal.com]

Спасибо!

[valentin budaev (from livejournal.com)]

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

[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 и сохранить или не сохранить чистоту там как раз показывается.

[lomeo.livejournal.com]

Не совсем, в ленивом выразить энергичность проще, чем в энергичном ленивость:
http://thesz.livejournal.com/906786.html

[nivanych.livejournal.com]

> Как добавить ++i и сохранить или не сохранить чистоту
Можно и Java запихать внутрь лямбды.
И сказать, что получили формально чистый язык.
Но всё-таки, если у нас торчит глобальное состояние, ну нельзя это называть чистым языком. Да и слишком будет отличаться от любой из классических лямбд.
Короче говоря, мне непонятно, почему это можно называть чистым.
Лучше почитаю, что там написано, чем лишние вопросы задавать.

[valentin budaev (from livejournal.com)]

Если надо заделеить аргумент - его надо делеить по всему стеку вызовов _вниз_, до упора. Если надо зафорсить аргумент - его надо форсить по всему стеку вызовов _вверх_, до упора, опять. Здесь совершенно строгая дуальность, в смысле двойственной категории. Ну а thesz в своем стиле просто сделал важное умолчание :)