Making function as parameter polymorphic

[flip111]

Is there any way to rewrite a function such as

runState :: s -> Eff (State s ': es) a -> Eff es (a, s)

So that the second parameter Eff (State s ': es) a can be of a polymorphic variant State s :> es?
Just simply putting State s :> es doesn't work because it will also put the constraint on the resulting value es in Eff es (a, s).

It's important because when the input function Eff (State s ': es) a can not be polymorphic than it effects other parts of the codebase as well.

[evanrelf]

The second parameter being concrete is by design. The order of effects should remain abstract throughout your program, except when you are popping one of them off the stack, if you will. In other words, the order is determined by the order of the run* functions.

I think this is only a "problem" if you are relying on the concrete ordering of effects elsewhere in the codebase, which I believe is an anti-pattern.

[flip111]

@evanrelf thanks for the help. I don't think i'm understanding it. Especially in combination with #204 which was solved with the plugin for the easier case.

The second parameter being concrete is by design.

I think i should have been more clearer. Not to change the design of the effectful library but to let runState accept a polymorphic value.

In the other ticket #204 Shows i CAN use a polymorphic Eff (bar returns with (State v :> es, Error e :> es) => Eff es a) to pass it to a concrete Eff (State v : Error e : es) a.

Here a part of my code

type Eval es v = (Error EvalMonadError :> es, State (EvalMonadState v) :> es)

evalProg :: forall es v. (EvalTarget v) => [Proc] -> [v] -> String -> [v] -> Eff (Error String : es) (StateMachine v, [v])
evalProg procs vs main args =
  let x :: Eval es v => Eff es [v] = (evalProc @v @es) main args
  in  runProg procs vs x -- Line 37: How to let runProg accept an x with constraints?
-- Also tried: in  (runProg @es @v) procs vs x

evalProc :: forall v es. EvalTarget v => Eval es v => String -> [v] -> Eff es [v]
evalProc = undefined -- < .. snip .. more code ..>

runProg :: forall es a v b. [Proc] -> [v] -> Eff (State (EvalMonadState v) : Error EvalMonadError : es) a -> Eff (Error EvalMonadError : es) (StateMachine v, a)
runProg procs vs f = do
  r <- raise $ runError (runState init_state f) -- raise because want to create a new Error some lines later
  -- < .. snip .. more code ..>

    • Couldn't match type ‘es’
                     with ‘State (EvalMonad.EvalMonadState v)
                             : Error EvalMonad.EvalMonadError : es’
      Expected: Eff
                  (State (EvalMonad.EvalMonadState v)
                     : Error EvalMonad.EvalMonadError : es)
                  [v]
        Actual: Eff es [v]
      ‘es’ is a rigid type variable bound by
        the type signature for:
          evalProg :: forall (es :: [(* -> *) -> * -> *]) v.
                      EvalTarget v =>
                      [Proc]
                      -> [v]
                      -> String
                      -> [v]
                      -> Eff (Error String : es) (StateMachine v, [v])
        at testing/Eval.hs:34:1-122
    • In the third argument of ‘runProg’, namely ‘x’
      In the expression: runProg procs vs x
      In the expression:
        let x :: Eval es v => Eff es [v] = (evalProc @v @es) main args
        in runProg procs vs x
    • Relevant bindings include
        x :: Eval es v => Eff es [v] (bound at testing/Eval.hs:36:7)
        args :: [v] (bound at testing/Eval.hs:35:24)
        vs :: [v] (bound at testing/Eval.hs:35:16)
        evalProg :: [Proc]
                    -> [v]
                    -> String
                    -> [v]
                    -> Eff (Error String : es) (StateMachine v, [v])
          (bound at testing/Eval.hs:35:1)
   |        
37 |   in  runProg procs vs x
   |                        ^

The only solution i see here it to let evalProc return a concrete type instead of Eval es v => Eff es [v]. That would mean that lot of other functions can also not return polymorphic/constrained values anymore because of how these functions call each other. Is it correct? Should i make all the library return concrete values. Or can i use polymorphic somehow like in #204 ?

[flip111]

@evanrelf someone else had a look at it as well. We didn't solve it but this was the comment

we have x :: (Error EvalMonadError :> es, State (EvalMonadState v) :> es) => Eff es [v]
and runProg expects a value of type Eff (State (EvalMonadState v) : Error EvalMonadError : es) [v]
these two 'es' are not the same
so let's say that runProg expects an Eff (State (EvalMonadState v) : Error EvalMonadError : es2) [v]
'es2' is the list 'es' without those Error EvalMonadError and State (EvalMonadState v) effects
a plain 'inject' there doesn't work because GHC is not smart enough to work out this subset relationship by itself
in particular it seems that here the Subset class

effectful/effectful-core/src/Effectful/Internal/Effect.hs

Lines 74 to 101 in 2037be9

	class KnownPrefix es => Subset (xs :: [Effect]) (es :: [Effect]) where
	subsetFullyKnown :: Bool
	subsetFullyKnown =
	-- Don't show "minimal complete definition" in haddock.
	error "subsetFullyKnown"
	reifyIndices :: [Int]
	reifyIndices =
	-- Don't show "minimal complete definition" in haddock.
	error "reifyIndices"
	-- If the subset is not fully known, make sure the subset and the base stack
	-- have the same unknown suffix.
	instance {-# INCOHERENT #-}
	( KnownPrefix es
	, xs `IsUnknownSuffixOf` es
	) => Subset xs es where
	subsetFullyKnown = False
	reifyIndices = []
	-- If the subset is fully known, we're done.
	instance KnownPrefix es => Subset '[] es where
	subsetFullyKnown = True
	reifyIndices = []
	instance (e :> es, Subset xs es) => Subset (e : xs) es where
	subsetFullyKnown = subsetFullyKnown @xs @es
	reifyIndices = reifyIndex @e @es : reifyIndices @xs @es

is defined the "other way round"
it expects the top few items from the argument's effect list to occur somewhere inside the result list
but in your case it's the other way round
maybe the GHC plugin works only if the lists are monomorphic, i.e. statically known?

Also tried putting an inject

evalProg :: forall es v. (EvalTarget v) => [Proc] -> [v] -> String -> [v] -> Eff (Error String : es) (StateMachine v, [v])
evalProg procs vs main args =
  let x :: Eval es v => Eff es [v] = (evalProc @v @es) main args
  in  (runProg @es @v) procs vs $ inject x

no joy

    • Could not deduce (Error EvalMonad.EvalMonadError :> es)
        arising from a use of ‘evalProc’
      from the context: EvalTarget v
        bound by the type signature for:
                   evalProg :: forall (es :: [(* -> *) -> * -> *]) v.
                               EvalTarget v =>
                               [Proc]
                               -> [v]
                               -> String
                               -> [v]
                               -> Eff (Error String : es) (StateMachine v, [v])
        at testing/Eval.hs:34:1-122
    • In the expression: (evalProc @v @es) main args
      In a pattern binding:
        x :: Eval es v => Eff es [v] = (evalProc @v @es) main args
      In the expression:
        let x :: Eval es v => Eff es [v] = (evalProc @v @es) main args
        in (runProg @es @v) procs vs $ inject x
   |        
36 |   let x :: Eval es v => Eff es [v] = (evalProc @v @es) main args
   |                                       ^^^^^^^^

[jhgarner]

I think using a separate es2 is on the right track. The following code compiles for me (with stubs tossed in for the extra types). The interesting change is on the let x =.... line. The trick is making sure that x works with any effect stack instead of forcing it to be something specific. I also had to change the type signature of runProg slightly to get the same error as you. I'm guessing that was a typo, but let me know if not.

type Eval es v = (Error EvalMonadError :> es, State (EvalMonadState v) :> es)

evalProg :: forall es v. EvalTarget v => [Proc] -> [v] -> String -> [v] -> Eff (Error String : es) (StateMachine v, [v])
evalProg procs vs main args =
  let x = ((evalProc @v @es2) main args :: forall es2. Eval es2 v => Eff es2 [v])
   in runProg procs vs x -- Line 37: How to let runProg accept an x with constraints?
  -- Also tried: in  (runProg @es @v) procs vs x

evalProc :: forall v es. EvalTarget v => Eval es v => String -> [v] -> Eff es [v]
evalProc = undefined -- < .. snip .. more code ..>

runProg :: forall es a v b. [Proc] -> [v] -> Eff (State (EvalMonadState v) : Error EvalMonadError : es) a -> Eff (Error String : es) (StateMachine v, a)
runProg procs vs f = do
  -- r <- raise $ runError (runState (init_state @v) f) -- raise because want to create a new Error some lines later
  undefined
-- < .. snip .. more code ..>

[flip111]

Hey thanks a lot. Putting the type of x on the right is definitely helpful. In one of my attempts i tried to use forall but i didn't know i was not allowed to put it in the pattern match part (left hand side of =). It makes sense to me that x needs to be typed with another es2, i hope next time i can recognize this situation myself. This fixed the problem for me.

I also had to change the type signature of runProg slightly to get the same error as you.

Your version is the same because of this definition that i omitted type EvalMonadError = String

In general, for someone else who is finding this issue, i would suggest that if function produce a different Eff effect stack to give the es type variables different names perhaps type errors will become clearer as well. Forall is also necessary in this case.