我只是在看类型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 as not not and M as not。这个翻译采用了每个公式a其双重否定翻译(a -> ⊥) -> ⊥并且最重要的是，它验证了公理 (1)-(4)，但不验证公理 (5)。我在这里问了一个问题https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples似乎双重否定翻译可以通过延续单子来模拟，endofunctor 采用每个公式a其双重否定翻译(a -> ⊥) -> ⊥。德里克·埃尔金斯 (Derek Elkins) 指出，存在两个双重否定翻译，通过 Curry-Howard 同构，对应于不同的连续传递风格变换，例如柯尔莫哥洛夫变换对应于按名称调用 CPS 变换。
也许可以通过 Haskell 在延续 monad 中完成其他操作，从而验证公理 (1)-(5)。
（只是为了消除一个例子：所谓的宽松逻辑之间存在明显的关系https://www.sciencedirect.com/science/article/pii/S0890540197926274 https://www.sciencedirect.com/science/article/pii/S0890540197926274和 Haskell 中的 Monad，返回操作遵循该逻辑的模态运算符（这是一个 endofunctor）的定律。我对这些例子不太感兴趣，但对 Haskell 运算符的例子不太感兴趣，它们遵守经典正态模态逻辑中模态运算符的一些公理）
初步说明：我很抱歉在这个答案中花了很大一部分时间谈论命题松散逻辑，这是您所关注的主题非常熟悉 https://mathoverflow.net/q/296211/123749就这个问题而言不太感兴趣。无论如何，我确实觉得这个主题值得更广泛的接触——感谢你让我意识到这一点！
命题松弛逻辑 (PLL) 中的模态运算符是 Curry-Howard 的对应项Monad类型构造函数。注意它的公理之间的对应关系......
DT: x -> D x
D4: D (D x) -> D x
DF: (x -> y) -> D x -> D y
...以及类型return, join and fmap， 分别。
Valeria de Paiva 有许多论文讨论了直觉模态逻辑，特别是 PLL。这里关于PLL的言论很大程度上是基于阿莱奇纳et. al., 构造性 S4 模态逻辑的分类语义和 Kripke 语义 (2001) https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf。有趣的是，该论文论证了 PLL 并不像乍看起来那么奇怪（参见 2017 年）。费尔特洛和门德勒，命题逻辑不严 (1997) https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf：“作为模态逻辑，它很特别，因为它具有单个模态运算符 [...]，既有可能性又有必然性”）。从 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变得微不足道（或者，用哈斯克尔的说法，Identity），将逻辑简化为 PLL。既然如此，PLL 可以被视为直觉 S4 变体的一个特例。此外，它还构建了 PLLD作为类似可能性的运算符。如果我们采用D作为 Haskell 的对应物Monads，通常确实有可能的味道（考虑Maybe Integer——“可能有一个Integer在这里”——或者IO Integer--“我会得到一个Integer当程序执行时”）。
其他一些可能性：
乍一看，这似乎是对称的动作D微不足道的事情让我们得到了非常类似的东西ComonadApply。我说“非常喜欢”主要是因为 Haskell 的函数强度Functor是，问题是x /\ B y -> B (x /\ y)如果您正在寻找传统的必需品模式，那么这是一件尴尬的事情。
肯尼思·福纳的Function Pearl：快速修复 Comonad https://github.com/kwf/GQFC（感谢 dfeuer 的参考）致力于在 Haskell 中表达直观的 K4，涵盖了沿途的一些困难（包括上面提到的函数强度问题）。
马特·帕森斯分布式模态逻辑 https://github.com/parsonsmatt/modalities提供了 intuitionistc S5 的面向 Haskell 的演示以及对它的解释，最初由 Tom Murphy VII 在分布式计算方面进行：B x as a x-生成可以在网络上任何地方运行的计算，以及D x作为地址x在它的某个地方。
时序逻辑可以通过 Curry-Howard 与函数反应式编程 (FRP) 联系起来。出发点的建议包括德派瓦和伊德斯三世，构造性时态逻辑，绝对 (2017) https://vcvpaiva.github.io/includes/pubs/2017-grisha.pdf， 也菲利普·舒斯特 (Philip Schuster) 的这篇博文 http://haskellexists.blogspot.com/2016/01/frp-for-free.html旁边这个有趣的 /r/haskell 线程关于它 https://www.reddit.com/r/haskell/comments/40x4wf/frp_for_free/.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
