How can one extend simply typed lambda calculus to have a type system that supports something like a monad type? Basically, I presently have a nice understanding of simply typed lambda calculus, and I'd like to understand the "minimal requirements" to add monads to that foundation. By "adding monads" I mean anything that would result in a language with an operational semantics and type assignment that allows one to recognize the "usefulness" of monads for programs, to some extent. For example, Haskell supports monads in reasonable sense even though it doesn't require the programmer to fully prove that their "monad" instance actually abides by the monad laws.
I'm hoping to understand some minimal way of extending STLC with monads in order to learn more about monads in relation to programming language theory. Personally, I find it easier to learn these things in a more stripped down/essential setting (as opposed to just using them in practice in a language like haskell). For this reason, I can't give any more of a precise description of what I'm looking for, than what I wrote above.
Edit, with regard to @Ben's comment: could you not have some kind of setup where you have a signature of "atomic" monads M, and then your simple types T are now:
T = σ | T1 → T2 | m T
where σ is an atomic type from the signature of atomic types, and m is an element of M.
And then maybe you also add constant terms to the lambda calculus terms:
t = x | t1 t2 | λ x.t | return t | t1 >>= t2$
I'm not sure if any of this would work, but it seems like something like this would be possible.