Haskell 中遵循模态公理的有趣运算符答案

【问题标题】：Interesting operators in Haskell that obey modal axiomsHaskell 中遵循模态公理的有趣运算符
【发布时间】：2018-08-22 02:22:20
【问题描述】：

我只是在查看map :: (a -> b) -> [a] -> [b] 的类型，而这个函数的形状让我想知道我们是否可以将列表形成运算符 [ ] 视为遵循普通模态逻辑常见的各种公理（例如，T、S4、 S5, B)，因为我们似乎至少有正常模态逻辑的 K 公理，[(a -> b)] -> [a] -> [b]。

这引出了我的问题：Haskell 中是否有熟悉的、有趣的运算符或函子，它们具有某种模态运算符的语法，并且遵循普通模态逻辑的公理（即 K、T、S4、 S5 和 B)？

这个问题可以更尖锐，更具体。考虑一个运算符L 及其对偶M。现在问题变成了：Haskell 中是否有任何熟悉的、有趣的运算符具有以下一些属性：

(1)L(a -> b) -> La -> Lb

(2)La -> a

(3)Ma -> L(M a)

(4)La -> L(L a)

(5)a -> L(M a)

看到一些很好的例子会很有趣。

我想到了一个潜在的例子，但最好知道我是否正确：将L 作为not not 和M 作为not 的双重否定翻译。这种转换将每个公式a 转换为它的双重否定转换(a -> ⊥) -> ⊥，并且至关重要的是，验证了公理 (1)-(4)，但不验证公理 (5)。我在这里问了一个问题https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples，似乎双重否定翻译可以通过延续单子来模拟，endofunctor 将每个公式a 带到它的双重否定翻译(a -> ⊥) -> ⊥。 Derek Elkins 注意到存在一些双重否定翻译，通过 Curry-Howard 同构，对应于不同的连续传递风格变换，例如Kolmogorov 对应于按名称调用的 CPS 变换。

也许还有其他操作可以通过 Haskell 在 continuation monad 中完成，这些操作可以验证公理 (1)-(5)。

（只是为了消除一个例子：所谓的 Lax 逻辑 https://www.sciencedirect.com/science/article/pii/S0890540197926274 和 Haskell 中的 Monads 之间有明确的关系，返回操作遵循该逻辑的模态运算符（它是一个内函子）的规律。我对这些示例不太感兴趣，但对遵循经典正态模态逻辑中模态运算符的一些公理的 Haskell 运算符的示例感兴趣）

【问题讨论】：

我不知道你的问题是什么，但[a -> b] -> [a] -> [b] 是(<*>) 的类型，专门用于[] 的Applicative 实例。
我们有(<*>) :: [a -> b] -> [a] -> [b]，对于“功能模态”，我们有(<*>) :: (e -> (a -> b)) -> (e -> a) -> (e -> b)，这是众所周知的K组合子。不过，他们共享 K 名称可能只是巧合。 ;-)
关于“太宽泛”的近距离投票：FWIW，我觉得这个问题不应该被关闭。它是以一种相当投机的方式表达的（可能是由于 OP 不熟悉 Haskell，在问题的原始修订中提到了这一点）；然而，其核心是一个相当合理的问题，即函子类是否与模态运算符有关。
L 确实看起来像个共生体，但不确定对应的 M 会是什么。但是例如已知的comonads，例如a的非空列表，(w,a)的对将满足。
您绝对应该阅读Getting a Quick Fix on Comonads，它主张（限制使用）ComonadApply 用于某些模态逻辑。

标签： haskell modal-logic

【解决方案1】：

初步说明：我很抱歉在这个答案中花费了很大一部分谈论 Propositional Lax Logic，这是一个您是 very familiar with 的话题，并且就这个问题而言不太感兴趣。无论如何，我确实觉得这个主题值得更广泛地曝光——感谢您让我意识到这一点！

命题松散逻辑 (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 et. al., Categorical and Kripke Semantics for Constructive S4 Modal Logic (2001)。有趣的是，该论文证明 PLL 并不像最初看起来那么奇怪（参见Fairtlough and 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变体的特例。此外，它将 PLL 的D 定义为类似可能性的运算符。如果我们将 D 作为 Haskell Monads 的对应物，这在直觉上很有吸引力，后者通常确实有一种可能的味道（考虑Maybe Integer——“这里可能有一个Integer”——或IO Integer -- "程序执行时我会得到一个Integer")。

其他一些可能性：

乍一看，似乎使D 微不足道的对称举动使我们得到了非常类似于ComonadApply 的东西。我说“非常喜欢”主要是因为 Haskell Functors 的功能强大，如果您正在寻找传统的必要模式，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 的 intuitionistc S5 演示文稿及其最初由 Tom Murphy VII 在分布式计算方面的解释：B x 作为 x 生成计算可以在网络上的任何地方运行，并将D x 作为地址到x 某处。
时间逻辑可以通过 Curry-Howard 与函数响应式编程 (FRP) 相关联。建议的起点包括de Paiva and Eades III, Constructive Temporal Logic, Categorically (2017)，以及this blog post by Philip Schuster和this interesting /r/haskell thread about it。

【讨论】：