Обычно я вижу ссылку на Referential Transparency (RT) в каком-нибудь посте по крайней мере раз в месяц в своем ежедневном троллинге блогов и форм по языкам программирования. Я думаю, что RT — вредная концепция в сообществе FP, как инкапсуляция была в сообществе OO. Вредный в том смысле, что этот термин используется для четкого технического определения, а затем используется для создания диких необоснованных заявлений, которые никоим образом не поддерживаются лежащим в основе техническим значением/определением. Короче говоря, мой язык поддерживает добро, унаследованное от X. Позвольте мне дать вам определение X. В моем языке есть X, поэтому он, очевидно, по своей сути лучше, чем языки без X. Это своего рода некритическое мышление, которое убивает реальный прогресс.
Позвольте мне внести свой вклад, чтобы остановить это, указав на некоторые истины, которые нечасто объясняют те, кто может копировать и вставлять из источников без какого-либо реального глубокого понимания или критического осмысления. Знать, что такое X, очень отличается от того, чтобы знать, является ли X хорошей или плохой вещью.
Вот довольно продвинутое использование RT, которое стало возможным благодаря нестрогости и чистоте в Haskell.
map f (map g xs) \equiv map (f . g) xs
Где \equiv означает, что выражения семантически/наблюдательно эквивалентны. Это действительно верное уравнение, верное для нестрогого языка. Подобное уравнение верно и для строгих языков, но мы должны добавить несколько ограничений, что f и g являются завершающими и не имеют наблюдаемых побочных эффектов. Я подозреваю, что наличие этих дополнительных побочных условий — это то, о чем говорят сторонники нестрогой оценки, но я не уверен, потому что это никогда толком не объясняется. При рассуждениях на языке с нестрогим вычислением побочных условий на естественные уравнения меньше. Однако рассуждать о правильности даже с побочными условиями, на первый взгляд, не так уж и сложно.
Я также отмечу, что в Haskell следующее «естественное» уравнение НЕ верно.
data Either a b = Left a | Right b (case e of A a -> A a | B b -> B b) \equiv e
Уравнение неверно, потому что выражение e может быть незавершенным выражением bottom. В правой части оператора case семантика Haskell заставит вычислить дно, что приведет к расхождению, в то время как левая сторона просто вернет невычисленное выражение без завершения, которое не расходится.
Конечно, приведенное выше уравнение верно, если мы добавим дополнительное условие, что «е» завершается, и вы получите обратно свое «естественное уравнение». Обратите внимание, что приведенное выше уравнение верно для нестрогих, нечистых языков без каких-либо побочных условий. Таким образом, эквивалентное уравнение в OCaml верно. Это демонстрирует, что некоторые «естественные» уравнения неверны в строгих языках без каких-либо раздражающих побочных условий, в то время как требуют побочных условий в нестрогих языках.
Я также могу показать вам обратное в более простой обстановке, чем в предыдущем примере карты.
fst (e1,e2) \equiv e1 snd (e1,e2) \equiv e2
Конечно, проблема снова в том, что это не прерывание. В строгих языках, если e2 расходится, первое уравнение неверно, если e1 расходится, второе уравнение неверно. В нестрогих языках независимо от расходимости выражений уравнения истинны.
Мне не ясно, что набор побочных условий, с которыми вам приходится иметь дело в строгих и нестрогих языках, существенно различается достаточно, чтобы быть проблематичным. Я также еще не видел никаких доказательств этого от сообщества Haskell. У меня есть множество свидетельств того, что люди ежедневно создают сложные системы на языках, отличных от Haskell или RT.
На самом деле, до сих пор мы говорили просто о наблюдаемой эквивалентности результатов, если вы начнете включать использование памяти в ваше определение эквивалентности. то есть to expression равны, если они вычисляют одно и то же значение и асимптически используют один и тот же объем памяти. Количество полезных эквивалентов, которые у вас есть в Haskell, по сравнению с таким языком, как OCaml, используемым для оправданной оптимизации или преобразования программы, кажется гораздо более редким в Haskell по сравнению с OCaml.
Единственный способ значительно упростить рассуждения о программировании — это исключить побочные эффекты и незавершенность. Структура монады Haskell может использоваться для обеспечения разделения между чистыми завершающими значениями и вычислениями. Тот факт, что «нижний» является допустимым значением в Haskell, является ошибкой проектирования, которая значительно усложняет рассуждения. Я не вижу тех, кто находит Haskell открывающим глаза опытом, или сообщество Haskell в целом пытается исправить это очевидное препятствие для рассуждений о программах на Haskell и четко отделить значения от вычислений. Даже если эти самые люди могут объяснить простым языком, что такое монада.
Короче говоря, я не вижу явного преимущества Haskell в рассуждениях о преобразованиях программ по сравнению с таким языком, как OCaml, как в теории, так и на практике. Я был бы рад, если бы люди объяснили мне это подробно или показали несколько примеров, выходящих за рамки Haskell. X В OCaml нет X.. поэтому Y должно быть правдой.
Чтобы добавить немного эмпирического подтверждения моим утверждениям, вы можете взглянуть на результаты ежегодного конкурса ICFP по программированию. Это далеко не контролируемый эксперимент, но если вы разделите языки, которые поддерживают ссылочную прозрачность, Haskell, и любой другой язык, вы увидите, что это явно не та особенность, которая отличает Haskell от остальных.
