Функциональный апартеид

[metaclass]

http://udpn.livejournal.com/78084.html?style=mine
Обычно говорят, что нормальный порядок редукции нужен для того, чтобы bottom в аргументе не превращался в bottom в результате всегда, когда это возможно. Само по себе это никому не нужно. Дело именно в отложенном вычислении аргументов. Чтобы определить управляющие конструкции в языке с аппл. порядком редукции, нужно это делать явно, и их можно ввести только конечное число на этапе разработки языка. С нормальным порядком мы имеем возможность определять новые конструкции в любом количестве.

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

Comments

[gds.livejournal.com]

конкретно в Coq проблема останова не стоит: для любой рекурсивной функции требуется доказательство завершимости. Соответственно, никакого bottom'а не нужно.
Но разница между нормальным и аппликативным порядками остаётся.

[thedeemon.livejournal.com]

причем тут миксфикс? речь о макросах и изменении синтаксиса

[thedeemon.livejournal.com]

Another outcome of total functional programming is that both strict evaluation and lazy evaluation result in the same behaviour, in principle; however, one or the other may still be preferable (or even required) for performance reasons. (педивикия)

[tzirechnoy.livejournal.com]

Я, как человек привыкшый к тиклю и лиспу, подозреваю, что коровники плачут всё-таки по кому-то другому.

[m e (from livejournal.com)]

хорошо, а куда отправлять тех, кто высказывание понял, но не понял, что оно неверно?

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

[nivanych.livejournal.com]

Да, оптимальность по количеству "мелких редукций".
Уходить от графо-редукции необязательно, хотя и codedot, в общем-то, это сделал для своей машинки — там он может и про память говорить.
А вот задаться вопросом, можно ли осуществить такую-то нормализацию более оптимально, чем в `ленивой` модели, очень даже можно. Мемоизация, это только одна из техник оптимизации, но есть и общий подход.

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

Есличо, в посте говорится не про то, какие ленивые языки безусловно хорошие, а что если кто не понимает, что там написано, то...

[nponeccop.livejournal.com]

А там не оптимальный порядок редукции, а оптимальный sharing, по сути. Разделяется больше, чем при call by need.

[nponeccop.livejournal.com]

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

[nponeccop.livejournal.com]

> Убрать его совсем не выйдет, проблема остановки же есть.

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

[jakobz.livejournal.com]

А реально ли достаточно? Ну т.е. кто-нибудь пробовал сделать что-нибудь уровня веб-сервера с каким-нибудь TODO-списком на не тьюринг-полной какой-нибудь штуковине?

[nponeccop.livejournal.com]

Есть порт http://wiki.basho.com/Webmachine.html на AGDA2.

[measles.livejournal.com]

Калі не можаш простымі словамі растлумачыць што ты робіш — не рабі гэта. © А. Эйнштэйн.

:) Прапануеце яго эксгуміраваць і павезці купацца ў Гангу?

[aamonster.livejournal.com]

Ну да, но срабатывание всего этого "в лоб", из коробки - просто за счёт "вызова" функций...
(функция не наткнется на bottom в ненужных аргументах ~= функция не вычисляет свои аргументы раньше времени ~= можно сделать if просто функцией)
(конечно, для всех "~=" ещё куча условий, типа иммутабельности, карринга и т.п.)

[nivanych.livejournal.com]

Ну и форт, это всё-таки, метапрограммирование.

[nivanych.livejournal.com]

Правда, должен заметить, что хоть сколько-то управляемая ресурсная семантика будет ещё и сиильно покруче более непривычная, чем итераты-енумераты, к примеру.
Я так думаю. И хотел бы, чтобы мне кто-то показал, что я неправ! ;-)

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

Ну, это небольшое лукавство.
Стоит заметить, что любая программа на Тьюринг-полном языке раскладывается на составляющие —
одна составляющая проверяет, что некое вычисление не ноль и повторяет его,
вторая составляющая Тьюринг-худая, и вполне бы, достаточно просто-типа-лямбды с натуральными числами.
Но вот уж завершающейся части Agda/CoQ для второй составляющеей точно достаточно.
Например, веб-сервер не должен завершаться.
Однако, его halting problem никого не волнует ;-)
А вот один шаг (ну или некоторой ограниченное число шагов) его работы (та самая Тьюринг-худая составляющая) очень даже интересно проверить на корректность, соответствие спецификации ивсётакое.

[nivanych.livejournal.com]

Они уже выплакали свои слёзы!

[nivanych.livejournal.com]

А это уже логика второго порядка, это нечестно!

[nivanych.livejournal.com]

Кстатее, от себя добавлю, что и в агдочке тоже.

[inhate.livejournal.com]

а с не-программистами что делать будем?

[metaclass.livejournal.com]

Тестерш - в декреты!