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.
CodePudding user response：
This is already addressed by Eugenio Moggi's 1991 seminal paper, "Notions of computation and monads." Here's a link: http://www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf
In particular, Section 2.3 explains how to interpret a simple programming language based on lambda-calculus in a monadic framework. Note that it doesn't matter if you add return, >>= etc; it's the semantics you give to your expressions and statements that are monadic. Haskell makes this explicit by separating the "pure" parts from the "monadic" parts in a syntactically nice way, whereas ML/Scheme etc. make it "convoluted" by keeping both look the same in the type system, but allow interpretations over suitable monads.