Не нарушает ли существование rseq/seq ссылочную прозрачность? Есть ли альтернативные подходы, которые этого не делают?

Question

Я всегда думал, что заменить выражение x :: () с () :: () будет одной из самых основных оптимизаций при компиляции программ на Haskell. поскольку () имеет одного жителя, независимо от того, что x есть результат (), Эта оптимизация показалась мне значительным следствием ссылочной прозрачности. И мы могли бы сделать такую ​​оптимизацию для любого типа только с одним жителем.

(Обновление: мои рассуждения в этом вопросе основаны на естественных правилах вывода. Там тип единицы соответствует истине (⊤), и у нас есть правило расширения "если x : ⊤ затем () : ⊤". Например, см. Этот текст на стр. 20. Я предположил, что можно безопасно заменить выражение его расширением или контрактом.)

Одним из следствий этой оптимизации будет то, что undefined :: () будет заменен () :: (), но я не вижу в этом проблемы - это просто сделает программы немного ленивее (и полагаться на undefined :: () это конечно плохая практика программирования).

Однако сегодня я понял, что такая оптимизация сломается Control.Seq полностью. Strategy определяется как

type Strategy a = a -> ()

и у нас есть

-- | 'rseq' evaluates its argument to weak head normal form.
rseq :: Strategy a
rseq x = x `seq` ()

Но rseq x :: () поэтому оптимизация просто отбросит требуемую оценку x на WHNF.

Так в чем же проблема?

• Есть ли существование rseq а также seq нарушить ссылочную прозрачность (даже если мы рассматриваем только завершающие выражения)?
• Или это недостаток дизайна Strategy и мы могли бы придумать лучший способ, как заставить выражения для WHNF совместимы с такими оптимизациями?

Answer 1

Ссылочная прозрачность - это утверждения о равенстве и ссылки на переменные. Когда вы говорите x = y и ваш язык прозрачен по ссылкам, вы можете заменить каждый вхождение x на y (по модулю области видимости).

Если вы не указали x = ()тогда ты не сможешь заменить x от () безопасно, как в вашем случае. Это потому, что вы не правы насчет жителей ()потому что в Haskell их два: один является единственным конструктором ()а именно (), Другое - это значение, которое никогда не рассчитывается. Вы можете назвать это нижней или неопределенной:

x :: ()
x = x

Вы, конечно, не можете заменить любое вхождение x от () здесь, потому что это будет шанс семантики. Существование дна в языковой семантике допускает некоторые неловкие крайние случаи, особенно когда у вас есть seq комбинатор, где вы можете даже доказать каждую монаду неправильно. Вот почему для многих официальных обсуждений мы игнорируем существование дна.

Однако ссылочная прозрачность от этого не страдает. Haskell по-прежнему прозрачен по ссылкам и как таковой является чисто функциональным языком.

Answer 2

Ваше определение ссылочной прозрачности неверно. Ссылочная прозрачность не означает, что вы можете заменить x :: () с () :: () и все остается прежним; это означает, что вы можете заменить все вхождения переменной на ее определение, и все останется прежним. seq а также rseq не противоречат ссылочной прозрачности, если вы используете это определение.

Answer 3

seq здесь красная сельдь

unitseq :: () -> a -> a
unitseq x y = case x of () -> y

Это та же семантика, что и seq на юнит и не требует магии. По факту, seq имеет что-то "волшебное" только при работе с вещами, с которыми вы не можете сопоставить паттерны - то есть с функциями

Замена undefined :: () с () имеет те же вредные последствия с unitseq как с более волшебным seq,

В целом, мы думаем о ценностях не только как о том, "что" они, но как они определены. С этой точки зрения должно быть понятно, почему мы не можем осуществлять преобразования, определяющие определенность, так или иначе.

Answer 4

Спасибо всем за вдохновляющие ответы. Подумав об этом больше, я прихожу к следующим взглядам:

Представление 1: Рассматривая только завершающие выражения

Если мы ограничимся нормирующей системой, то seq (или же rseq и т. д.) не влияет на результат программы. Это может изменить объем памяти, который использует программа, и увеличить время процессора (вычисляя выражения, которые нам на самом деле не нужны), но результат остается тем же. Так что в этом случае правило x :: () --> () :: () допустимо - ничего не теряется, процессорное время и память могут быть сохранены.

Вид 2: изоморфизм Карри-Говарда

Поскольку Haskell полон по Тьюрингу, и поэтому любой тип населён бесконечным циклом, соответствующая логическая система CH непоследовательна (как указал Витус) - все может быть доказано. Так что на самом деле любое правило допустимо в такой системе. Это, наверное, самая большая проблема в моем первоначальном мышлении.

Вид 3: Правила расширения

Естественные правила вычета дают нам сокращения и расширения для операторов разных типов. Например для -> это β-сокращение и η-расширение, для (,) это

fst (x, y) --reduce -> x (и аналогично для snd)

x : (a,b) --expand -> (fst x, snd x)

и т. д. При наличии дна правила сокращения все еще допустимы (я считаю), но правила расширения нет! В частности, для ->:

rseq (undefined :: Int -> Int) = undefined

но это п-расширение

rseq (\x -> (undefined :: Int -> Int) x) = ()

или для (,):

case undefined of (a,b) -> ()

но

case (fst undefined, snd undefined) of (a,b) -> ()

и т.д. Таким же образом, правило расширения для () не допустимо

Вид 4: Ленивое сопоставление с образцом

позволяющий x :: () расширить до () :: () может рассматриваться как особый случай принудительного сопоставления всех шаблонов в типах данных с одним конструктором. Я никогда не видел, чтобы ленивое сопоставление с образцом использовалось в типе данных с несколькими конструкторами, поэтому я считаю, что это изменение позволило бы нам избавиться от ~ ленивый образец, соответствующий символу полностью. Однако это изменило бы семантику языка на более ленивый (см. Также комментарий Дэниела Фишера к этому вопросу). И более того (как описано в вопросе) перерыв Strategy,