Incorporate something like lifted-async's Pure constraint

[enolan]

lifted-async's Control.Concurrent.Async.Lifted.Safe module has a Pure class that requires the monad satisfy StM m a ~ a i.e. there is no state to restore. It's used to ensure that monadic computations run in async threads don't have state that would be dropped.

I think this is generally useful functionality that should be in monad-control, although I'll confess to not fully understanding the type hackery.

[basvandijk]

Interesting. I also don't understand the type hackery yet. For example I'm wondering why the following:

async :: forall m a. (MonadBaseControl IO m, Forall (Pure m)) => m a -> m (Async a)

can't be simplified to:

async :: forall m a. (MonadBaseControl IO m, StM m a ~ a) => m a -> m (Async a)

It probably has something to do with the quantification of a.

Anyway, it seems like Pure is a useful concept. If we're going to move it over to monad-control we have to do a coordinated release with lifted-async to enable a smooth transition.

@maoe as the author of lifted-async, what are your thoughts on this?

[maoe]

@basvandijk Yes, the type hackery is related to the quantification of a. Without the help of constraints package, we can't write the Applicative instance for Concurrently because e.g. pure :: Applicative f => a -> f a can have no constraints on a.

Ideally GHC should accept something like

instance (MonadBaseControl IO m, forall a. (StM m a ~ a)) => Applicative (Concurrently m) where ...

but that would require quantified contexts.

I'd be happy if Pure (or equivalent with different name) was incorporated upstream.

It's probably worth mentioning that there's an opportunity for bike shedding. There are equivalent of Pure out there:

• https://ro-che.info/articles/2017-06-04-universally-stateless-monads uses Stateless
• monad-unlift uses Identical

I personally prefer Stateless or Pure for backward-compatibility but people may have different taste.

[basvandijk]

@maoe thanks for the explanation.

I would prefer the name Stateless over Pure because it's more relatable to StM.

@enolan care to submit a PR to bring this into monad-control?

[basvandijk]

@feuerbach you might be interested in this as well.

[UnkindPartition]

I think at this point we should ask whether, even if this functionality is added, monad-control can add something over monad-unlift or unliftio.

[phadej]

I started a work in https://github.com/basvandijk/monad-control/compare/unlift branch.

There's also https://github.com/basvandijk/monad-control/compare/unlift

I don't like Identical hack of monad-control. It can be done in less hacky way:

class MonadTransControl t => MonadTransUnlift t where
  sttIsId :: Proxy t -> StT t a :~: a
  default sttIsId :: (StT t a ~ a) => Proxy t -> StT t a :~: a
  sttIsId _ = Refl

  withUnlift :: Monad m => (Unlift t -> m a) -> t m a
  withUnlift action = liftWith (\unlift -> action (\ma -> coe $ unlift ma))
    where
      coe :: forall b n. n (StT t b) -> n b
      coe = case sttIsId (Proxy :: Proxy t) :: StT t b :~: b of
          Refl -> id

type Unlift t = forall n b. Monad n => t n b -> n b

Also QuantifiedConstraintsdon't work, so the above is something I'd experiment with. I expect that in practice everyone would use (and define) withUnlift, and sttIsId is there just to make it harder to cheat.

[phadej]

Also https://github.com/basvandijk/monad-control/issues/39 is another approach. Where StM m ~ Identity would be essentially the same as having MonadBaseUnlift. Which means we would only need to define combinators (but redefine instances). I'll experiment with that too.