История изменений

Что такое «вычисления IO»?

Процесс выполнения всех необходимых эффектов в рамках RTS для соответствующего терма main типа IO a.

Вот тут:

{-# LANGUAGE GADTs, KindSignatures #-}

import Prelude hiding ( IO, putStrLn, getLine )

data IO :: * -> * where
  Return :: a -> IO a
  Bind :: IO a -> (a -> IO b) -> IO b
  PutStrLn :: String -> IO ()
  GetLine :: IO String
  -- ...

instance Monad IO where
  return = Return
  (>>=) = Bind

putStrLn :: String -> IO ()
putStrLn = PutStrLn

getLine :: IO String
getLine = GetLine

main' :: IO ()
main' = do
  name <- getLine
  putStrLn name
  putStrLn "I'm pure-pure-pure :/"

с точки зрения абстрактного хаскеля всё чисто (с точки зрения денотационной семантики этого языка), main' в нормальной форме это просто некий терм типа IO (), то есть дерево/AST представляющее описание императивной программы. Но с точки зрения компилятора (и вообще операционной семантики RTS) это описание нужно скомпилировать в представление RTS, задействовать её функции, так чтобы при выполнении/запуске скомпилированного кода правильно выполнились все эффекты. То есть можно сказать, что тип и функции IO описывают теорию вычислений с эффектами в чистом языке, а компилятор (интерпретатор) уже реализует модель такой теории.

Что такое «вычисления IO»?

Процесс выполнения всех необходимых эффектов в рамках RST для соответствующего терма main типа IO a.

Вот тут:

{-# LANGUAGE GADTs, KindSignatures #-}

import Prelude hiding ( IO, putStrLn, getLine )

data IO :: * -> * where
  Return :: a -> IO a
  Bind :: IO a -> (a -> IO b) -> IO b
  PutStrLn :: String -> IO ()
  GetLine :: IO String
  -- ...

instance Monad IO where
  return = Return
  (>>=) = Bind

putStrLn :: String -> IO ()
putStrLn = PutStrLn

getLine :: IO String
getLine = GetLine

main' :: IO ()
main' = do
  name <- getLine
  putStrLn name
  putStrLn "I'm pure-pure-pure :/"

с точки зрения абстрактного хаскеля всё чисто (с точки зрения денотационной семантики этого языка), main' в нормальной форме это просто некий терм типа IO (), то есть дерево/AST представляющее описание императивной программы. Но с точки зрения компилятора (и вообще операционной семантики RTS) это описание нужно скомпилировать в представление RST, задействовать её функции, так чтобы при выполнении/запуске скомпилированного кода правильно выполнились все эффекты. То есть можно сказать, что тип и функции IO описывают теорию вычислений с эффектами в чистом языке, а компилятор (интерпретатор) уже реализует модель такой теории.