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

Question

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

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

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

T = σ | T₁ → T₂ | m T

其中 σ 是原子类型签名中的原子类型，m 是 M 的元素。

然后也许您还可以将常数项添加到 lambda 演算项中:

t = x | t₁ t₂ | λ x.t |返回 t | t₁>>= t₂$

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

Answer 1

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

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