如何扩展简单类型的lambda演算来拥有支持monad类型的类型系统?基本上，我现在对简单类型的lambda演算有了很好的理解，我想了解"最低要求"。在此基础上添加单子。通过"添加单子"我的意思是任何会导致语言具有操作语义和类型赋值的东西，允许人们识别"有用"。在某种程度上，是程序的单子。例如，Haskell在合理的意义上支持单子，即使它不要求程序员完全证明他们的单子。实例实际上遵守单子规则。
我希望了解一些扩展STLC与单子的最小方法，以便更多地了解与编程语言理论有关的单子。就我个人而言，我发现在一个更简单/基本的环境中学习这些东西更容易(而不是在像haskell这样的语言中实际使用它们)。由于这个原因，我不能给出比我上面写的更精确的描述我在寻找什么。
编辑，关于@Ben的评论:你能不能有一些设置，你有一个"原子"的签名;单子M，然后你的简单类型T现在是:
T=σ|T<子>1→T<子>2|mT
其中σ是原子类型签名中的一个原子类型，而m是m的一个元素。
也许你还可以在微积分项中加入常数项
t=x|t<子>1t<子>2|λx。t|返回t|t<子>1祝辞祝辞=t<子>2美元
我不确定这些是否有效，但看起来像这样的事情是可能的。
Eugenio Moggi在1991年的开创性论文《计算和单子的概念》中已经解决了这个问题。这里有一个链接:http://www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf
特别地，第2.3节解释了如何在一元框架中解释基于lambda演算的简单编程语言。请注意，如果你添加return,>>=等并不重要;它是你赋予一元的表达式和语句的语义。Haskell通过将"纯净"one_answers";部分来自"一元"。而ML/Scheme等则使其"错综复杂"。通过在类型系统中保持两者看起来相同，但允许在合适的单子上进行解释。