有没有简单的方法可以用 monad 类型扩展简单类型的 lambda 演算？
Is there simple way to extend simply typed lambda calculus with monad types?
如何扩展简单类型的 lambda 演算以拥有支持类似 monad 类型的类型系统？基本上，我目前对简单类型的 lambda 演算有了很好的理解，并且我想了解将 monad 添加到该基础的“最低要求”。通过“添加 monad”，我的意思是任何会产生一种语言的操作语义和类型分配，允许人们在某种程度上识别 monad 对程序的“有用性”。例如，Haskell 在合理的意义上支持 monad，即使它不需要程序员完全证明他们的“monad”实例实际上遵守 monad 法则。
我希望了解一些使用 monad 扩展 STLC 的最小方法，以便了解更多关于与编程语言理论相关的 monad。就个人而言，我发现在更简单的 down/essential 设置中学习这些东西更容易（而不是仅仅在实践中使用像 haskell 这样的语言）。出于这个原因，除了上面写的内容，我无法对我正在寻找的内容进行更准确的描述。
编辑，关于@Ben 的评论：你能不能有某种设置，你有一个“原子”单子的签名M，然后你的简单类型T 现在是：
T = σ | T1 → T2 | m T
其中σ是原子类型签名中的原子类型，m是M的一个元素.
然后也许您还可以将常数项添加到 lambda 演算项中：
t = x | t1 t2 | λ x.t | return t | t1 >>= t2$
我不确定这是否可行，但看起来像这样的事情是可能的。
Eugenio Moggi 1991 年的开创性论文“计算概念和单子”已经解决了这个问题。这是 link：http://www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf
特别是，第 2.3 节解释了如何在单子框架中解释基于 lambda 演算的简单编程语言。请注意，是否添加 return、>>= 等并不重要；这是你赋予表达式和语句的语义，它们是一元的。 Haskell 通过在语法上很好的方式将“纯”部分与“单子”部分分开来使其明确，而 ML/Scheme 等通过在类型系统中保持两者看起来相同使其“复杂” , 但允许对合适的单子进行解释。
如何扩展简单类型的 lambda 演算以拥有支持类似 monad 类型的类型系统？基本上，我目前对简单类型的 lambda 演算有了很好的理解，并且我想了解将 monad 添加到该基础的“最低要求”。通过“添加 monad”，我的意思是任何会产生一种语言的操作语义和类型分配，允许人们在某种程度上识别 monad 对程序的“有用性”。例如，Haskell 在合理的意义上支持 monad，即使它不需要程序员完全证明他们的“monad”实例实际上遵守 monad 法则。
我希望了解一些使用 monad 扩展 STLC 的最小方法，以便了解更多关于与编程语言理论相关的 monad。就个人而言，我发现在更简单的 down/essential 设置中学习这些东西更容易（而不是仅仅在实践中使用像 haskell 这样的语言）。出于这个原因，除了上面写的内容，我无法对我正在寻找的内容进行更准确的描述。
编辑，关于@Ben 的评论：你能不能有某种设置，你有一个“原子”单子的签名M，然后你的简单类型T 现在是：
T = σ | T1 → T2 | m T
其中σ是原子类型签名中的原子类型，m是M的一个元素.
然后也许您还可以将常数项添加到 lambda 演算项中：
t = x | t1 t2 | λ x.t | return t | t1 >>= t2$
我不确定这是否可行，但看起来像这样的事情是可能的。
Eugenio Moggi 1991 年的开创性论文“计算概念和单子”已经解决了这个问题。这是 link：http://www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf
特别是，第 2.3 节解释了如何在单子框架中解释基于 lambda 演算的简单编程语言。请注意，是否添加 return、>>= 等并不重要；这是你赋予表达式和语句的语义，它们是一元的。 Haskell 通过在语法上很好的方式将“纯”部分与“单子”部分分开来使其明确，而 ML/Scheme 等通过在类型系统中保持两者看起来相同使其“复杂” , 但允许对合适的单子进行解释。