有没有简单的方法可以用 monad 类型扩展简单类型的 lambda 演算？

Question

如何扩展简单类型的 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 ₂ $

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

Answer 1

Eugenio Moggi 1991 年的开创性论文“计算和单子的概念”已经解决了这个问题。这是一个链接：http : //www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf

特别是，第 2.3 节解释了如何在 monadic 框架中解释基于 lambda 演算的简单编程语言。请注意，如果你加也没关系return，>>=等; 这是您赋予表达式和语句的语义，它们是一元的。Haskell 通过以一种语法上很好的方式将“纯”部分与“一元”部分分开来使这一点变得明确，而 ML/Scheme 等通过在类型系统中保持两者看起来相同来使其“复杂”，但允许解释过度合适单子。