小编ttb*_*tbo的帖子

如何扩展简单类型的 lambda 演算以拥有支持类似 monad 类型的类型系统？基本上，我目前对简单类型的 lambda 演算有很好的理解，并且我想了解将 monad 添加到该基础的“最低要求”。通过“添加 monad”，我的意思是任何会产生具有操作语义和类型分配的语言，允许人们在某种程度上识别 monad 对程序的“有用性”。例如，Haskell 在合理的意义上支持 monad，即使它不要求程序员完全证明他们的“monad”实例实际上遵守 monad 定律。

我希望了解一些使用 monad 扩展 STLC 的最小方法，以便更多地了解与编程语言理论相关的 monad。就我个人而言，我发现在更精简/基本的环境中学习这些东西更容易（而不是仅仅在像 haskell 这样的语言中在实践中使用它们）。出于这个原因，除了我上面写的内容之外，我无法对我正在寻找的内容进行更准确的描述。

编辑，关于@Ben 的评论：你能不能有某种设置，你有一个“原子”单子M的签名，然后你的简单类型T现在是：

T = ? | Ť ₁？T ₂ | 米 Ť

在哪里？是来自原子类型签名的原子类型，并且m是M的元素。

然后也许您还向 lambda 演算项添加常数项：

t = x | t ₁ t ₂ | ? ×。吨| 返回t | t ₁ >>= t ₂ $

我不确定这是否可行，但看起来像这样的事情是可能的。