System.IO.Linear

This module redefines IO with linear types.

To use this IO, do the following:

• use main = withLinearIO $ do ...
• pull in any safe non-linear IO functions with fromSystemIO and fromSystemIOU
• for mutable IO references/pointers, file handles, or any resources, use the linear APIs provided here and in other linear System.IO modules

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.

Documentation

newtype IO a

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.

Constructors

IO (State# RealWorld %1 -> (# State# RealWorld, a #))

Instances

Applicative IO

Defined in System.IO.Linear

Methods

pure :: a %1 -> IO a

(<*>) :: IO (a %1 -> b) %1 -> IO a %1 -> IO b

liftA2 :: (a %1 -> b %1 -> c) %1 -> IO a %1 -> IO b %1 -> IO c

Functor IO

Defined in System.IO.Linear

Methods

fmap :: (a %1 -> b) %1 -> IO a %1 -> IO b

Monad IO

Defined in System.IO.Linear

Methods

(>>=) :: IO a %1 -> (a %1 -> IO b) %1 -> IO b

(>>) :: IO () %1 -> IO a %1 -> IO a

MonadIO IO

Defined in Control.Monad.IO.Class.Linear

Methods

liftIO :: IO a %1 -> IO a

liftSystemIO :: IO0 a -> IO a

liftSystemIOU :: IO0 a -> IO (Ur a)

Applicative IO

Defined in System.IO.Linear

Methods

pure :: a -> IO a

(<*>) :: IO (a %1 -> b) %1 -> IO a %1 -> IO b

liftA2 :: (a %1 -> b %1 -> c) -> IO a %1 -> IO b %1 -> IO c

Functor IO

Defined in System.IO.Linear

Methods

fmap :: (a %1 -> b) -> IO a %1 -> IO b

Monoid a => Monoid (IO a)

Defined in System.IO.Linear

Methods

mempty :: IO a

Semigroup a => Semigroup (IO a)

Defined in System.IO.Linear

Methods

(<>) :: IO a %1 -> IO a %1 -> IO a

Interfacing with System.IO

fromSystemIO :: IO a %1 -> IO a

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)

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

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.

newIORef :: a -> IO (Ur (IORef a))

readIORef :: IORef a -> IO (Ur a)

writeIORef :: IORef a -> a -> IO ()

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.

throwIO :: Exception e => e -> IO a

catch :: Exception e => IO (Ur a) -> (e -> IO (Ur a)) -> IO (Ur a)

mask_ :: IO a -> IO a