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

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

[nivanych.livejournal.com]

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

[thedeemon.livejournal.com]

Ну вот хацкель с его монадами - чистый или нет? А Clean?

[nivanych.livejournal.com]

Прочитал. Пожалуй, согласен с аффтарами.