Add Effectful.ST and Effectful.ST.STRef

[Innf107]

With this, effectful is able to mix STE with other effects, which makes it a very convenient way to avoid having to depend on IOE just to locally use mutable data structures.

The effect is tagged with an s region parameter and runSTE uses the same higher rank type trick as regular runST to prevent references from escaping.

I'm pretty sure that this is sound, however ST can be subtle so it would be nice to have a second opinion.
For some prior art: Koka uses a similar st effect that can be combined with arbitrary other effects.
References escaping through other effects (e.g. exceptions) shouldn't be an issue since that can only happen through an existential, at which point the reference cannot be accessed anymore anyway.

One thing I'm not entirely sure about is the type role on STE. The region parameter needs to be nominal for soundness, but making the others phantom seems a bit dangerous? This is also what is inferred for other effects like Process though.

[arybczak]

Thanks for the PR 👍 However...

Did you see https://hackage-content.haskell.org/package/effectful-core-2.6.0.0/docs/Effectful-Prim.html? It allows you to use everything from primitive, which pretty much generalizes and extends ST. The only thing you lose is the scope restriction (and thus runPrim requres IOE, so you can't use it within runPureEff), but it's IMO the best compromise.

I considered making it Prim s but the type parameter doesn't play well with type inference (as you already noticed since you're talking about having to use type applications and introduced a proxy). It really requires effectful-plugin in order to not be very annoying to use.

For example code like this:

blub :: forall s es. STE s :> es => Eff es ()
blub = do
  _ <- newSTRef @s 'x'
  pure ()

won't compile without effectful-plugin if you don't have AllowAmbiguousTypes enabled.

In conclusion: I experimented with this approach and decided it's not worth it over how currently Prim operates, so I'm not going to include it in the core library. But it's of course a great candidate for a separate library.

[Innf107]

Did you see https://hackage-content.haskell.org/package/effectful-core-2.6.0.0/docs/Effectful-Prim.html?

I have! Prim is very nice for giving functions the ability to write to shared mutable references without exposing full IOE, but the problem compared to STE is that Prim still leaks to consumers. It's more like an IORef effect than ST per se.

The main use case I see for ST(E) is as an implementation detail of functions that may otherwise not depend on Prim.

For example, what motivated me to make this PR was a very generic graph algorithm of type (essentially)

computeSCC :: (Hashable node) => (node -> Eff es [node]) -> node -> Eff es (HashMap node SCCId)

The function to access a node's edges needs to run in an effect since edges sometimes need to be computed from a mutable structure, so I can't just use regular ST, but I also don't want to force Prim onto callers since some of them may already have the full immutable graph available and use runPureEff.

As for the ambiguity, I agree that it is a bit unfortunate, but I don't think it's as bad as it seems.

A function using STE is only ambiguous, if it doesn't mention the passed in region in its arguments or return type. But in that case, there is really no point in requiring a region to be passed in over just running a new one.

So an example like your blub could always be rewritten unambiguously like this with no downside.

blub :: Eff es ()
blub = runSTE \(Proxy :: Proxy s) -> do
    _ <- newSTRef @s 'x'
    pure ()

Moreover, the only operations that ever need to use the s parameter are operations that create a new value that depends on s. Any read/write operation or anything else that takes an existing object parameterized on s (like an STRef or hash table) is already unambiguous.

So really, the only operations that need type applications are operations like newSTRef that create new objects, which are going to be comparatively rare anyway. I think that's pretty manageable.

[Innf107]

As a concrete example, the SCC algorithm I mentioned works with STE with no type annotations aside from the parts that create STRefs/hashtables. It otherwise needed no modifications going from IORefs to STRefs other than changing the names of all the functions and adding a raise around the call to outEdgesOrPrecomputedSCC

(simplified to reduce dependencies so i could check it in the effectful repo)

computeSCC ::
    forall node es.
    (Show node, Ord node) =>
    (node -> Eff es (Maybe [node])) ->
    node ->
    Eff es (Map node Int)
computeSCC outEdgesOrPrecomputedSCC node = runSTE $ \(Proxy :: Proxy s) -> do
    visited :: STRef s (Set node) <- newSTRef [node]
    currentDFSNum :: STRef s Int <- newSTRef 0
    dfsNums :: STRef s (Map node Int) <- newSTRef mempty

    openSCCs :: STRef s [node] <- newSTRef [node]
    openNodes :: STRef s [node] <- newSTRef [node]

    sccs :: STRef s (Map node Int) <- newSTRef mempty

    sccIds :: STRef s Int <- newSTRef 0
    let newSCCId = do
            id <- readSTRef sccIds
            writeSTRef sccIds (id + 1)
            pure id

    let go node = do
            dfsNum <- readSTRef currentDFSNum
            writeSTRef currentDFSNum (dfsNum + 1)
            modifySTRef' dfsNums (Map.insert node dfsNum)
            raise (outEdgesOrPrecomputedSCC node) >>= \case
                Nothing -> pure ()
                Just neighbors -> do
                    for_ neighbors $ \neighbor -> do
                        visitedUntilNow <- readSTRef visited
                        case Set.member neighbor visitedUntilNow of
                            False -> do
                                modifySTRef' visited (Set.insert neighbor)
                                modifySTRef' openSCCs (neighbor :)
                                modifySTRef' openNodes (neighbor :)

                                go neighbor
                            True -> do
                                dfsNumsUntilNow <- readSTRef dfsNums
                                let dfsNumOf otherNode = case Map.lookup otherNode dfsNumsUntilNow of
                                        Nothing -> error $ "DFS number of '" <> show node <> "' not found"
                                        Just dfsNum -> dfsNum

                                modifySTRef' openSCCs (dropWhile (\representative -> dfsNumOf representative >= dfsNum))
                    -- backtrack
                    readSTRef openSCCs >>= \case
                        (topRepresentative : rest)
                            | topRepresentative == node -> do
                                writeSTRef openSCCs rest

                                sccId <- newSCCId

                                let assignSCC = \case
                                        [] -> pure []
                                        (openNode : rest) -> do
                                            modifySTRef' sccs (Map.insert openNode sccId)
                                            if openNode == node
                                                then pure rest
                                                else assignSCC rest
                                currentOpenNodes <- readSTRef openNodes
                                remainingOpenNodes <- assignSCC currentOpenNodes
                                writeSTRef openNodes remainingOpenNodes
                        _ -> pure ()

    go node
    readSTRef sccs

[arybczak]

So an example like your blub could always be rewritten unambiguously like this with no downside.

It's a bit different, because my example is a util function for where STE is already in scope, while yours introduces and discharges it.

Ok, I see STE has an advantage over Prim in that you can introduce it anywhere in Eff without IOE in scope. But somewhat awkward usability without a plugin and multiple designs (Proxy vs no Proxy) remains.

Also, there's already https://hackage.haskell.org/package/effectful-st, but it takes a slightly different route and provides just adapter functions. Perhaps it would be worth coordinating with its author and introduce this PR there?

Btw, looking at this package I just remebered about #93, so this discussion happened before :) And the author of the ticket is the author of effectful-st. Looks like I remembered wrong in that Prim can't be parametrized with s like I thought it could be.