But many effect systems do it under the hood, e.g. speff has this:
-- | Unpack the 'Eff' monad.
runEff :: Eff '[] a -> a
runEff (Eff m) = unsafeDupablePerformIO (runCtl $ m Rec.empty)
{-# INLINE runEff #-}
Do we really know for sure that is safe?
I believe, especially with higher operations, there are still open problems. For example you can store the continuation in a data type and run it later under another handler. I think that is also what Alexis’ Twitch stream was about.
It is really only used for the State effect though, and I’m pretty sure the underlying IORef is not accessible via the API. So I’d say its most likely safe.
For example you can store the continuation in a data type and run it later under another handler.
Ningning talked about this in her 2020 paper too. I used an existential trap to rule out this case in speff so it should be safe in this regard. But this does mean some limitations over expressiveness e.g. unable to implement the Async effect.
…which is just one potential problem whenever continuations are being used; it isn’t restricted to effect system implementations. Like state values, continuations require careful handling…
I am not totally sure, but I believe if you do that GHC will not be able to optimize stuff very well, because the monad m is abstract, so the monadic binds require a dictionary call etc. It is the same problem we get with mtl and fused-effects, you can get around it with SPECIALIZE, but it’s very inconvenient.
Has the “asthetic similarity” between effect systems and checked exceptions been noticed by anyone else?
If the terminology is changed from “effect system” to “checked effects”, then the experience with compile-time checking of exceptions seems relevant - to to paraphrase Anders Hejlsberg from this article:
These could be why some people prefer just using IO actions with IORefs, etc over checked effects effect systems - due to the monadic interface, I/O by itself is already considered rather invasive by more than a few…
I don’t see any similarities other than exposing information in function signatures, and if we’re throwing out that baby then why use static types at all? I have to handle all my Maybes at some point? The nerve! I’m trying to get real work done!
Checked exceptions and effect systems address entirely different concerns (except that I suppose an effect system could model checked exceptions but not vice versa) and there are a number of evolving implementations of the latter in multiple languages compared to the one that everyone writes articles about for the former.
It strikes me as a facile comparison and one that bespeaks ignorance of how people actually use these things unless there’s a very deep effect signature floating around to give the argument some teeth. My own use and the examples I steal from tend to expose very small sets of effects and combine them by composition and pretty immediate elimination rather than having to carry around knowledge about the whole universe as one does with checked exceptions.
Local reasoning is the point.
I cannot agree more that infection of effects (monad transformer or algebraic effects) to higher level is a huge issue. IO is generally better solution.
That said, the so-called “purity” of Haskell might be fiction, anyway…
…many users of Lisp, Scheme and Erlang would probably agree with you :-)
That’s why I used the term “asthetic similarity” - obviously there’s a difference between an exception (usually a visible value) and an effect (usually an abstract entity, often to ensure correct usage). And as I noted eariler:
…so you are correct - exposing very small sets of effects should be no worse than using a stack of monadic types, “aesthetically” speaking.
Yes. I think the argument can be made that local reasoning does get harder with effects systems at some point. They don’t constrain complexity and they cloud the actual implementation behind a set of abstract primitives that I have to track down in the end (the interpreter).
Coming up with primitives is in fact really hard. If you get the boundaries wrong or if you’re too abstract, they stop making sense.
And that’s what effects systems are about, IMO: primitives.
…I would say it’s the effects themselves, rather than the framework in which they’re restrained (monadic, applicative, functorial, arrowed, CPS, et al) e.g. accounting semantically for timing in a nonstrict language intended for real-time programming - interested readers should see Dave Harrison’s Ruth thesis for the details (from 1988: no monadic interface ;-).
Effects: they’ve been confounding semanticists since (at least) the 1960s, and that situation doesn’t look like changing any time soon:
# ghci GHCi, version 9.0.2: https://www.haskell.org/ghc/ :? for help ghci> :m Control.Monad.State ghci> ghci> forever $ putChar 'a' aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa^CaaaaInterrupted. ghci> ghci> case \c -> modify (++ [c]) of putChar' -> snd $ runState (forever $ putChar' 'a') [] "^CInterrupted. ghci> ghci> runState (forever $ return ()) () ^CInterrupted. ghci> ghci> forever $ return () ^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^Z Suspended (signal) #
Do you think one of the things that make effect systems harder to work with is that they are more expressive than MTL, which allows them to do much more, meaning it could get confusing to follow the code? If so, do you think an effect system like effectful but more restricted in expressivity would be better? Like freer-simple?
I think I understand your point about interpreters, but I feel like it isn’t that big of an issue to work with the effect interpreters. In a lot of cases you want to do things and you don’t care about how they’re done, and that’s what effect interpreters are for. But as I said, I won’t really understand your point since I’ve never been in this situation, which is why I think a demonstrative piece of code could be useful. That said, I don’t realy think hunting down the implementation of interpreters is that hard (actually, it would be useful if you mentioned which effect system you’ve been burned by), if it’s from the effect system itself you fetch it from their source code, if it’s in-house, you check out your own source code… but I’m really not sure
The trouble with Java’s checked exceptions is to a large extent syntactic. Not only are type signatures mandatory, but they have to individually list every checked exception (or its ancestor). There’s also no simple way to provide a generic exception-handler function, or in general to abstract away many common patterns. In contrast, any well designed application-level Haskell code in production will declare things like
type MyApplicationMonad = Eff MyApplicationEffects
type MyApplicationEffects = (CanLog, CanAccessDB, ...)
handleFileErrors :: (Peel (CanThrow 'MissingFile, CanThrow 'FileReadError) m n) => m a -> n a
So complaints like
are really about having to repeat those 40 declarations everywhere. In Haskell you declare them once and refer to the type synonym.
…which assumes all 40 definitions use the same set of effects: I suspect that rarely happens. So for the more likely case - each of those 40 (or 80) definitions using a different set of effects - one single type synonym for all those definitions seems less practical.
And if I’m not mistaken, that’s one of the proclaimed advantages of effects systems - being able to provide individual lists of effects for each definition, instead of having one “sin bin” effects-type for all definitions…
So for the more likely case - each of those 40 (or 80) definitions using a different set of effects…
That’s never been the more likely case in any codebase I’ve seen. Of course business applications tend to be closed source, but here’s an open-source example I’m familiar with:
The Contract monad is the type you’ll see in practically all Plutus contract signatures. If you skim the linked page and other documentation pages linked through the index, you’ll confirm that the API overwhelmingly refers to this type. The individual ContractEffs are made available but they’re rarely used.
…and out of all the definitions which use Contract directly:
how many use all of the effects Contract provides,
and how many have Contract in their type signatures “just for convenience”, e.g. because it’s too annoying to individually list the subset of effects the definition uses?
That’s beside my point. The complaints about checked exceptions in Java are about how inconvenient they are. Haskell APIs can provide the missing convenience because of the superior abstraction abilities of the language.
Furthermore, if some API users are more interested in precision than convenience, we can even provide two versions of the API: one that’s convenient and another that tracks the effects precisely. In my experience, once you reach the business level of an application the convenience always wins.
…just like how people often opt for the convenience of putting everything in IO, DynFlags, HscEnv (see page 33 of 59) or some other “kitchen sink” type. This observation would seem to diminish the claim that:
Haskell APIs can provide the missing convenience because of the superior abstraction abilities of the language.
Then again, maybe with the right set of effects GHC extensions…
This is interesting:
…so the similarity between effect systems and checked exceptions has been noticed before (albeit confined to the topic of exception-handling in this example).
For me, it seems like there are two uses of effect systems:
I think the effectiveness of point 1 is up for debate. Am I understanding this right?
On the point 2, how does effect systems compare with the deriving-trans approach?
I dislike Contract-like amalgamations of constraints and prefer sharply delineated effects.
In my experience, once you reach the business level of an application the convenience always wins.
I think we should draw inspiration from how dependency injection is done in OOP frameworks, like the Spring Framework for Java.
(I’m making an analogy between effects and DI “beans”, for example a repository component.)
In these frameworks, each component lists in its constructor the components on which it depends, and no more. In a sense, constructor arguments play the part of Eff constraints. It’s rare—and something of an antipattern—for a component to have knowledge of the whole set of components.
All methods within a component share the same member variables, so there’s no need to repeat the list of dependencies for each method.
There are so many options. If one has time to invest in learning one system, which would you recommend? I was about to dive into Effectful but now I am not sure.