Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Categories:

За что мы любим лень

Вынес из комментов

TL;DR: я тут сформулировал две киллер-фичи ленивости, невидимые из-за Blub paradox

Фича I - инвариантность control flow относительно бета-конверсии
Фича II - вместо двух разных версий у нас один и тот же код для данных и коданных

> Ленивые вычисления нужны, вроде как, для того, чтобы о
> порядке вычислений не думать (любой нормализуемый терм
> будет нормализован).

Учоныи (не путать с учёными) дали нам бесполезные ввиду своей слабости гарантии: любой терм будет нормализован на машине Тьюринга (у физ.компа закончится память) за конечное (но не ограниченное!) время, потребив конечное (но не ограниченное!) количество ресурсов.

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

Совсем другое дело, что нам гарантируется производительность не хуже нормальной стратегии.

1) В частности, гарантируется, что соптимизированный код не зайдёт в те ветки, в которые не заходит нормальная стратегия.

2) Гарантируется, что потребление кучи данными и санками будет не хуже.

То есть, де факто программист ОБЯЗАН считать порядок вычислений прибитым гвоздями к нормальному.

И написание foldl без ' и ! является ОШИБКОЙ переносимости "зависимость от деталей реализации компилятора" (на практике это не очень заметно - разве что есть риск что ВНЕЗАПНО при смене версии компилятора что-то оптимизироваться перестанет)

Тем не менее, мы любим ленивость как раз за первую подгарантию. Из которой следует, что бета-конверсия в обе стороны нам ничем не грозит (с практической т.з. - теоретически есть казусы вроде незамкнутости системы типов Haskell98/2010 относительно бета-экспансии).

Из чего, в свою очередь, следует

1а) минимальный смысловой и лексический оверхед на бета-абстракцию (в строгом языке приходится дополнительно гадить семантическим мусором defer/force - т.е. де факто "экстрактить повторяющийся контрол флоу? нахуй-нахуй, пишем как в сях, разве что вместо одного while пара библиотечных фолдов, лапша в 1-2 строки лапшой не считается")

1б) абсолютнейшая лёгкость рефакторинга

1в) значительное повышение пользы от библиотек абстракций управления (в частности, почти никогда не нужно отдельных версий функций - для данных и для коданных)

Фича I - это более сильное свойство, чем чистота. Чистота всего лишь гарантирует, что бета-конверсия сохраняет big step semantics, что не имеет физ. смысла. Здесь же гарантируется абсолютное потребление ресурсов - с точностью до оверхеда бета-редукции в рантайме.

Фича II является своего рода аналогом гомоиконности - данные можно хранить в конструкторах, в функциях (в санках), в катаморфизмах (кодировка Чёрча), причём все три способа первоклассные и почти полностью эквивалентны. О практической пользе экзотических представлений надо отдельно писать.
Tags: fp, programming
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 16 comments