Is Members transitive?

[jgrosso]

This is a highly-simplified version of some Members constraints I'm working with (I think), and I guess I'm a bit confused why it can't compile.

foo :: (Sem.Members '[Sem.Reader Int] effs1, Sem.Members effs1 effs) => Sem.Sem effs ()
foo = Sem.ask @Int >> pure ()

Specifically, the error is:

    • Could not deduce: Polysemy.Internal.Union.IndexOf
                          effs10 (Polysemy.Internal.Union.Found effs10 (Sem.Reader Int))
                        ~ Sem.Reader Int
      from the context: (Sem.Members '[Sem.Reader Int] effs1,
                         Sem.Members effs1 effs)
...

Intuitively, shouldn't being a member of effs1 make Sem.Reader Int transitively a member of effs?

[KingoftheHomeless]

Unfortunately, this is not possible, as Members is only a simple type family to convert [e1, e2, e3, ...] into (Member e1 r, Member e2 r, Member e3 r, ...). Since effs1 is polymorphic, Members effs1 effs gets stuck, and the type checker can't figure out that Member (Reader Int) effs.

Actually, maybe it is possible to have Members be transitive; I have a trick in mind I can try out. But even if it were possible, I'm not sure if we want to complicate the definition of Members; it's only intended as simple sugar to avoid writing Member ... r for every needed effect.

[jgrosso]

Got it. Is there any workaround from the client-side perspective, do you know (regardless of how complex it might be)?

[isovector]

The easiest workaround is to just get rid of effs1 in the original problem. I'd be curious to see a more real-life example where you need this functionality --- I suspect there is an easy workaround, but it's hard to say without more details.

[KingoftheHomeless]

The trick I had in mind didn't pan out. I tried leveraging quantified constraints, and define Members like this (also requires UndecidableSuperclasses):

class (forall z. Members r z => Members es z, Members' es r) => Members es r
instance (forall z. Members r z => Members es z, Members' es r) => Members es r

type family Members' es r :: Constraint where
  Members' '[]       r = ()
  Members' (e ': es) r = (Member e r, Members' es r)

But for whatever reason, GHC still can't figure out the original example, and says that the use of Reader Int is ambiguous.

[isovector]

@KingoftheHomeless that's due to this: https://gitlab.haskell.org/ghc/ghc/issues/14860, i think

[KingoftheHomeless]

@isovector redefining it like this doesn't work either:

class (forall z. Members' r z => Members' es z, Members' es r) => Members es r
instance (forall z. Members' r z => Members' es z, Members' es r) => Members es r

class Members' (es :: [k]) (r :: [k])
instance Members' '[] r
instance (Member h r, Members' t r) => Members' (h ': t) r

or this:

type Members = Members'
class Members' (es :: [k]) (r :: [k])
instance Members' '[] r
instance (forall z. Members' r z => Member h z, Member h r, Members' t r) => Members' (h ': t) r

Then again, if type families trip up quantified constraints, then maybe the type families Member uses could also be part of the problem.

[jgrosso]

I tried to make an MVCE, and now I think my actual issue might be related to a combination of #114 and #188, not the transitivity of Members 😬. Specifically, this a simplified version of what I'm trying to do:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import qualified Polysemy as Sem
import qualified Polysemy.Reader as Sem
import qualified Polysemy.State as Sem

type Callback effs fn a
   = forall openEffs. (Sem.Members effs openEffs) =>
                        fn (Sem.Sem openEffs a)

type DependencyArgs a = a

type Dependency effs = Callback effs DependencyArgs Int

type FooCbArgs a = Int -> a

type FooCb effs = Callback effs FooCbArgs Int

injectedCb ::
     forall depEffs effs.
     ( Sem.Member (Sem.Reader Int) effs
     , Sem.Members depEffs (Sem.Reader String ': effs)
     )
  => Dependency depEffs
  -> FooCb effs
injectedCb dep x = Sem.runReader "" $ dep

foo ::
     forall cbEffs depEffs effs.
     ( Sem.Members cbEffs effs
     , Sem.Members depEffs effs
     , Sem.Members depEffs cbEffs
     )
  => Dependency depEffs
  -> (Dependency depEffs -> FooCb cbEffs)
  -> Sem.Sem effs Int
foo dep mkCb = mkCb dep 0

main :: IO ()
main = pure ()

and this is the error

• Could not deduce: Sem.Members
                      depEffs (Sem.Reader [Char] : openEffs)
    arising from a use of ‘dep’
  from the context: (Sem.Member (Sem.Reader Int) effs,
                     Sem.Members depEffs (Sem.Reader String : effs))
    bound by the type signature for:
               injectedCb :: forall (depEffs :: [(* -> *) -> * -> *]) (effs :: [(*
                                                                                 -> *)
                                                                                -> * -> *]).
                             (Sem.Member (Sem.Reader Int) effs,
                              Sem.Members depEffs (Sem.Reader String : effs)) =>
                             Dependency depEffs -> FooCb effs
    at app/Main.hs:(27,1)-(33,15)
  or from: Sem.Members effs openEffs
    bound by the type signature for:
               injectedCb :: Dependency depEffs -> FooCb effs
    at app/Main.hs:34:1-41
• In the second argument of ‘($)’, namely ‘dep’
  In the expression: Sem.runReader "" $ dep
  In an equation for ‘injectedCb’:
      injectedCb dep x = Sem.runReader "" $ dep
• Relevant bindings include
    dep :: Dependency depEffs (bound at app/Main.hs:34:12)
    injectedCb :: Dependency depEffs -> FooCb effs
      (bound at app/Main.hs:34:1)

34 | injectedCb dep x = Sem.runReader "" $ dep

If I should add this to #114, or open a new issue entirely, please let me know. (Sorry for the goose chase regarding Members transitivity!)

[isovector]

What's the intent here? I think Callback is too clever for the plugin/GHC, and that the Member givens aren't propagating properly.

[jgrosso]

@isovector My main goal was to have callbacks that could have arbitrary effects, such that the calling functions can absorb them without knowing explicitly what they are. (It did work pretty well – albeit a bit boilerplate-heavy – until I ran into this issue.)

[jgrosso]

In this specific case, I guess what I'm hoping for is to have callbacks that can themselves take callbacks, so to speak.

[isovector]

So the issue here is that you're saying that injectedCb works for any effect stack --- but that is not true, it only works for a Dependency whose openEffs starts with a Reader String. This really and truly is a type error!

The solution I think is to just be less clever. The constraint system is really good, and will propagate Member constraints from actual callbacks upwards as they get called.

FWIW to work this out, I inlined all of the type synonyms, and then lifted out the rank-2 stuff which is necessary. The error was clear at this point that you're trying to run a reader that doesn't exist. This gives us:

injectedCb ::
     forall depEffs effs openEffs.
     ( Sem.Member (Sem.Reader Int) effs
     , Sem.Members depEffs (Sem.Reader String ': effs)
     , Sem.Members depEffs openEffs
     , Sem.Members effs openEffs
     )
  => Sem.Sem (Sem.Reader String ': openEffs) Int
  -> Int
  -> Sem.Sem openEffs Int
injectedCb dep x = Sem.runReader "" $ dep

but now it's clear that none of those constraints are necessary, so the above simplifies down to

injectedCb
  :: Sem.Sem (Sem.Reader String ': openEffs) Int
  -> Int
  -> Sem.Sem openEffs Int
injectedCb dep x = Sem.runReader "" $ dep

[jgrosso]

Ohhh, I think my confusion had been from interpreting the openEffs in the error message as that of FooCb rather than Dependency... when you expand it all out, though, it makes a lot more sense (at least in a preliminary read) what's going wrong. I'm going to try this out tonight, thank you so much @isovector.

[jgrosso]

I guess one thing I'm still wondering about is, is there a way for dep to basically just ignore the runReader it's wrapped in? I think my original reason for using openEffs existentially was so that dep itself wouldn't need the Reader String effect. In this case it breaks down (as we've seen), but is there an alternate formulation that would work?

Sorry if the question doesn't make sense, I'm still trying to wrap my head around all this 😃

[isovector]

Sorry for the delay --- somehow missed this.

If you'd like to hide the Reader String effect, you can use raise, which will introduce a new, unused effect on top of the stack. This thing is analogous to lift from MTL.

For example, if you have a foo :: Sem r a you'd like to run alongside some bar :: Sem (Reader String ': r) b code, you could do this:

runReader "hello" $ do
  raise foo
  bar

[isovector]

FWIW, I'd recommend using Input instead of Reader unless you're certain that you need local :)

[expipiplus1]

@isovector out of interest, why is that?

[googleson78]

@expipiplus1

• Reader is higher-order - more things to think about
• If you aren't using some functionality what benefit does having it bring?

[bolt12]

Excuse my ignorance but when/why would I want to use local? It seems that it modifies the state of the Reader. Shouldnt we use something more like State for that?

[googleson78]

Personally I haven't used it, but I've imagined cases where I only need local, and not the full "power" of state (i.e. to be able to retain the change after a computation finishes)

Things that come to mind are

• having a trail of crumbs while traversing a tree, so you can know how you reached the place where you are now
• evaluating a function - you only need temporary (name, value) bindings for the arguments
• doing shifting when processing debruijn indices - you want to keep track of how deep you are, but you want to "unwind" once you go out of your recursive call

(after writing all these out I guess anything that's in the push, oper, pop pattern fits the bill)

The reason why it's in there in the first place I would guess is because transformers/mtl has it.. and it has it because.. it's just something you can do with a Reader? idk

[bolt12]

(after writing all these out I guess anything that's in the push, oper, pop pattern fits the bill)

Okay I think I got it with your examples, it seems useful indeed!

Thanks!

[bolt12]

Could Members be implemented as a type family similar to elem function? Why is it implemented the way it is?

[googleson78]

I haven't looked too much at how it's used, but my guess would be this:
With a type family you would lose all "backwards" information flow (because it's non-injective), so you would only be able to verify that programs that are fully specified are well-typed. The current implementation allows ghc to infer more things via constraint solving (?).

Another (and probably more important) thing that immediately comes to mind is that the current implementation also has runtime proof (the Here/There stuff), allowing you to recover which effect you are working with right now, and this would 100% be gone if you used only type families (unless you mean something that I am not aware of, like type families + some data)

@KingoftheHomeless (and/or Sandy) is a much better fit to answer the question tbh