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

-- | 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 Control.Exception (Exception)
import qualified Control.Exception as System (catch, mask_, throwIO)
import qualified Control.Functor.Linear as Control
import qualified Data.Functor.Linear as Data
import Data.IORef (IORef)
import qualified Data.IORef as System
import GHC.Exts (RealWorld, State#)
import Prelude.Linear hiding (IO)
import qualified System.IO as System
import qualified Unsafe.Linear as Unsafe
import qualified Prelude

-- | 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
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
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 = 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 =
  forall a. IO a %1 -> IO a
fromSystemIO (forall a. a -> Ur a
Ur 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 = 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 -> forall a. Ur a %1 -> a
unur Ur a
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Prelude.<$> (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 = forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \State# RealWorld
s ->
    forall a b.
(# State# RealWorld, a #)
%1 -> (a %1 -> b) %1 -> (# State# RealWorld, b #)
cont (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 = forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> 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
(<*>) = 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 = forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \State# RealWorld
s ->
    forall a b.
(# State# RealWorld, a #)
%1 -> (a %1 -> IO b) %1 -> (# State# RealWorld, b #)
cont (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' = 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 = forall a.
(State# RealWorld %1 -> (# State# RealWorld, a #)) -> IO a
IO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \State# RealWorld
s ->
    forall b.
(# State# RealWorld, () #)
%1 -> IO b %1 -> (# State# RealWorld, b #)
cont (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' = forall a.
IO a %1 -> State# RealWorld %1 -> (# State# RealWorld, a #)
unIO IO b
y' State# RealWorld
s'

instance Semigroup a => Semigroup (IO a) where
  <> :: IO a %1 -> IO a %1 -> IO a
(<>) = forall (f :: * -> *) a b c.
Applicative f =>
(a %1 -> b %1 -> c) %1 -> f a %1 -> f b %1 -> f c
Control.liftA2 forall a. Semigroup a => a %1 -> a %1 -> a
(<>)

instance Monoid a => Monoid (IO a) where
  mempty :: IO a
mempty = forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure forall a. Monoid a => a
mempty

-- $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 = forall a. IO a -> IO (Ur a)
fromSystemIOU (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 = forall a. IO a -> IO (Ur a)
fromSystemIOU (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 = forall a. IO a %1 -> IO a
fromSystemIO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ 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 = forall a. IO a %1 -> IO a
fromSystemIO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ 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 =
  forall a. IO a %1 -> IO a
fromSystemIO forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall e a. Exception e => IO a -> (e -> IO a) -> IO a
System.catch (forall a. IO a %1 -> IO a
toSystemIO IO (Ur a)
body) (\e
e -> 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 = forall a. IO a %1 -> IO a
fromSystemIO (forall a. IO a -> IO a
System.mask_ (forall a. IO a %1 -> IO a
toSystemIO IO a
action))