mtl icon indicating copy to clipboard operation
mtl copied to clipboard

mtl 3.0 planning

Open emilypi opened this issue 2 years ago • 12 comments

Per discussions with @ekmett and elsewhere

  • [ ] Factor MonadReader into Ask and Local classes
  • [ ] Factor MonadWriter into Tell and Listen, and Pass
  • [ ] Reduce constraints where applicative (i.e. FunctorTell, ApplicativeAsk)
  • [ ] Address Kmetto-senpai's reqeuest for laws and better docs
  • [ ] Clear the existing PR backlog
  • [ ] A proper ListT
  • [ ] Handler-like algebraic catch (see: https://paste.tomsmeding.com/aAYwOy7t)
  • [ ] etc...

Thoughts welcome

emilypi avatar May 08 '22 06:05 emilypi

MonadAccum would need to gain MonadAsk and MonadTell superclass constraints. I also feel we need to nail down precise laws, and restrict down some instances: for example, ContT r' (Reader r) is a MonadAsk, but not a MonadLocal as per #83.

kozross avatar May 08 '22 06:05 kozross

Also, does it make sense to crack MonadError into MonadThrow and MonadCatch, paralleling the design choices for exception-chucking classes?

kozross avatar May 08 '22 06:05 kozross

With regard to a proper ListT, in order for this to 'belong' sensibly in this package, we need something like MonadChoice or MonadNonDet (I favour the latter). The best design for this is basically the MonadLogic of logict (I literally can't think of another), and that comes with laws, which I appreciate. However, this would mean 'taking ownership' of the equivalent of two whole packages.

kozross avatar May 08 '22 07:05 kozross

add an update monad a la https://danel.ahman.ee/papers/types13postproc.pdf ?

gbaz avatar May 10 '22 17:05 gbaz

@gbaz I've considered this, but this would require a monoid action type class, which we'd also end up having to 'own'.

kozross avatar May 10 '22 18:05 kozross

Ooo dibs

emilypi avatar May 10 '22 20:05 emilypi

@emilypi If we decide to go this way, we definitely need to consider the fundep question. I personally favour 'action determines state'. It does mean we basically can't provide almost any instances, though.

kozross avatar May 10 '22 20:05 kozross

Uh. I have feelings about this. I've made several attempts and bounced off of the question of which which is approach is best for several reasons. On one hand, I hate biting the overlapping/overlappable/incoherent approach of using raw MPTC (i.e. Act a x ) without fundeps, because it becomes extremely easy to write nonsensical and conflicting instances for Endo x rather quickly.

The solution, if we were to go down the overlapping road, would be to backpack a la @ekmett's Deltas in coda. It would allow us to subclass particular actions relatively cleanly. But then we have to admit backpacking into the project and ahaha guess what problems we face then? Politics and nobody being able to build upon our work. AnD i aiN'T gOt TiME fOr thaT :DDDD

On the other hand, fundeps requires us to work with fundeps and proliferate a billion newtypes. I think if we were to go down that road, we'd have to commit to a set of core actions we care to support and let others write the actions-extras package that i'm not gonna maintain personally if they want to expand the repertoire.

Regardless, we also run into the problem into the problem of committing this to mtl or a package upstream of mtl and that's a tough sell.

emilypi avatar May 10 '22 20:05 emilypi

I strongly oppose any kind of typechecker soup arising from not having fundeps on a multi-param type class. The biggest pain for me is that the most natural such fundep (action determines state) means that certain 'obvious' instances become literally un-writeable. Consider more-or-less the canonical implementation of the functionality of MonadAsk, which would require something like instance Action () a: this falls apart immediately, since you're now asking () to determine basically everything. For what it's worth, this problem also arises in the other direction, and makes even less sense there.

I definitely don't know how I feel about such a cost: it essentially pushes all instances onto users. However, I'd rather that than the alternatives, which is typechecker slurry or significant complexity. I don't know in how far Backpack would help this, but this means becoming immediately incompatible with Stack, for example. While I don't really care much for Stack, and consider it useless in 2022, I don't think many people will agree with me, especially on a package as 'core' as mtl.

kozross avatar May 10 '22 21:05 kozross

Also, could we add 'laws and tests for these'? I'm already laying the groundwork, but it'd be nice to have that too.

kozross avatar May 10 '22 21:05 kozross

One thing I have wanted a few times is a MonadStateReadOnly superclass of MonadState (and I guess dually a MonadStateWriteOnly) so I can mark (in a compiler-checked way!) helper functions as "this will only read the state, not modify it". Whilst you can do this by writing functions over a reader monad and translating that into state, this is awkward and does not work if you are using a reader for something else already (e.g. a global environment for your state machine, or an IO action for logging purposes etc).

Unfortunately I don't actually know how feasible / sensible this factoring would be in practice.

brprice avatar Aug 31 '22 13:08 brprice

From chats with Ed, which would also affect transformers:

edwardk> type ContT :: forall k i o. k -> (k -> TYPE o) -> TYPE i -> Type
8:02 PM <edwardk> type ReaderT :: forall k i o. TYPE i -> (k -> TYPE o) -> k -> Type
8:04 PM <edwardk> type WriterT :: forall o. Type -> (Type -> TYPE o) -> Type -> TYPE o
8:04 PM <edwardk> type StateT :: forall o. Type -> (Type -> TYPE o) -> Type -> Type
8:05 PM <edwardk> type IO :: forall o. TYPE o -> Type
8:06 PM <edwardk> type ST :: forall o. Type -> TYPE o -> Type
8:07 PM <edwardk> type MaybeT :: forall o. (Type -> TYPE o) -> Type -> TYPE o
8:08 PM <edwardk> type ExceptT :: forall o. Type -> (Type -> TYPE o) -> Type -> TYPE o
8:08 PM <edwardk> type IdentityT :: forall k o. (k -> TYPE o) -> k -> TYPE o
8:09 PM <edwardk> type SelectT :: forall k o. k -> (k -> TYPE o) -> TYPE o -> Type
8:11 PM <edwardk> type Control.Monad.Trans.RWS.CPS.RWST :: forall i o. TYPE i -> Type -> Type -> (Type -> TYPE o) -> Type -> Type
8:12 PM <edwardk> type Control.Monad.Trans.RWS.RWST :: forall i o. TYPE i -> Type -> Type -> (Type -> TYPE o) -> Type -> Type
8:13 PM <edwardk> type AccumT :: forall o. Type -> (Type -> TYPE o) -> Type -> TYPE o

emilypi avatar Sep 02 '22 15:09 emilypi