Каково значение действий ИО в чистых функциях?

Я думал, что в принципе система типа haskell запретит вызывать нечистые функции (т.е. f :: a -> IO b) из чистых, но сегодня я понял, что, называя их с помощью return, они компилируются просто отлично. В примере:

h :: Maybe ()
h = do
    return $ putStrLn "???"
    return ()

Теперь h работает в возможно монаде, но это чистая функция. Компиляция и запуск этого метода просто возвращает Just (), как и следовало ожидать, без ввода каких-либо операций ввода-вывода. Я думаю, что haskell лень объединяет вещи (т.е. putStrLn возвращаемое значение не используется - и не может, поскольку его конструкторы значений скрыты, и я не могу сопоставить их с ним), но почему этот код является законным? Существуют ли другие причины, позволяющие это разрешить?

В качестве бонуса, связанный с ним вопрос: вообще, можно ли вообще запретить исполнение действий монады изнутри других? Как?

Ответ 1

Операции ввода-вывода являются первоклассными значениями, как и любые другие; что делает Haskell IO настолько выразительным, что позволяет создавать структуры управления более высокого порядка (например, mapM_) с нуля. Лень здесь не уместна, ¹ просто, что вы фактически не выполняете действие. Вы просто строите значение Just (putStrLn "???"), а затем выбрасываете его.

putStrLn "???" Существующий не вызывает печать строки на экране. Сам по себе putStrLn "???" - это просто описание некоторого IO, которое можно было бы сделать, чтобы вывести строку на экран. Выполняется только выполнение main, которое вы создали из других операций ввода-вывода или любых действий, которые вы вводите в GHCi. Для получения дополнительной информации см. введение в IO.

В самом деле, вполне возможно, что вам может понадобиться манипулировать действиями IO внутри Maybe; представьте функцию String -> Maybe (IO ()), которая проверяет строку на достоверность, и, если она действительна, возвращает действие IO для печати некоторой информации, полученной из строки. Это возможно именно благодаря Haskell первоклассным действиям IO.

Но монада не может выполнять действия другой монады, если вы не дадите ей эту способность.

¹ В самом деле, h = putStrLn "???" `seq` return () не вызывает никакого ввода-вывода, даже если он вызывает оценку putStrLn "???".

Ответ 2

Пусть desugar!

h = do return (putStrLn "???"); return ()
-- rewrite (do foo; bar) as (foo >> do bar)
h = return (putStrLn "???") >> do return ()
-- redundant do
h = return (putStrLn "???") >> return ()
-- return for Maybe = Just
h = Just (putStrLn "???") >> Just ()
-- replace (foo >> bar) with its definition, (foo >>= (\_ -> bar))
h = Just (putStrLn "???") >>= (\_ -> Just ())

Теперь, что происходит, когда вы оцениваете h? * Ну, возможно,

(Just x) >>= f = f x
Nothing  >>= f = Nothing

Итак, мы сопоставляем первый случай

f x
-- x = (putStrLn "???"), f = (\_ -> Just ())
(\_ -> Just ()) (putStrLn "???")
-- apply the argument and ignore it
Just ()

Обратите внимание, что нам никогда не приходилось выполнять putStrLn "???", чтобы оценить это выражение.

* n.b. Несколько неясно, в какой момент "десурганизация" прекращается, и начинается "оценка". Это зависит от ваших решений, связанных с компилятором. Чистые вычисления могут быть полностью оценены во время компиляции.