| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
System.IO.Linear
Description
This module redefines IO with linear types.
To use this IO, do the following:
- use
main = withLinearIO $ do ... - pull in any safe non-linear
IOfunctions withfromSystemIOandfromSystemIOU - for mutable IO references/pointers, file handles, or any resources, use
the linear APIs provided here and in other linear
System.IOmodules
Example
import qualified System.IO.Linear as Linear main :: IO () main = Linear.withLinearIO $ Linear.fromSystemIOU $ putStrLn "hello world today"
Replacing The Original IO With This Module.
This module will be deprecated if the definition for IO found here is
upstreamed in System.IO. When multiplicity-polymorphism is implemented,
this module will supercede IO by providing a seamless replacement for
System.IO that won't break non-linear code.
Synopsis
- newtype IO a = IO (State# RealWorld %1 -> (# State# RealWorld, a #))
- fromSystemIO :: IO a %1 -> IO a
- fromSystemIOU :: IO a -> IO (Ur a)
- withLinearIO :: IO (Ur a) -> IO a
- newIORef :: a -> IO (Ur (IORef a))
- readIORef :: IORef a -> IO (Ur a)
- writeIORef :: IORef a -> a -> IO ()
- throwIO :: Exception e => e -> IO a
- catch :: Exception e => IO (Ur a) -> (e -> IO (Ur a)) -> IO (Ur a)
- mask_ :: IO a -> IO a
Documentation
This is the linear IO monad.
It is a newtype around a function that transitions from one
State# RealWorld to another, producing a value of type a along with it.
The State# RealWorld is the state of the world/machine outside the program.
The only way, such a computation is run is by putting it in Main.main
somewhere.
Note that this is the same definition as the standard IO monad, but with a linear arrow enforcing the implicit invariant that IO actions linearly thread the state of the real world. Hence, we can safely release the constructor to this newtype.
Interfacing with System.IO
fromSystemIO :: IO a %1 -> IO a Source #
Coerces a standard IO action into a linear IO action.
Note that the value a must be used linearly in the linear IO monad.
fromSystemIOU :: IO a -> IO (Ur a) Source #
Coerces a standard IO action to a linear IO action, allowing you to use
the result of type a in a non-linear manner by wrapping it inside
Ur.
withLinearIO :: IO (Ur a) -> IO a Source #
Use at the top of main function in your program to switch to the
linearly typed version of IO:
main :: IO () main = Linear.withLinearIO $ do ...
Using Mutable References
IORefs are mutable references to values, or pointers to values.
You can create, mutate and read them from running IO actions.
Note that all arrows are unrestricted. This is because IORefs containing linear values can make linear values escape their scope and be used non-linearly.
writeIORef :: IORef a -> a -> IO () Source #
Catching and Throwing Exceptions
Note that the types of throw and catch sport only unrestricted arrows.
Having any of the arrows be linear is unsound.
See here
to learn about exceptions.