Effects and linear types

[mmhat]

I've been looking into the linear types that came with GHC 9 lately and I wondered if the following was possible:
If I was sending a dynamically dispatched effect, can we provide a type-level guarantee that this effect is handled exactly once? I.e.

send :: (HasCallStack, e :> es) => e (Eff es) a %1 -> Eff es a
type EffectHandler e es = forall a localEs. HasCallStack => LocalEnv localEs -> e (Eff localEs) a %1 -> Eff es a
interpret :: EffectHandler e es %1 -> Eff (e : es) a -> Eff es a

Note that this is trivial for statically dispatched effects.
Besides that it might be interesting if there are other parts in effectful where linear types might be beneficial.

[arybczak]

can we provide a type-level guarantee that this effect is handled exactly once?

What do you mean by this?

Also, my understanding of LinearTypes is superficial at best, but I didn't get into it very much because:
a) implementation in GHC 9.0 is experimental and buggy,
b) nothing in base is multiplicity polymorphic, so there is no infrastructure and you have to reinvent everything.

Besides that it might be interesting if there are other parts in effectful where linear types might be beneficial.

The only thing I'm aware of would be unsafeConsEnv and unsafeTailEnv. As it stands now, if you do es' <- unsafeConsEnv es, then you can't use es until you call unsafeTailEnv es' or you'll get garbage results and/or a segmentation fault, but it's not checked at all.

[mmhat]

What do you mean by this?

Ok, that was not the best phrasing 😄 What I mean is: Can we provide functions with the type signatures that I listed in my comment?

I totally agree that LinearTypes is in an early state and not supported widely; IMHO it is not yet the right time to use those throughout effectful-core/effectful. Right now it is more of a research topic to me; I try to evaluate at what point LinearTypes can be useful in the context of an effect system and effectful in particular.

The only thing I'm aware of would be unsafeConsEnv and unsafeTailEnv.

Thank you for the pointer; I was not aware of those.

[mmhat]

@arybczak If you don't mind I suggest to keep this issue open to track this effort which may lead to a new companion library (linear-effectful ?) providing the linear version of send, interpret, etc.

[arybczak]

Sure. But I still don't think it's worth it. In particular:

send :: (HasCallStack, e :> es) => e (Eff es) a %1 -> Eff es a

This means "send uses the effect operation exactly once". It trivially does, it just passes it to the effect handler, the function is a couple of lines long.

type EffectHandler e es = forall a localEs. HasCallStack => LocalEnv localEs -> e (Eff localEs) a %1 -> Eff es a

This means "the effect handler uses the effect operation exactly once". Well, it has to use it at least once, since otherwise it won't produce the result. What happens if it uses it more than once?

interpret :: EffectHandler e es %1 -> Eff (e : es) a -> Eff es a

This means "interpret uses the effect handler exactly once". Once again, it trivially does, the function is a couple of lines long.

As for unsafeConsEnv/unsafeTailEnv, I think you'd need to make the Eff a linear state monad in order to pull that off.