"Shadowing" Handles

[maralorn]

This is not a pressing matter, but I am bringing it up in the interest of keeping the discussion from ghc-proposals/ghc-proposals#621 (comment) going.

In playing around with bluefin I noticed that it is hard to express that an effect must not be allowed at some place, while other effects can. I think this came up for me while writing a terminal UI. Imagine I have two effects ReadWrite and NCursesUI. The handler of NCursesUI needs the ReadWrite effect

runNCursesUI :: (e :> es) => ReadWrite e -> (forall eui. NCursesUI eui -> Eff (es :& eui) r) -> Eff es r

I find it hard get the effect tags right so that

a) arbitrary effects can be passed through to the inner action.
b) the inner action cannot use the ReadWrite handle directly (because that would most likely screw the UI output)

I realize that this is a strong requirement and a) more or less makes b) impossible already on a theoretical level. But I thought that maybe having the ReadWrite handle be linear could make sure that it is only used by exactly one handler.

Tangentially: I tried expressing in some way, that runNCursesUI plucks e out of es:

runNCursesUI :: ReadWrite e -> (forall eui. NCursesUI eui -> Eff (es :& eui) r) -> Eff (e :& es) r

but this does not prevent the caller from putting e into es on the outside anyway and it also makes this handler inconvenient to use because it suddenly restricts the effect order in the tag.

[tomjaguarpaw]

Ah indeed, I was going to suggest universally quantifying es to restrict the effects accessible in the inner action to a known set, but if you truly want "arbitrary" effects except the ReadWrite then I think you need linear types. It would be something like

runNCursesUI ::
  ReadWrite e %1 ->
  (forall eui. NCursesUI eui -> Eff (es :& eui) r) ->
  Eff (e :& es) (ReadWrite e, r)

This can actually be done with Bluefin and GHC as they currently are. It might be a bit tedious because you have to manually thread the ReadWrite, but it is possible. I believe the linear constraints proposal will make it less tedious, because you would not have to thread the ReadWrite. Instead it could be an unrestricted function argument, and the linear constraint that allows it to be used would be implicitly threaded.