Suggestion to improve type inference

[ocharles]

I really want to like freer-simple, but I can't until it infers at least as well as idiomatic mtl usage. The big problem at the moment is Member:

class FindElem eff effs => Member (eff :: * -> *) effs

This multi-parameter type class infers miserably because there is no connection between the parameters. However, we can do better! Ignoring FindElem for now, this has much better inference, at the cost of: a. limiting you to a single type of effect and b. Adding a parameter to effect definitions:

class Member ( eff :: k -> * -> * ) config effs | effs eff -> config

That is, if I know the set of effects and a particular effect, I can tell you the "configuration" of that effect. Configured or parameterized effects are polymorphic effects such Reader, State, etc. This encoding means

Member Reader r effs

is like

MonadReader r m

This has the same "drawbacks" as functional dependencies in mtl, but I believe those drawbacks are significantly overblown. The good news is that as effects are first class in freer-simple, it's pretty trivial to just newtype Reader for example to have it occur twice (at different types) in eff.

The complication to the kind of eff can probably be worked around with

data Mono (eff :: * -> *) (config :: ()) a where
  Mono :: eff a -> Mono '() a

or something.

What do you think? Happy to throw up a PR if you want to see how it looks in practice. I'm using this in a private extensible effects like library to much success.

[ocharles]

As an example of where the inference in freer-simple kills me, consider logging-effect logging prettyprinter Docs.

I create my effect type:

data Log a where
  LogMsg :: a -> Log ()

log :: Member (Log msg) effs => msg -> Eff effs ()
log = send . LogMsg

However, if I try and log a Doc, everything falls apart:

foo :: Member (Log (Doc ()) effs => Eff effs ()
foo = do
  ...
  log "Hello"

"Hello" :: forall ann. Doc ann, and even though I've provided a concrete type signature to foo, this still won't infer, because nothing is going to force ann ~ (). However,

foo :: Member Log (Doc ()) effs => Eff effs ()
foo =

works out beautifully - effs Log determines that the type of the thing I'm logging is Doc ().

[lexi-lambda]

I’m not sure I like the idea of effectively forcing a single instance of a given effect per list, but I’m not dead set against the idea, either. I’ll probably have to think about it a little more.

[ocharles]

Glad you're open minded on this. To be honest, I can count on one hand the amount of times I've wanted multiple instances of one effect. I'd also note that this approach doesn't necessarily preclude this. Assume we had

data Multi effect cfg a where Multi :: effect a -> Multi effect cfg a

(Name subject to bike shedding)

Now we can say

(Member (Multi (Reader r1)) () m, Member (Multi (Reader r2)) () m) => 

The fun-dep says "there can only be one Multi (Reader r1) and one Multi (Reader r2), but as those are different types, a set of effs can have both.

Next, add

multi :: forall x. Eff (effect x ': effs) a -> Eff (Multi (effect x) ': effs) a

And we can write

x <- multi @Int ask

And recover multiple instances of an effect, essentially via newtyping. Basically we've shifted the burden onto people who want multiple instances, rather than having everyone pay.

See also the discussion here.

[lexi-lambda]

After a little bit of thought, my gut reaction is that I don’t like how this makes the API more complicated. Members [Reader String, State Integer, Console] => is a pleasant-looking constraint, and it’s extremely easy to understand. You have a list of effects. Even Haskell beginners can grok that. Members [(Reader, String), (State, Integer), (Console, ())] => is much less obvious, especially the last bit involving Console. Sure, if you are an experienced Haskeller, and especially if you are knee-deep in the problem of Haskell effects systems, it makes sense, and it might seem like a tiny cost to pay to solve a big problem (specifically, lack of type inference).

I wrote the API of freer-simple so that I could explain a Haskell system that uses effects to someone who has never even written any Haskell before. Sure, it requires some white lies and vigorous handwaving, but the notation is clear (which it turns out helps immensely in practice), and actually writing it is harder than reading it, but it’s critical that people don’t feel completely lost in the language as soon as they have to do a tiny bit of I/O.

The mental model of freer-simple is that an effect is just a capability, and they are individual, self-contained things that can be moved around at will. Don’t get me wrong, I am deeply saddened by the fact that these very same beginners can bump into awkward type ambiguity errors, but those type errors can be explained, and I think the simpler mental model has a lot going for it.

[isovector]

I'd like to strongly weigh-in against this; when you start considering freer monads as "implementation mixins", you generally do want a significant number of the same effect. I've used an eff stack in production with as many as eight readers and 12 writers--amongst other more interesting effects.

For example, at the domain level, lots of things are just writers---you don't particularly care what happens to them in your business logic, just that you emitted them. The mixin behavior can rewrite these into external effects with arbitrary systems.

Restricting effects to one-per-stack fundamentally limits the composability of these mixins.

[ocharles]

I may explore

class MonadFoo a m | m -> a where
  sendFoo :: Foo a -> m a

instance Member (Foo a) effs => MonadFoo a (Eff effs) where
  sendFoo = send

data Foo :: * -> * -> * where
  Op :: a -> Foo a ()

op :: MonadFoo a m => a -> m ()
op = sendFoo . Op

I still feel that while multiple effects is nice to have theoretically, in practical Haskell it just doesn't work for me. I easily end up with polymorphic effects and then hating the complete lack of any usable inference.

I ultimately moved to simple-effects instead though, which has a slightly different take:

• ExtraConstraint allows an effect to add a functional dependency keeping main effect constraint small. E.g., MonadEffect (State s) m is all you need to write, and you get a fun dep on m -> s.
• MonadEffect uses ExtraConstraint to enforce the (optional) functional dependency.

as many as eight readers and 12 writers--amongst other more interesting effects.

Are those monomorphic reads/writes? If so I can understand how that could work. I find things start to fall apart when you write things like tell (Sum 1) >> tell (Sum 2). Without a functional dependency, I believe that's just Member (Writer i) effs, Member (Writer j) effs, Integral i, Integral j, but that's almost certainly not what I meant.

[isovector]

Yeah, monomorphic reads/writes. I will admit that numbers (and MonadIO sends) are where the primary pain points are. It's usually enough to slap down a type application in a infrequently used place, or to let-bind a monomorphic read/write if you're going to be doing lots of it.

Not an ideal solution by any means, but I'd argue the benefits greatly outweigh the costs.

[ocharles]

logMsg :: (IsString s, Member (Log s) effs) => s -> Eff effs () is not an unreasonable thing to consider writing, but is almost entirely unusable if you want to retain polymorphic usage within freer-simple as things stand today. To use that, you would need to enable at least ScopedTypeVariables to be able to talk about the same s over multiple log messages. This, along with polymorphic state, is enough to convince me that this is worth serious consideration. I'm less attached to what the API is, I trust there is one out there that is good.

It's worth noting that you can still compose multiple readers in this, you just have to map them into a common type when you need to use two at once. I could imagine combinators like

embed :: Member (Reader y) effs => (y -> x) -> Eff (Reader x ': effs) ~> Eff effs

such that you might write

do
  foo <- embed fst ask
  bar <- embed snd ask
  return (if foo then bar else "!")

This isn't much more than forcing people to use ask @Bool and ask @String, but it means you don't have to do that if you only have a single consistent environment. The same story applies to other polymorphic effects.

[isovector]

The problem with that is that you often want to interpret Reader x differently than Reader y. A reader effect isn't simply an alias for (->) x--- it also could be HttpRequest [x] if you wanted to write an application that invisibly pages over websites.

I wonder if the underlying problem could be better solved via a typechecker plugin. If our only given in scope is a Member (Writer Int) r, then it seems pretty plausible to unify a tell 15 :: (Num a, Member (Writer a) r) => Eff r () with this.

[ocharles]

I wonder if the underlying problem could be better solved via a typechecker plugin. If our only given in scope is a Member (Writer Int) r, then it seems pretty plausible to unify a tell 15 :: (Num a, Member (Writer a) r) => Eff r () with this.

https://gitlab.com/LukaHorvat/simple-effects/commit/966ce80b8b5777a4bd8f87ffd443f5fa80cc8845. FWIW, it didn't work for the majority of uses in our code at work (loads of stuff was still ambiguous).

[isovector]

Great minds. Thanks for the lead---I'll take a look when I get a chance!