The issues with effect systems

[atravers]

@jaror

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 […]

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

[gusbicalho]

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.

[atravers]

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:

• Let’s start with versioning, because the issues are pretty easy to see there. Let’s say I create a [definition] foo that declares it [uses effects] A, B, and C. In version two of foo, I want to add a bunch of features, and now foo might [use effect] D. It is a breaking change for me to add D to the [type signature] of that [definition], because [any] existing caller of that [definition] will almost certainly [need its type signature changed].

  Adding a new [effect] to a [type signature] in a new version breaks client code. […]

• The scalability issue is somewhat related to the versionability issue. In the small, checked [effects] are very enticing. With a little example, you can show that you’ve actually checked that you [dealt with the effect], and isn’t that great? Well, that’s fine when you’re just calling one API. The trouble begins when you start building big systems where you’re talking to four or five different subsystems. Each subsystem [relies on] four to ten [effects]. Now, each time you walk up the ladder of aggregation, you have this exponential hierarchy below you of [effects] you have to deal with. You end up having to declare 40 [effects] that you might [rely on]. And once you aggregate that with another subsystem you’ve got 80 [effects] in your [type signature]. It just balloons out of control.

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…

[jhenahan]

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.

[Abab9579]

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…

[atravers]

@jhenahan

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!

…many users of Lisp, Scheme and Erlang would probably agree with you :-)

---

@jhenahan

It strikes me as a facile comparison and one that bespeaks ignorance […]

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:

@atravers

…provided the number of independent effects is kept relatively small […]

…so you are correct - exposing very small sets of effects should be no worse than using a stack of monadic types, “aesthetically” speaking.

---

@Abab9579

That said, the so-called “purity” of Haskell might be fiction, anyway…

Should Haskell be rebranded away from "Pure Functional Programming"

Here’s the thing, Haskell isn’t actually “pure (functional programming)”. It has support for procedural-looking code (do notation), actually mutable variables (IORef, STRef, MVar, TVar), as well as dynamic types (Dynamic, -fdefer-type-errors), and even objects, via libraries like Hoop and Objective. What it is, instead, because of how Haskell relies on the IO monad, and GHC relies on State# RealWorld a, is “pure functional $ programming”. What you end up with is a relatively strict isolation be…

[hasufell]

@jhenahan

Local reasoning is the point

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.

[atravers]

@hasufell

I think the argument can be made that local reasoning does get harder with effects systems at some point.

…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)
#

[ribosomerocker]

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

[blamario]

@atravers

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:

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

@atravers

You end up having to declare 40 [effects] that you might [rely on].

are really about having to repeat those 40 declarations everywhere. In Haskell you declare them once and refer to the type synonym.

[atravers]

@blamario

[…] having to repeat those 40 declarations everywhere.

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

[blamario]

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:

https://playground.plutus.iohkdev.io/doc/haddock/plutus-contract/html/Plutus-Contract.html#t:Contract

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.

[atravers]

@blamario

The Contract monad is the type you’ll see [practically everywhere …].

…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?

[blamario]

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.

[atravers]

---

@blamario

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…

---

@atravers

Has the “asthetic similarity” between effect systems and checked exceptions been noticed by anyone else?

This is interesting:

Exceptions

Besides input/output, the most common type of effect found in most programming is the ability to fail. […] This is clearly an effect that we can model and we can create an interface similar to checked exceptions found in other languages.

Exotic Programming Ideas: Part 3 (Effect Systems), Stephen Diehl.

…so the similarity between effect systems and checked exceptions has been noticed before (albeit confined to the topic of exception-handling in this example).

[Abab9579]

For me, it seems like there are two uses of effect systems:

1. To annotate every effects being used.
2. To implement your own stack without much boilerplate.

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?

[danidiaz]

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.

[dataopt]

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.

[tomjaguarpaw]

Dive into effectful. I am sure.

[ocharles]

I think effectful and cleff would be good choices today. It depends a bit on what effects you want, though. Both effectful and cleff are essentially a reader-monad with a record of effect handlers, and some clever machinery to thread them around your program as you introduce and eliminate effects. This encoding does limit exactly what effects you can encode - but I think is a good trade-off as the more elaborate control-flow effects can usually be locally recovered by layering on things like ListT, LogicT, SearchT, etc. If you want those in an effects library, fused-effects might be a reasonable choice though.