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

[metaclass]

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

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

Comments

[gds.livejournal.com]

+1. А вот в Coq, где синтаксис расширяется отнюдь не через подобные функции, а через более правильный механизм Notations, вполне делается do-нотация.
И в окамле подобное решается без лентяйки -- достаточно написать camlp4-расширение (или, с новым подходом, который уже в транке, но ещё не в релизе, всего лишь функцию на 20 строк, что ещё проще).

[udpn.livejournal.com]

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

[gds.livejournal.com]

нет, это не просто другая запись функций. (иначе как бы я сделал do-нотацию? там же явно требуется "a <- b" транслировать в "b >>= fun a -> ...")
Ну и вот, чтобы не быть голословным, покажу няшечьку: http://paste.in.ua/4459/ -- судя по коду, который экстрактится в окамл, вычисляется только одно из выражений.

[udpn.livejournal.com]

Здесь я, похоже, слился, потому что Сoq видел полтора раза в жизни. Это там в Notation вставка ML'я? Как это сказывается на корректности программ? Сам Coq-то ленивый?

[gds.livejournal.com]

в Notation -- вставка того же Coq'а. Символы cond/th/el -- выражения, они не обязаны быть значениями и не обязаны вычисляться, они просто подставляются, почти синтаксически. На корректности сказывается как любой другой Coq код.
В do-нотации, если по памяти, у меня было как-то так: Notation "a <- b ;; c" := "bind (fun a => c) b", то есть, "a" рассматривается как идентификатор, и везде, где используется эта нотация, данное ограничение учитывается.
Сам Coq -- скорее строгий. Впрочем, 1. касаемо доказательств и редукций: есть тактики для ленивой работы с пруф-термами, для ленивой редукции, 2. в некоторых местах он при экстракции в окамл использует лентяйку, сходу помню экстракцию всяких коиндуктивных типов данных и работу с ними. Вот тут мне надо было бы толком разобраться, почему там лентяйка, а то понятно только интуитивно, но никак не чётко.

[thedeemon.livejournal.com]

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