Что произойдет, если вы скомпилируете программу, которая не требует ввода? (Вопросы чистоты Haskell IO (снова))

Question

putStrLn при вызове с любыми аргументами всегда будет возвращать значение типа IO (). Я согласен, это чисто, я могу справиться с этим. Но действительно ли это прозрачно? Я так думаю, потому что для любого заданного ввода вы могли бы заменить вызов функции на IO (), который выкинул бы правильную строку в стандартный вывод.

Так что я крут с putStrLn, но getLine при вызове без аргументов может вернуть любое количество вещей, если они имеют тип IO String. Это не является ни чистым, ни ссылочно-прозрачным, верно?

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

Это поднимает еще один вопрос для меня. Достаточно ли умен компилятор для распознавания программы, которая не требует ввода? Например, скажу, что я компилирую

main = putStrLn . show $ map (+1) [1..10]

Достаточно ли умен GHC, чтобы сократить эту программу до IO (), что приводит к распечатке [2,3,4,5,6,7,8,9,10,11]? Или это все еще решает и оценивает / выполняет все во время выполнения? То же самое касается произвольных программ, где ввод не требуется. Использует ли GHC тот факт, что вся программа прозрачна по ссылкам и может быть просто заменена ее значением?

Answer 1

Да, эти монадические функции прозрачны по ссылкам, поскольку к ним все еще применяется правило подстановки.

В Haskell следующие две программы эквивалентны

main = (puStrLn "17" >> puStrLn "17")
main = let x = putStrLn "17" in (x >> x)

На "нормальном" языке второй пример будет напечатан только один раз, как побочный эффект оценки x. То, как эти две программы на самом деле одинаковы, становится немного понятнее, когда вы понимаете, что значение типа IO() на самом деле не является побочным эффектом, а на самом деле является описанием такого вычисления , которое вы можете использовать как строительный блок для построения больших вычислений из.

Answer 2

Я думаю, что здесь есть два вопроса.

1. Является ли IO ссылочно-прозрачным
2. Сократит ли GHC произвольные выражения во время компиляции

Глядя наТип IO, вы можете себе представить, что он эмулирует ссылочную прозрачность, полагаясь на таинственное значение RealWorld, которое не имеет конструктора данных, и заставляя каждое выражение зависеть от последнего (в однопоточном мире).В случае IO String это оболочка нового типа вокруг RealWorld -> (RealWorld, String) ... которая является функцией, а не значением.Использование IO без экземпляра Monad делает это особенно и мучительно очевидным.

Prelude GHC.Types> :info IO
newtype IO a
  = IO (GHC.Prim.State# GHC.Prim.RealWorld
        -> (# GHC.Prim.State# GHC.Prim.RealWorld, a #))

Что касается оптимизации GHC, в этом случае он не сокращает список до строки во время компиляции.Оптимизированный код, созданный GHC 7.2.1, лениво генерирует список, сопоставляет (+1) с результатами, преобразует список в строку и, наконец, выводит его на консоль.Почти так же, как в вашем примере.

Answer 3

getLine :: IO String чисто;его значением является действие ввода-вывода, которое читает и возвращает * строку из стандартного ввода.getLine всегда равно этому значению.

* Я использую здесь слово «возврат» из-за отсутствия лучшего слова.

Википедия определяет ссылочную прозрачность как:

Выражение называется ссылочно-прозрачным, если его можно заменить значением, не меняя поведения программы (другими словами, получая программу с такими же эффектами и выходными данными на одном входе).

Так что getLine также ссылочно прозрачен.Хотя я не могу придумать хороший способ выразить его «значение» каким-либо другим способом для «замены выражения его значением».

Кроме того, нужно быть немного осторожнее с такими утверждениями, какMsgstr "putStrLn при вызове с любыми аргументами всегда будет возвращать IO ()".IO () это тип, а не значение.Для каждого s :: String, putStrLn s - это значение типа IO (), да.Но то, что это значение, конечно, зависит от s.

(Кроме того, если исключить эти unsafe вещи, все чисто и референтно прозрачно, и в частности так же getLine.)

Answer 4

Позвольте мне просто ответить на вторую часть вопроса (я ответил на первую часть в предыдущем вопросе). Компилятор может делать с выражением все, что захочет, если только он не меняет семантику программы. Поэтому вы должны задать вопрос о конкретном компиляторе, чтобы он имел смысл. Есть ли GHC? Нет, не текущая версия. Есть ли компиляторы, которые делают? Да, есть.

Answer 5

Я не уверен, поможет ли это (заранее извиняюсь, если это только сбивает с толку), но способ, которым IO делается ссылочно-прозрачным в Mercury, заключается в явной передаче значения типа io всем выполняющим IO код, который также должен возвращать новое значение типа io.

Ввод io представляет «состояние мира» непосредственно перед вызовом кода. весь мир вне программы; содержимое диска, то, что напечатано на экране, что набирает пользователь, что будет получено из сети, все.

Выходные данные io представляют состояние мира сразу после вызова кода. Разница между входом io и выходом io содержит изменения в мире, которые были сделаны этим кодом (плюс все остальное, что произошло снаружи, в теории).

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

Конечно, реальное состояние реального мира не кодируется в значения типа io; на самом деле под капотом io совершенно пусто! Там нет информации, передаваемой на всех! Но io значения представляют состояние мира.

Вы можете думать о функциях в монаде IO как о том же. Они принимают дополнительный неявный аргумент состояния мира и возвращают дополнительное неявное значение состояния мира. Реализация монады IO обрабатывает передачу этого дополнительного вывода следующей функции. Это делает монаду IO очень похожей на монаду государства; Легко видеть, что get в этой монаде чисто, хотя, похоже, она не принимает аргументов.

В этом понимании main получает начальное состояние мира до запуска вашей программы и преобразует его в состояние мира после запуска программы, пропуская его через весь код ввода-вывода в вашей программе.

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

Так что getLine :: IO String можно рассматривать как нечто вроде getLine :: World -> (World, String). Это чисто, потому что все эти разные времена он вызывается и возвращает разные строки, которые он получает разные World каждый раз.

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

Аналогия в том, что вы можете реализовать карту с деревьями поиска или хеш-таблицами или другими способами. Но, реализовав его, когда вы рассуждаете о коде, который использует карту, вы не думаете о левом и правом поддеревьях или сегментах и ​​хэшах, вы думаете об абстракции, которая является картой.

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

---

И краткое дополнение к вашему второму вопросу.GHC теоретически может свести эту входную программу к выходному.Я не верю, что это очень трудно сделать, потому что это вообще неразрешимо.Представьте себе программу, которая не требует ввода, но генерирует бесконечный список и затем печатает последние 3 элемента.Теоретически любая программа, которая не зависит от ее входных данных, может быть сокращена до ее выходных данных, но для этого компилятор должен сделать что-то эквивалентное выполнению программы во время компиляции.Таким образом, чтобы сделать это полностью , вы должны быть рады, что ваши программы иногда переходят в бесконечные циклы во время компиляции .И почти каждая программа зависит от ее входных данных, поэтому даже попытка сделать это не так уж велика.

Там - это что-то, что можно получитьвыявление частей программ, не зависящих от какого-либо ввода, и замена их результатом.Это называется частичная оценка , и это активная тема исследования, но это также очень сложно, и нет единого решения для всех.Чтобы сделать это, вы должны быть в состоянии определить области программы, которые не будут отправлять компилятор в бесконечный цикл, пытаясь выяснить, что они возвращают, и вы должны принять решение о том, удалить ли какой-либо код, который занимает несколькоСекунды во время выполнения - это достаточно хорошее преимущество, если оно означает встраивание структуры данных размером в несколько сотен мегабайт, которую она возвращает в двоичный файл программы.И вы должны выполнить весь этот анализ, не тратя часов на компиляцию умеренно сложных программ.

Answer 6

По поводу второй части вопроса. Есть нечто, называемое суперкомпиляцией , которое, мы надеемся, подхватит что-то подобное. Это все еще область исследований.