Wrapping side-effects in pure programming languages

91 views Asked by At

I'm researching possible ways to have computational effects in a pure programming language.

Monads are commonly presented as a way to wrap side effects in pure languages. I don't see how they help though. The problem I see is that monads can be copied or discarded.

In a pure language result of an operation should depend only on its arguments. But in a hypothetical language with

putStrLn :: String -> IO ()

the code

let a = putStrLn "1"
let b = putStrLn "2"
in ()

will get type Unit and fail to capture presence of side effects.

I can later also

let a1 = do
  _ <- a
  _ <- putStrLn "2.1"
let a2 = do
  _ <- a
  _ <- putStrLn "2.2"
in ()

Presumably diverging (not latest) state a into two paths a1 and a2. Or are all effects delayed until one selected IO () term is returned from the main function? I'm wondering then how purposely copyable monads holding mutable state are compiled (when a monad indeed diverged, at which point and how was the state copied?)

In contrast unique type seems to be able to naturally capture presence of the only one context

putStrLn :: 1 IO () -> String -> 1 IO ()

main :: 1 IO () -> 1 IO ()
main io = 
  let a = putStrLn io "1"
  let b = putStrLn a "2"

  // compile error, a has type 0 IO ()
  // let a1 = putStrLn a "2.1"
  in b

Which seems to capture that the state is irreversibly modified and cannot be accessed again. Thus all results of function calls indeed depend only on their arguments.

0

There are 0 answers