Overlapping instances using paramerized effects

[aztecrex]

I would like to parameterize effects but they always lead to overlapping instances for me. A boiled-down example:

module Demo.OverlappingEffects where

import Control.Monad.Freer (Eff, Member, send)

data Box contents a where
    Receive :: Box contents [contents]
    Ship :: contents -> Box contents ()

-- | where we receive' a box of things and ship them out sep'rately
distribute :: forall contents effects. (Member (Box contents) effects) => Eff effects ()
distribute = do
    received <- receive'
    mapM_ ship' received
    where
        receive' = send Receive
        ship' c = send $ Ship c

But GHC tells me i'm being foolish:

    • Overlapping instances for Member (Box contents0) effects
      Matching givens (or their superclasses):
        Member (Box contents) effects
          bound by the type signature for:
                     distribute :: forall contents (effects :: [* -> *]).
                                   Member (Box contents) effects =>
                                   Eff effects ()
          at src/Demo/OverlappingEffects.hs:10:15-88
      Matching instances:
        instance (Data.OpenUnion.Internal.FindElem t r,
                  Data.OpenUnion.Internal.IfNotFound t r r) =>
                 Member t r
          -- Defined in ‘Data.OpenUnion.Internal’
      (The choice depends on the instantiation of ‘contents0, effects’)
    • In the ambiguity check for ‘distribute’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        distribute :: forall contents effects.
                      (Member (Box contents) effects) => Eff effects ()

I'm wondering if a) there is something I could do to my source to make this work e.g. move some qualifications around, b) this will forever be impossible with Freer-simple, please go away or, c) there is possibly a change to the Freer-simple implementation that would make this work.

If y'all think it's "c," I am happy to try to do the work. Not super confident in my type-level programming skills which is why I don't have a PR handy already.

Oh, and hi Alexis, I miss you.

[lexi-lambda]

I'm wondering if a) there is something I could do to my source to make this work e.g. move some qualifications around, b) this will forever be impossible with Freer-simple, please go away or, c) there is possibly a change to the Freer-simple implementation that would make this work.

I have only skimmed your code, so I may be wrong, but at first glance, my guess is that the answer is (a) in this case. Allow me to explain why.

With mtl, all the effect classes have a fundep, like class MonadReader r m | m -> r. This means there can only ever be one r per transformer stack, so if you have something like ReaderT A (ReaderT B) m a, you can only ever ask for an A, not a B (the outermost one wins). This is sometimes nice, since it improves type inference—the fact that there’s only one possible r means that a use of ask is always unambiguous. But it also leads to needing some ugly hacks to support compositional reader contexts. If you have some part of your application that needs an implicitly-bound Foo, and some other part that needs an implicitly bound Bar, you can’t use them together if they have constraints like MonadReader Foo m => and MonadReader Bar m =>.

One solution to this while staying in mtl-land is to use “classy mtl”, an allusion to so-called “classy lenses”. You generate classy lenses for your various datatypes, which generate classes like HasFoo and HasBar. Then you write things like (MonadReader r m, HasFoo r) => and (MonadReader r m, HasBar r) =>, and you use the lens to get the value out of some piece of implicit context that carries both of them around. This regains compositionality, but it isn’t perfect. Namely, you still can’t discharge the constraints individually (you still need to call runReaderT all in one go, so you can’t discharge the Bar-needing part separately from the Foo-needing part), and your types are now harder to read.

Freer monads take the approach of just allowing multiple versions of the same effect to show up in a stack. This means you can totally have an effect stack that contains Reader Foo and Reader Bar, and they don’t conflict! It just means that GHC needs a bit more help to figure out which one you want when you write ask (and unfortunately, it isn’t smart enough to just pick one when the choice is unambiguous within a particular scope).

Getting back to your code, you have a function receive' that is producing some [contents], but GHC doesn’t know which contents to use. This is because you write mapM_ ship' receive', which is kind of like writing show (read x). GHC won’t be able to figure out which Read instance to use because show doesn’t constraint the type of its argument, and the result of read is otherwise unused. Fortunately, you can help GHC out by adding a type annotation somewhere, so long as you have ScopedTypeVariables turned on:

distribute :: forall contents effects. (Member (Box contents) effects) => Eff effects ()
distribute = do
    received <- receive'
    mapM_ ship' (received :: [contents])
  where
    receive' = send Receive
    ship' c = send $ Ship c

Where exactly you put the annotation is arbitrary, so long as it’s enough to provide enough information to the typechecker to unify contentsreceive with contentsdistribute.

There’s also a clearer way as of GHC 8: use TypeApplications. This will just let you write receive' @contents, so long as the first quantified type variable in receive' is contents, not eff. To make sure this is the case, write the definition of receive' with an explicitly quantified type signature:

receive' :: forall contents eff. Member (Box contents) eff => Eff eff [contents]
receive' = send Receive

Now writing recieved <- receive' @contents should do the trick.

Oh, and hi Alexis, I miss you.

Hi to you, too. :) I miss you all as well! It’s nice to hear from you, even if just through a GitHub issue.

[lexi-lambda]

Oh, and I should probably also point out that this limitation isn’t normally as burdensome as it might seem. Generally, when you have something like Reader, you are going to actually use the value in a way that will cause GHC to infer the appropriate type, so you won’t need the type annotation. For example, if you write something like this:

do x <- ask
   pure $ not x

…then GHC will be able to figure out that x should be a Bool and therefore you are referring to a use of Reader Bool. In your case, GHC wasn’t able to do that because your distribute function is polymorphic over contents. The upshot to this is that, if you do a bit of extra work to explain to GHC how distribute should work, you can freely use the distribute function in an effect stack with many Box effects, since the caller will pick which contents to use.

[aztecrex]

Thanks. I should have checked GH again last night!

That didn't work for me unfortunately. I get the exact same error even with explicit signatures for ship' and receive' and explicitly typing received :: [contents]. One thing I don't understand is that the list of matching instances in the error message contains (at least the way i'm reading it) just one item.

[lexi-lambda]

Ah, you’re right! I actually took the time to run your example myself, and I realized there is something related but slightly different going on.

Let’s look at the type of distribute:

forall contents effects. (Member (Box contents) eff) => Eff eff ()

This type is, according to the Haskell standard, ambiguous. Why? Well, look at the type to the right of the =>, in this case Eff eff (). Notice that there is no occurrence of contents in that type. Therefore, how can GHC possibly know which contents should be chosen when distribute is called? Since the typeclass constraints are satisfied implicitly, there is no term-level value that determines which type to use for contents.

Prior to GHC 8, this was usually solved by adding a Proxy argument, like this:

import Data.Proxy (Proxy(..))

distribute :: forall contents effects. (Member (Box contents) effects) => Proxy contents -> Eff effects ()

Now, when we call distribute, we provide a Proxy value that is isomorphic to () at runtime but carries an additional piece of type information at compile-time. This works, but it’s a little ugly. With GHC 8, we can use TypeApplications to pick the type, so ambiguous types are actually okay. Therefore, we can enable AllowAmbiguousTypes to defer the ambiguity check to use-sites, then use TypeApplications to specify the type that should be used for contents when we call distribute.

With AllowAmbiguousTypes turned on, you’ll get a different ambiguity error in the body of distribute, at which point my original comment earlier in this thread applies. You’ll need to resolve the ambiguous call to receive' by writing receive' @contents, and at that point, your program will typecheck.

If this seems like too much work to have to do, consider what it is you’re asking of GHC. You’ve defined a polymorphic effect, but when you do receive' >>= mapM_ ship', you ask GHC to become an oracle and magically pick which type of thing should be received and shipped. Perhaps there’s an argument to be made here that you really do want the “one effect per stack” behavior of mtl for particular effects, but that feels to me like it could cause problems. It’s hard for me to say more without knowing more about what you’re actually doing.

[aztecrex]

I think I see why it can't work in this case.

My goal was to write a program that knows how to distribute anything, in the context of a shipping and receiving authority offering that protocol.

My hope was not that GHC would discern the type inside the polymorphic distribute, but that it could defer type selection until distribute was embedded in an actual shipping department with contents selected.

The workarounds are OK. I'll probably try the proxy solution first and fall back to AllowAmbiguousTypes depending on how the API of the actual code looks with proxy.

[lexi-lambda]

You might be able to get what you want with some sort of existential encoding. If you’d like, I’d be willing to chat via hangouts or something and talk more about what you’re trying to do—your problem sounds interesting! (And I got your email, just haven’t had a chance to respond to it, but I will soon.)

[aztecrex]

that would be great. mother's day is tomorrow and mondays at cj are, well, mondays at cj. i'll reach out via email and try to set something up this week.