Монада ввода-вывода технически неверна?

12

На вики Haskell есть следующий пример условного использования монады ввода / вывода (см. Здесь) .

when :: Bool -> IO () -> IO ()
when condition action world =
    if condition
      then action world
      else ((), world)

Обратите внимание, что в этом примере определение IO aиспользуется, RealWorld -> (a, RealWorld)чтобы сделать все более понятным.

Этот фрагмент условно выполняет действие в монаде IO. Теперь, если предположить, что conditionэто Falseдействие actionникогда не должно выполняться. Используя ленивую семантику, это действительно так. Тем не менее, следует отметить здесь , что Haskell технически говоря нестрого. Это означает, что компилятору разрешено, например, превентивно запускаться action worldв другом потоке, а затем отбрасывать это вычисление, когда он обнаруживает, что оно ему не нужно. Однако к этому моменту побочные эффекты уже произошли.

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

Означает ли это, что монада ввода-вывода технически неверна или что-то еще мешает этому случиться?

Лассе
источник
Добро пожаловать в информатику ! Ваш вопрос здесь не по теме: мы занимаемся вопросами информатики , а не вопросами программирования (см. Наш FAQ ). Ваш вопрос может быть связан с переполнением стека .
dkaeae
2
На мой взгляд, это вопрос информатики, поскольку он касается теоретической семантики Haskell, а не практического вопроса программирования.
Лассе
4
Я не слишком знаком с теорией языка программирования, но думаю, что этот вопрос здесь актуален. Это может помочь, если вы уточнить, что здесь означает «неправильно». Как вы думаете, какое свойство имеет монада IO?
Дискретная ящерица
1
Эта программа плохо напечатана. Я не уверен, что ты на самом деле хотел написать. Определение whenможет быть типизированным, но у него нет типа, который вы объявляете, и я не вижу, что делает этот конкретный код интересным.
Жиль "ТАК - перестань быть злым"
2
Эта программа взята дословно со страницы вики на Haskell, ссылки на которую приведены выше. Это действительно не тип. Это потому, что он написан в предположении, IO aкоторое определено как RealWorld -> (a, RealWorld), чтобы сделать внутреннюю часть ввода-вывода более читаемой.
Лассе

Ответы:

12

Это предполагаемая «интерпретация» IOмонады. Если вы хотите отнестись к этой «интерпретации» серьезно, то вам нужно отнестись к «RealWorld» серьезно. Не имеет значения, action worldбудет ли он спекулятивно оценен или нет, actionне имеет побочных эффектов, его эффекты, если таковые имеются, обрабатываются путем возврата нового состояния юниверса, в котором эти эффекты имели место, например, был отправлен сетевой пакет. Тем не менее, результатом функции является ((),world)и, следовательно, новое состояние вселенной world. Мы не используем новую вселенную, которую мы могли спекулятивно оценить на стороне. Состояние вселенной есть world.

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

«Подожди, подожди», - говорите вы. « RealWorldэто просто« знак ». На самом деле это не состояние всей вселенной». Хорошо, тогда эта «интерпретация» ничего не объясняет. Тем не менее, как деталь реализации , именно так моделируется GHC IO. 1 Однако это означает, что у нас есть магические «функции», которые на самом деле имеют побочные эффекты, и эта модель не дает указаний по их значению. И, поскольку у этих функций действительно есть побочные эффекты, проблема, о которой вы говорите, полностью соответствует действительности. GHC действительно должен выйти из своего пути , чтобы убедиться , что RealWorldи эти специальные функции не оптимизированы таким образом , чтобы изменить целевое поведение программы.

Лично (как это, вероятно, очевидно сейчас), я думаю, что эта «проходящая мимо» модель IOпросто бесполезна и запутана как педагогический инструмент. (Полезно ли это для реализации, я не знаю. Для GHC я думаю, что это скорее исторический артефакт.)

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

data IO a = Return a | Request OSRequest (OSResponse -> IO a)

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

data OSRequest = OpenFile FilePath | PutStr String | ...

Точно так же OSResponseможет быть что-то вроде:

data OSResponse = Errno Int | OpenSucceeded Handle | ...

(Одно из усовершенствований , которые можно сделать, чтобы сделать вещи более типобезопасно так , что вы знаете , что вы не получите OpenSucceededот PutStrзапроса.) Эти модели , IOкак описывающие запросов , которые интерпретируются некоторой система (для «реального» IOмонады это сама среда выполнения Haskell), а затем, возможно, эта система вызовет обработчик, которому мы предоставили ответ. Это, конечно, также не дает никаких указаний на то, как PutStr "hello world"должен обрабатываться подобный запрос , но также не претендует на это. Это ясно показывает, что это делегируется какой-то другой системе. Эта модель также довольно точна. Все пользовательские программы в современных ОС должны делать запросы к ОС, чтобы что-либо делать.

Эта модель обеспечивает правильную интуицию. Например, многие начинающие рассматривают такие вещи, как <-оператор, как «развёртывание» IO, или имеют (к сожалению, усиленные) представления, которые IO String, скажем, являются «контейнером», который «содержит» Strings (а затем <-выводит их). Это представление запрос-ответ делает эту перспективу явно неправильной. Там нет файлового дескриптора внутри OpenFile "foo" (\r -> ...). Распространенная аналогия, подчеркивающая это, состоит в том, что в рецепте для пирога нет торта (или, может быть, в этом случае «счет» будет лучше).

Эта модель также легко работает с параллелизмом. Мы можем легко иметь конструктор для OSRequestlike, Fork :: (OSResponse -> IO ()) -> OSRequestи тогда среда выполнения может чередовать запросы, генерируемые этим дополнительным обработчиком, с обычным обработчиком, как ему нравится. С некоторой сообразительностью вы можете использовать это (или связанные с ним методы) для того, чтобы на самом деле более точно моделировать такие вещи, как параллелизм, вместо того, чтобы просто сказать «мы делаем запрос к ОС, и все происходит». Вот как работает IOSpecбиблиотека .

1 Объятия использовали реализацию на основе продолжения из IOкоторого примерно подобно тому , что я описать хотя и с непрозрачными функциями вместо явного типа данных. HBC также использовал реализацию, основанную на продолжениях, поверх старого ввода-вывода, основанного на запросе-ответе. NHC (и, таким образом, YHC) использовали thunks, то есть, IO a = () -> aхотя они и ()назывались World, но не передают состояния. JHC и UHC использовали в основном тот же подход, что и GHC.

Дерек Элкинс покинул ЮВ
источник
Спасибо за ваш просветляющий ответ, это действительно помогло. Ваша реализация IO заняла некоторое время, чтобы обернуть мой разум, но я согласен, что это более интуитивно понятно. Вы утверждаете, что эта реализация не страдает от потенциальных проблем с упорядочением побочных эффектов, как реализация RealWorld? Я не могу сразу увидеть какие-либо проблемы, но мне также не ясно, что они не существуют.
Лассе
Один комментарий: кажется, что на OpenFile "foo" (\r -> ...)самом деле должно быть Request (OpenFile "foo") (\r -> ...)?
Лассе
@Lasse Да, это должно было быть с Request. Чтобы ответить на ваш первый вопрос, это IOявно нечувствительно к порядку оценки (по модулю дна), потому что это инертная ценность. Все побочные эффекты (если таковые имеются) будут вызваны тем, что интерпретирует это значение. В этом whenпримере это не имеет значения, если actionего оценивать, потому что это будет просто значение, Request (PutStr "foo") (...)которое мы не будем отдавать тому, что интерпретирует эти запросы в любом случае. Это как исходный код; не имеет значения, будете ли вы сокращать его с энтузиазмом или ленивостью, ничего не произойдет, пока он не будет передан переводчику.
Дерек Элкинс покинул SE
Ах да, я вижу это. Это действительно умное определение. Сначала я подумал, что все побочные эффекты обязательно должны произойти, когда закончится выполнение всей программы, потому что вы должны построить структуру данных, прежде чем сможете ее интерпретировать. Но так как запрос содержит продолжение, вам нужно только собрать данные самого первого Request, чтобы начать видеть побочные эффекты. Последующие побочные эффекты могут быть созданы при оценке продолжения. Умная!
Лассе