{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE UnboxedTuples #-}

-- | 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.

module System.IO.Linear
  ( IO(..)
  -- * Interfacing with "System.IO"
  , fromSystemIO
  , fromSystemIOU
  , withLinearIO
  -- * Using Mutable References
  -- $ioref
  , newIORef
  , readIORef
  , writeIORef
  -- * Catching and Throwing Exceptions
  -- $exceptions
  , throwIO
  , catch
  , mask_
  ) where

import Data.IORef (IORef)
import qualified Data.IORef as System
import Control.Exception (Exception)
import qualified Control.Exception as System (throwIO, catch, mask_)
import qualified Control.Functor.Linear as Control
import qualified Data.Functor.Linear as Data
import GHC.Exts (State#, RealWorld)
import Prelude.Linear hiding (IO)
import qualified Unsafe.Linear as Unsafe
import qualified Prelude
import qualified System.IO as System


-- | 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.
newtype IO a = IO (State# RealWorld %1-> (# State# RealWorld, a #))
  deriving ((forall a b. (a %1 -> b) -> IO a %1 -> IO b) -> Functor IO
forall a b. (a %1 -> b) -> IO a %1 -> IO b
forall (f :: * -> *).
(forall a b. (a %1 -> b) -> f a %1 -> f b) -> Functor f
fmap :: forall a b. (a %1 -> b) -> IO a %1 -> IO b
$cfmap :: forall a b. (a %1 -> b) -> IO a %1 -> IO b
Data.Functor, Functor IO
Functor IO
-> (forall a. a -> IO a)
-> (forall a b. IO (a %1 -> b) %1 -> IO a %1 -> IO b)
-> (forall a b c.
    (a %1 -> b %1 -> c) -> IO a %1 -> IO b %1 -> IO c)
-> Applicative IO
forall a. a -> IO a
forall a b. IO (a %1 -> b) %1 -> IO a %1 -> IO b
forall a b c. (a %1 -> b %1 -> c) -> IO a %1 -> IO b %1 -> IO c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a %1 -> b) %1 -> f a %1 -> f b)
-> (forall a b c. (a %1 -> b %1 -> c) -> f a %1 -> f b %1 -> f c)
-> Applicative f
liftA2 :: forall a b c. (a %1 -> b %1 -> c) -> IO a %1 -> IO b %1 -> IO c
$cliftA2 :: forall a b c. (a %1 -> b %1 -> c) -> IO a %1 -> IO b %1 -> IO c
<*> :: forall a b. IO (a %1 -> b) %1 -> IO a %1 -> IO b
$c<*> :: forall a b. IO (a %1 -> b) %1 -> IO a %1 -> IO b
pure :: forall a. a -> IO a
$cpure :: forall a. a -> IO a
Data.Applicative) via (Control.Data IO)
type role IO representational

-- Defined separately because projections from newtypes are considered like
-- general projections of data types, which take an unrestricted argument.
unIO :: IO a %1-> State# RealWorld %1-> (# State# RealWorld, a #)
unIO :: forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO (IO State# RealWorld %1 -> (# State# RealWorld, a #)
action) = State# RealWorld %1 -> (# State# RealWorld, a #)
action

-- | Coerces a standard IO action into a linear IO action.
-- Note that the value @a@ must be used linearly in the linear IO monad.
fromSystemIO :: System.IO a %1-> IO a
-- The implementation relies on the fact that the monad abstraction for IO
-- actually enforces linear use of the @RealWorld@ token.
--
-- There are potential difficulties coming from the fact that usage differs:
-- returned value in 'System.IO' can be used unrestrictedly, which is not
-- typically possible of linear 'IO'. This means that 'System.IO' action are
-- not actually mere translations of linear 'IO' action. Still I [aspiwack]
-- think that it is safe, hence no "unsafe" in the name.
fromSystemIO :: forall a. IO a %1 -> IO a
fromSystemIO = IO a %1 -> IO a
forall a b. a %1 -> b
Unsafe.coerce

-- | 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'.
fromSystemIOU :: System.IO a -> IO (Ur a)
fromSystemIOU :: forall a. IO a -> IO (Ur a)
fromSystemIOU IO a
action =
  IO (Ur a) %1 -> IO (Ur a)
forall a. IO a %1 -> IO a
fromSystemIO (a -> Ur a
forall a. a -> Ur a
Ur (a -> Ur a) -> IO a -> IO (Ur a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Prelude.<$> IO a
action)

-- | Convert a linear IO action to a "System.IO" action.
toSystemIO :: IO a %1-> System.IO a
toSystemIO :: forall a. IO a %1 -> IO a
toSystemIO = IO a %1 -> IO a
forall a b. a %1 -> b
Unsafe.coerce -- basically just subtyping

-- | 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 ...
-- @
withLinearIO :: IO (Ur a) -> System.IO a
withLinearIO :: forall a. IO (Ur a) -> IO a
withLinearIO IO (Ur a)
action = (\Ur a
x -> Ur a %1 -> a
forall a. Ur a %1 -> a
unur Ur a
x) (Ur a -> a) -> IO (Ur a) -> IO a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Prelude.<$> (IO (Ur a) %1 -> IO (Ur a)
forall a. IO a %1 -> IO a
toSystemIO IO (Ur a)
action)

-- * Monadic interface

instance Control.Functor IO where
  fmap :: forall a b. (a %1-> b) %1-> IO a %1-> IO b
  fmap :: forall a b. (a %1 -> b) %1 -> IO a %1 -> IO b
fmap a %1 -> b
f IO a
x = (State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b
forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b)
%1 -> (State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ \State# RealWorld
s ->
      (# State# RealWorld, a #)
%1 -> (a %1 -> b) %1 -> (# State# RealWorld, b #)
forall a b.
(# State# RealWorld, a #)
%1 -> (a %1 -> b) %1 -> (# State# RealWorld, b #)
cont (IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO IO a
x State# RealWorld
s) a %1 -> b
f
    where
      -- XXX: long line
      cont :: (# State# RealWorld, a #) %1-> (a %1-> b) %1-> (# State# RealWorld, b #)
      cont :: forall a b.
(# State# RealWorld, a #)
%1 -> (a %1 -> b) %1 -> (# State# RealWorld, b #)
cont (# State# RealWorld
s', a
a #) a %1 -> b
f' = (# State# RealWorld
s', a %1 -> b
f' a
a #)

instance Control.Applicative IO where
  pure :: forall a. a %1-> IO a
  pure :: forall a. a %1 -> IO a
pure a
a = (State# RealWorld %1 -> (# State# RealWorld, a #)) %1 -> IO a
forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld %1 -> (# State# RealWorld, a #)) %1 -> IO a)
%1 -> (State# RealWorld %1 -> (# State# RealWorld, a #)) %1 -> IO a
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ \State# RealWorld
s -> (# State# RealWorld
s, a
a #)

  (<*>) :: forall a b. IO (a %1-> b) %1-> IO a %1-> IO b
  <*> :: forall a b. IO (a %1 -> b) %1 -> IO a %1 -> IO b
(<*>) = IO (a %1 -> b) %1 -> IO a %1 -> IO b
forall (m :: * -> *) a b.
Monad m =>
m (a %1 -> b) %1 -> m a %1 -> m b
Control.ap

instance Control.Monad IO where
  (>>=) :: forall a b. IO a %1-> (a %1-> IO b) %1-> IO b
  IO a
x >>= :: forall a b. IO a %1 -> (a %1 -> IO b) %1 -> IO b
>>= a %1 -> IO b
f = (State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b
forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b)
%1 -> (State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ \State# RealWorld
s ->
      (# State# RealWorld, a #)
%1 -> (a %1 -> IO b) %1 -> (# State# RealWorld, b #)
forall a b.
(# State# RealWorld, a #)
%1 -> (a %1 -> IO b) %1 -> (# State# RealWorld, b #)
cont (IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO IO a
x State# RealWorld
s) a %1 -> IO b
f
    where
      -- XXX: long line
      cont :: (# State# RealWorld, a #) %1-> (a %1-> IO b) %1-> (# State# RealWorld, b #)
      cont :: forall a b.
(# State# RealWorld, a #)
%1 -> (a %1 -> IO b) %1 -> (# State# RealWorld, b #)
cont (# State# RealWorld
s', a
a #) a %1 -> IO b
f' = IO b %1 -> State# RealWorld %1 -> (# State# RealWorld, b #)
forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO (a %1 -> IO b
f' a
a) State# RealWorld
s'

  (>>) :: forall b. IO () %1-> IO b %1-> IO b
  IO ()
x >> :: forall a. IO () %1 -> IO a %1 -> IO a
>> IO b
y = (State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b
forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b)
%1 -> (State# RealWorld %1 -> (# State# RealWorld, b #)) %1 -> IO b
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ \State# RealWorld
s ->
      (# State# RealWorld, () #)
%1 -> IO b %1 -> (# State# RealWorld, b #)
forall b.
(# State# RealWorld, () #)
%1 -> IO b %1 -> (# State# RealWorld, b #)
cont (IO () %1 -> State# RealWorld %1 -> (# State# RealWorld, () #)
forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO IO ()
x State# RealWorld
s) IO b
y
    where
      cont :: (# State# RealWorld, () #) %1-> IO b %1-> (# State# RealWorld, b #)
      cont :: forall b.
(# State# RealWorld, () #)
%1 -> IO b %1 -> (# State# RealWorld, b #)
cont (# State# RealWorld
s', () #) IO b
y' = IO b %1 -> State# RealWorld %1 -> (# State# RealWorld, b #)
forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO IO b
y' State# RealWorld
s'

-- $ioref
-- @IORef@s 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))
newIORef :: forall a. a -> IO (Ur (IORef a))
newIORef a
a = IO (IORef a) -> IO (Ur (IORef a))
forall a. IO a -> IO (Ur a)
fromSystemIOU (a -> IO (IORef a)
forall a. a -> IO (IORef a)
System.newIORef a
a)

readIORef :: IORef a -> IO (Ur a)
readIORef :: forall a. IORef a -> IO (Ur a)
readIORef IORef a
r = IO a -> IO (Ur a)
forall a. IO a -> IO (Ur a)
fromSystemIOU (IORef a -> IO a
forall a. IORef a -> IO a
System.readIORef IORef a
r)

writeIORef :: IORef a -> a -> IO ()
writeIORef :: forall a. IORef a -> a -> IO ()
writeIORef IORef a
r a
a = IO () %1 -> IO ()
forall a. IO a %1 -> IO a
fromSystemIO (IO () %1 -> IO ()) %1 -> IO () %1 -> IO ()
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
System.writeIORef IORef a
r a
a

-- $exceptions
--
-- Note that the types of @throw@ and @catch@ sport only unrestricted arrows.
-- Having any of the arrows be linear is unsound.
-- See [here](http://dev.stephendiehl.com/hask/index.html#control.exception)
-- to learn about exceptions.

throwIO :: Exception e => e -> IO a
throwIO :: forall e a. Exception e => e -> IO a
throwIO e
e = IO a %1 -> IO a
forall a. IO a %1 -> IO a
fromSystemIO (IO a %1 -> IO a) %1 -> IO a %1 -> IO a
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ e -> IO a
forall e a. Exception e => e -> IO a
System.throwIO e
e

catch
  :: Exception e
  => IO (Ur a) -> (e -> IO (Ur a)) -> IO (Ur a)
catch :: forall e a.
Exception e =>
IO (Ur a) -> (e -> IO (Ur a)) -> IO (Ur a)
catch IO (Ur a)
body e -> IO (Ur a)
handler =
  IO (Ur a) %1 -> IO (Ur a)
forall a. IO a %1 -> IO a
fromSystemIO (IO (Ur a) %1 -> IO (Ur a)) %1 -> IO (Ur a) %1 -> IO (Ur a)
forall a b. (a %1 -> b) %1 -> a %1 -> b
$ IO (Ur a) -> (e -> IO (Ur a)) -> IO (Ur a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
System.catch (IO (Ur a) %1 -> IO (Ur a)
forall a. IO a %1 -> IO a
toSystemIO IO (Ur a)
body) (\e
e -> IO (Ur a) %1 -> IO (Ur a)
forall a. IO a %1 -> IO a
toSystemIO (e -> IO (Ur a)
handler e
e))

mask_ :: IO a -> IO a
mask_ :: forall a. IO a -> IO a
mask_ IO a
action = IO a %1 -> IO a
forall a. IO a %1 -> IO a
fromSystemIO (IO a -> IO a
forall a. IO a -> IO a
System.mask_ (IO a %1 -> IO a
forall a. IO a %1 -> IO a
toSystemIO IO a
action))