Consolidate stateT to extlib?

[elefthei]

Why is state and stateT defined both in ext-lib and Basics.v
https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/Monads/StateMonad.v
https://github.com/DeepSpec/InteractionTrees/blob/master/theories/Basics/Basics.v

[Lysxia]

In hindsight I agree it's worth switching to ext-lib's definition, if only to make things less confusing.

My thought at the time was that ext-lib's stateT was meant to mimick the StateT newtype in Haskell, but in Coq newtypes are not really necessary since they can just as well be Definition, so I was experimenting with doing things this way. In the end I think it's more trouble than it's worth, and a stronger distinction between stateT and its unfolding may actually be quite useful in places.

[elefthei]

I am indifferent to newtype vs definition, maybe I slightly prefer definition because it requires one less constructor to keep track of. But I do have strong preference for no duplication, if that seems reasonable I can fix on the next version (not sure when this will be)

[gmalecha]

The motivation for the constructor was to aid in error messages. When writing monadic computations, having an extra lamba is something that is not very uncommon when changing code and getting a good error message is very useful.

[elefthei]

This makes sense, thanks for the clarification! Will keep ext-lib stateT and import it in InteractionTrees

[laelath]

Sorry to bump an old issue, but I would agree that switching to the ext-lib monad definitions would make things easier. I would also advocate for readerT and writerT also getting consolidated. I lost at least an hour trying to figure out why I was getting errors trying to use run_state in what I thought was a pretty straightforwards way (not helped by Coq's typeclass failure errors being a bit hard to parse).

[Lysxia]

The main challenge is to find the bandwidth to do it. I'll be happy to accept a PR.