OPAQUE is better than NOINLINE for this idiom, but it’s not obvious that one should use OPAQUE over NOINLINE
One must use unsafePerformIO, but it’s not actually unsafe if one uses OPAQUE. You lose ordering guarantees with regard to other IO actions, but that’s no more unsafe than hGetContents.
foo :: %TopLevelIO (IORef Int); foo = newIORef 0 is actually semantically sound and safe, provided the compiler respect the modifier
{-# LANGUAGE StandaloneKindSignatures #-}
module Control.Monad.ACIO
( ACIO (), -- Constructor not exposed.
acioToIO,
newIORef,
getNumProcessors,
)
where
import Control.Monad.IO.Class
import qualified Data.IORef as IO
import Data.Kind (Type)
import qualified GHC.Conc as IO
-- | IO-like monad with the the following two properties:
-- - The effect of `ACIO a` can be omitted if the result `a` is not needed in the program.
-- - The effect of running `ACIO a` can be commuted with any other effect in IO.
type ACIO :: Type -> Type
newtype ACIO a = MkACIO (IO a)
instance Functor ACIO
instance Applicative ACIO
instance Monad ACIO
acioToIO :: ACIO a -> IO a
acioToIO (MkACIO x) = x
newIORef :: a -> ACIO (IO.IORef a)
newIORef x = MkACIO $ IO.newIORef x
getNumProcessors :: ACIO Int
getNumProcessors = MkACIO IO.getNumProcessors
-- Extendable with new operations that are verified to fulfil the promises of ACIO
Then desugar:
f :: %ToplevelIO a
f = body
(where body :: ACIO a) to
{-# OPAQUE f #-}
f :: a
f = unsafePerformIO (acioToIO body)
This would preserve the reasoning principles of safe code, also wouldn’t special case the newIORef method, and make it extensible by just adding new functions to the Control.Monad.ACIO module which have been verified to fulfil the semantic properties of that monad.
You wouldn’t be able to run arbitrary IO code or extend the monad with new methods in user libraries, except by using unsafeCoerce. But that is probably what you want, since it is not semantically sound to lift arbitrary IO functions to ACIO.
My original motivation is for prometheus metrics backed by a ByteArray. IIUC your suggestion would be equivalent to a global Reader effect (with local), whereas I intentionally want a global State/Writer effect
There’s no special casing of newIORef. It allows any IO
Your ACIO code snippet has a MonadIO instance, so anyone could liftIO arbitrary actions in it
You can’t liftIO an ACIO action, liftIO only works on IO. You need to export an explicit acioToIO function
I’m not sure why we need to restrict IO actions. Where is the unsafety here? If you’re worried about third-party code running arbitrary IO code in an innocuously named pure value, you can already do so with unsafePerformIO today. Making it easier/safer to use doesn’t change the attack vector
And a State/Writer effect is the same as passing a mutable value as
a Reader effect/plain argument.
I’m not fond of effect system language in this context, it obscures implementation. The point is simply that thread-local state is not something that can be inlined, so if it were a feature you’d be able to use it to sidestep the entire problem.
There’s no special casing of newIORef. It allows any IO
Sorry, I expressed myself a bit awkwardly. Previous proposals (not yours) proposed to special case newIORef. Both your original proposal and my proposed variant using ACIO don’t special case newIORef.
Your ACIO code snippet has a MonadIO instance, so anyone could liftIO arbitrary actions in it
You can’t liftIO an ACIO action, liftIO only works on IO. You need to export an explicit acioToIO function
Sorry, didn’t check my code carefully enough. I have changed the snippet and the desugaring accordingly. (Removed the MonadIO instance and added acioToIO.)
I’m not sure why we need to restrict IO actions. Where is the unsafety here? If you’re worried about third-party code running arbitrary IO code in an innocuously named pure value, you can already do so with unsafePerformIO today. Making it easier/safer to use doesn’t change the attack vector
It’s not about an attack vector by a malicious actor, but about semantic guarantees.
If you allow to run arbitrary IO actions with unsafePerformIO using the on-demand semantics that you propose, then you potentially invalidate valid Haskell rewrites. I gave an example in the GitHub discussion. Let me repost it here:
f :: %ToplevelIO (IORef String)
f = newIORef "one"
g :: %ToplevelIO ()
g = writeIORef f "two"
main :: IO ()
main = do
case g of
() -> do
x <- readIORef f
print x -- prints "two"
-- After "refactoring" `main` by removing redundant case expression on unit type
main' :: IO ()
main' = do
x <- readIORef f
print x -- prints "one"
The difference with the restricted set of actions living in ACIO is that they do not invalidate any Haskell reasoning if performed using unsafePerformIO. That is why previous proposals suggested just special casing newIORef on the toplevel.
An alternative is to not have a lazy on-demand semantics of toplevel IO, but to give a deterministic “initialization” semantics to toplevel IO: They are all run in some deterministic order upon program start.
(I was also turning crazy because I knew that this had been discussed somewhere, but I couldn’t find it in the GHC proposals repo. I finally found it linked from the old Haskell prime mailing list from around 2008: Re: [Haskell-cafe] global variables - Haskell-prime - Haskell.org )
Just out of curiosity: If you knew whether the result of an action is unused, you could solve the Halting Problem, couldn’t you? In other words, the property we’re looking for is acio >>= (const (return a)) = return a which holds for a surprisingly small family of monads.
So pragmas that influence optimisation are something I can live with. But using pragmas to influence *semantics* really is an evil practice IMO and is something that should be discouraged, not made an unavoidable necessity.
I don’t like the fact that we’re relying on a pragma here for semantics. Unfortunately, we already have this in the OVERLAPPING pragmas, but I think we should move away from this.
Global variables seems to be many steps backwards for Haskell. If I had a say, I vote to abandon this and redirect efforts on fixing bugs or supporting abandoned hackage packages.
There was a time, when a good number of GHC proposals had clear denotational and operational semantics fleshed out as well all the concommitant proofs on completeness, soundness, etc. It would be nice to see something similar instead of this ad-hoc coding approach that affects all GHC programmers.
Couldn’t this be done as a library instead of a sledge-hammer approach of modifying the compiler?
I’m almost postive that many–if not the majority–of haskell programmers would find “global varaibles” an awfully bad idea at the compiler level.
Yes, I agree with the principle that using pragmas should not influence semantics. But this sentiment holds, in my opinion, only for code that doesn’t unsafeX functions. Using unsafeX means that you are leaving the realm of Haskell semantics and entering the realm of GHC implementation details. And also that the semantics of the code might be dependent on details of the optimization pipeline that are influenced by pragmas.
The other principle I would like to propose is that enabling a language extension should not change the equational theory of Haskell. I don’t think there are any language extensions that do this (maybe Strict, StrictData do this at the moment?). If you restrict the proposal to ACIO then you can make a reasonably solid argument that you don’t change the equational theory, but if you allow any top level IO then you substantially weaken it.
A monadic action f :: IO a has the first property if f >> g = g for all IO actions g. This is true for almost all IO actions which don’t change the environment but read something from it. So most getX functions from System.Environment, but also readIORef, or functions that generate a random number in the IO monad. Importantly, newIORef also has this property.
Very few monadic functions f have the second property, i.e. they commute with all other IO actions. In particular, this means they cannot have any observable effect in time, or which can be influenced by other IO actions. readIORef doesn’t have this property since it does not commute with writeIORef, for example. newIORef is the main example of a function having this property, but getNumProcessors similarly commutes with all other IO actions, since no IO action can change the number of CPU cores. getRandom specialized to IO also has the property, if we consider that the state of the PRNG is not observable.
The main problem also is not so much decidability but that we currently don’t have a formal model of the semantics of IO. So we cannot really say when to IO actions f and g are equivalent. Clearly we have that print "hello" >> print "world" != print "world" >> print "hello", but as soon as we have IORefs, forkIO etc. it all becomes muddy in the absence of a formal memory model.
I disagree. Doesn’t newIORef allocate something and alter the heap? Couldn’t the host system of a VM alter the result of getNumProcessors over the lifetime of the Haskell program?
The >> example is only the most obvious, syntactic case. My criticism is that no compiler can, in general, tell whether subsequentCode :: IORef a -> IO something is a constant function and therefore the preceding call to newIORef can be optimized away or floated elsewhere in the control flow.
Operationally newIORef does alter the state of the heap. But this change shouldn’t be observable from Haskell programs according to any sensible semantics for IO and IORefs. The purpose of a semantics of IO is to give exact definitions of what IO programs are considered equivalent and should always allow to optimize newIORef x >> m to m.
(Section 4 of the SC-Haskell paper https://www.recurial.com/ppopp17-sc-haskell.pdf gives a good idea of how such a semantics for IORefs should look like. They specify sequential consistency for IORefs, but weaker memory models are possible as well.)
For this use case it is not essential that the compiler can decide whether a value is used. The property is needed to make %ToplevelIO sound. Especially for the combination of lazyness + unsafePerformIO: lazyness means that the IO effect of a toplevel declaration f :: %ToplevelIO will not be executed if the result is not needed and that it may be performed at an unpredictable point in time. The first property of ACIO guarantees that the semantics of the program doesn’t change if the f is not executed at all, and the second property of ACIO guarantees that the semantics of the program doesn’t depend on the point in time that the IO effect of f occurs.
What’s wrong with the existing way to do it? The proposal doesn’t actually explain this.
This proposal smells very superficial to me. We are adding syntax for a very niche pattern. A pattern that offends the core language culture. A pattern that already is 100% supported with some skill.
Because..some spec from the 2010s said we need global state?
I’m sorry but that i read a NOINLINE vs OPAQUE discourse thread and then see a ghc proposal about it is wild to me LOL