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.