Add something like Polysemy's `Members`

[sproott]

For quickly defining the possible effects, Polysemy has the Members type family. This can of course be implemented in effectful, something like this:

type family Effs effs es :: Constraint where
  Effs '[] es = ()
  Effs (e ': effs) es = (e :> es, Effs effs es)

Or maybe another type operator like ::>?

Or is there any particular reason it's not a thing yet?

[arybczak]

Yeah, I considered it. I didn't yet since not having it avoids unnecessary bikeshedding whether (A :> es, B :> es, C :> es) or e.g. [A, B, C] :>> es should be used in type signatures :thinking:

But maybe that's a weak argument.

[sproott]

I think that once you get to 5+ effects on the stack, the second way becomes much more readable.

Loving the library btw, managed to port pat.hs from Polysemy to effectful today.

[arybczak]

Loving the library

Thanks :bow:

I think that once you get to 5+ effects on the stack, the second way becomes much more readable.

That's a good point. You've convinced me ;) I have a plan of porting a big application that uses a lot of effects from the mtl style once effectful is released, so having that would indeed simplify type signatures.

There's one more thing though. For some reason ghci 9.2.1 started printing such signatures in a very ugly way:

>>> :t test
test
  :: (A :> es, (B :> es, (C :> es, () :: Constraint))) => Eff es ()

But previous releases print it normally:

>>> :t test
test :: (A :> es, B :> es, C :> es) => Eff es ()

I'd consider that a regression though, I'll make a ticket on the GHC bug tracker.

[arybczak]

Bikeshedding time. :>>, :<, :->, <:? Or something else? Not a fan of :< though, I prefer happy operators :joy:

<: is quite nice since it looks a bit like inclusion. But :>> is similar to :>.

⊆ would be great, but that isn't going to fly, too inconvenient to type.

[sproott]

I am against just using the flipped version <: because that could be confusing. I just used ::> and remember it like having more things on the left side. But :>> is also alright to me.

[arybczak]

Fixed by 938550b784269855dcc2a77a29fc3bbfe181be73.

BTW, the GHC ticket is here: https://gitlab.haskell.org/ghc/ghc/-/issues/20974

It'll be fixed, so everything works out :+1:

[arybczak]

Sadly I have to remove this (see #101 for explanation) for the sake of good long-term user experience in terms of compilation times.

[mmhat]

Maybe we could re-open this issue then and mark it as blocked by the GHC issue? Just to keep track of it and signal to users that we actually want this feature...

[arybczak]

Fair enough. I decided to deprecate it for now and only remove it in 3.0.0.0 to ease the transition period for people who were writing type signatures with it.

[Kleidukos]

Thank you @arybczak for shedding light on this flaw. I wonder if by chance we could have :>> rewritten to use :> via the compiler plugin?

[arybczak]

That maybe could work, but compiler plugins come with their own set of problems, so I'm reluctant to use them for this.

[oberblastmeister]

We could try manually generating cases of the type family (up to some limit)

type family Effs effs es :: Constraint where
  Effs '[] es = ()
  Effs '[e1, e2] es = (e1 :> es, e2 :> es)
  Effs '[e1, e2, e3] es = (e1 :> es, e2 :> es, e3 :> es)
  Effs '[... en] es = (... en :> es)

This is used in fastsum. We could run the template-haskell as code generation so we don't need to depend on it.

[arybczak]

That would be much better than recursive definition, but there's still some overhead when compared to direct usage of :> (when you look at Core).

Also, I just realized that -Wredundant-constraints doesn't work with :>>, i.e. it won't tell you if any effects on the list are redundant :thinking:

[sproott]

Also, I just realized that -Wredundant-constraints doesn't work with :>>, i.e. it won't tell you if any effects on the list are redundant thinking

I'm thinking in order to get support for this, it would have to probably be specifically added to the compiler plugin too, right? I don't think we can expect GHC to evaluate type families producing constraints in every case in order to find redundant ones.

(It's probably not even possible in some cases where the constraints produced depend on a type parameter.)

[arybczak]

Ok, so I benchmarked it by measuring compilation times and Core sizes of 50 functions that look like this:

testN :: [E1, ..., E21] :>> es => Eff es ()
testN = do
  send E21
  ...
  send E1

Here are results for 50 functions that use 11 effects each:

:>> recursive

Result size of Tidy Core
  = {terms: 18,595, types: 50,727, coercions: 56,809, joins: 0/0}

Compilation time: 2.1s

:>> unrolled

Result size of Tidy Core
  = {terms: 17,545, types: 41,777, coercions: 16,609, joins: 0/0}

Compilation time: 1.8s

:>

Result size of Tidy Core
  = {terms: 17,495, types: 17,627, coercions: 7,909, joins: 0/0}

Compilation time: 1.66s

So a slowdown of 8% and 16% respectively.

and for 50 functions that use 21 effects each:

:>> recursive

Result size of Tidy Core
  = {terms: 35,095, types: 136,727, coercions: 169,809, joins: 0/0}

Compilation time: 3.8s

:>> unrolled

Result size of Tidy Core
  = {terms: 33,045, types: 109,277, coercions: 41,109, joins: 0/0}

Compilation time: 3.1s

:>

Result size of Tidy Core
  = {terms: 32,995, types: 32,627, coercions: 14,409, joins: 0/0}

Compilation time: 2.6s

A slowdown of 16% and 46% respectively.

So:

Pros:

• Shorter type signatures.

Cons:

• Significantly longer compilation times (multiply the additional time by 100 or more if you have a reasonably large application)
• -Wredundant-constraints doesn't work.

I can't say I'm a fan of leaving this in.

[goertzenator]

I'm porting a codebase from cleff to effectful and am running into deprecated :>> issues. The code has stuff like this...

type AppE = '[Effect1, Effect2, Effect3]
myFunction1 = AppE :>> es => Eff es Int
myFunction2 = (Effect4 ': AppE) :>> es => Eff es Int

Is there some analog to AppE I can achieve with just :>, or do I have to hand-unroll all the constraints everywhere AppE is used?

[arybczak]

Is there some analog to AppE I can achieve with just :>

What about type AppE es = (Effect1 :> es, Effect2 :> es, Effect3 :> es)? :slightly_smiling_face:

[goertzenator]

Thanks, that did the trick! I didn't know about the ConstraintKinds extension before. Now I do.

The conversion from cleff went well. I liked cleff, but the compiler plugin no longer works on current ghc.