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

[metaclass]

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

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

Comments

[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. в некоторых местах он при экстракции в окамл использует лентяйку, сходу помню экстракцию всяких коиндуктивных типов данных и работу с ними. Вот тут мне надо было бы толком разобраться, почему там лентяйка, а то понятно только интуитивно, но никак не чётко.