1 回答
初步说明：我很抱歉在这个答案中花了很大一部分时间谈论 Propositional Lax Logic，这是一个您非常熟悉且就这个问题而言不太感兴趣的话题。无论如何，我确实觉得这个主题值得更广泛地曝光——感谢您让我意识到这一点！
命题松散逻辑 (PLL) 中的模态运算符是Monad类型构造函数的 Curry-Howard 对应物。注意它的公理之间的对应关系......
DT: x -> D x
D4: D (D x) -> D x
DF: (x -> y) -> D x -> D y
... 以及 , 和return的join类型fmap。
Valeria de Paiva 有许多论文讨论直觉模态逻辑，特别是 PLL。这里关于 PLL 的评论主要基于Alechina等。人。，建设性 S4 模态逻辑的分类和 Kripke 语义（2001 年）。有趣的是，那篇论文证明 PLL 不像最初看起来那么奇怪（参见Fairtlough 和 Mendler，Propositional Lax Logic (1997)：“作为模态逻辑，它很特别，因为它具有单个模态运算符 [. ..] 具有可能性和必要性的味道”）。从 CS4 开始，直觉主义 S4 的一个版本，没有在析取上分配可能性……
B stands for box, and D for diamond
BK: B (x -> y) -> (B x -> B y)
BT: B x -> x
B4: B x -> B (B x)
DK: B (x -> y) -> (D x -> D y)
DT: x -> D x
D4: B (B x) -> B x
...并添加x -> B x它会导致B变得微不足道（或者，用 Haskell 的话来说，Identity），简化了 PLL 的逻辑。既然如此，PLL可以被视为直觉S4变体的特例。此外，它将 PLLD定义为类似可能性的算子。如果我们将D其作为 Haskell 的对应物，这在直觉上很有吸引力Monad，它通常确实具有可能性的味道（考虑Maybe Integer——“这里可能有一个Integer”——或者IO Integer——“我会Integer在程序执行时得到一个”）。
其他几种可能性：
乍一看，似乎把
D琐碎化的对称动作引导我们到非常类似的东西ComonadApply。我说“非常喜欢”主要是因为 Haskell 的功能强大，如果您正在寻找传统的必要性模态Functor，这是一件尴尬的事情。x /\ B y -> B (x /\ y)Kenneth Foner 的Functional Pearl: Getting a Quick Fix on Comonads（感谢 dfeuer 的参考）致力于在 Haskell 中表达直觉主义的 K4，涵盖了沿途的一些困难（包括上面提到的功能强度问题）。
Matt Parsons 的Distributed Modal Logic提供了一个面向 Haskell 的直觉主义 S5 演示和对它的解释，最初由 Tom Murphy VII 在分布式计算方面：
B x作为x可以在网络上任何地方运行的生成计算，以及D x作为地址到x某处就可以了。时间逻辑可以通过 Curry-Howard 与函数式反应式编程 (FRP) 相关联。建议的起点包括de Paiva 和 Eades III，Constructive Temporal Logic，Categorically (2017)，以及Philip Schuster 的这篇博客文章以及这个有趣的 /r/haskell 主题。