Haskell中有趣的操作符遵守模态公理

Question

我只是看着map :: (a -> b) -> [a] -> [b]这个函数的类型和形状让我想知道我们是否能够看到列表形成operator []遵循正常模态逻辑(例如,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)

看到一些很好的例子会非常有趣.

我已经想到了一个潜在的例子,但是知道我是否正确是很好的:带有Las not not和Mas 的双重否定翻译not.这种翻译将每个公式都a用于其双重否定翻译,(a -> ?) -> ?并且至关重要的是,验证公理(1) - (4),但不是公理(5).我在这里问了一个问题https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples 似乎可以通过continuation monad模拟双重否定翻译,endofunctor将每个公式都a带到它的双重否定翻译(a -> ?) -> ?.德里克·埃尔金斯注意到存在一些双重否定翻译,通过库里 - 霍华德同构,对应于不同的连续传递风格变换,例如,Kolmogorov对应于逐个呼叫的CPS变换.

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

---

(并且只是为了消除一个例子:所谓的Lax逻辑https://www.sciencedirect.com/science/article/pii/S0890540197926274 与Haskell中的Monads 之间存在明确的关系,返回操作遵循模态的规律这个逻辑的运算符(它是一个endofunctor).我对这些例子并不感兴趣,但是在Haskell运算符的例子中,这些运算符遵循经典正态模态逻辑中的模态运算符的一些公理)

Answer 1

初步说明：我很抱歉在答案中花了很多钱来谈论命题松弛逻辑，这是一个您非常熟悉但对这个问题不太感兴趣的话题。无论如何，我确实认为这个主题值得更广泛地曝光-感谢您让我意识到这一点！

命题松弛逻辑（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变体的特殊情况。此外，它把PLL构造D成类似可能性的运算符。如果我们采用DHaskell Monad的对应物，这在直觉上很吸引人，而Haskell 的确具有某种可能性（考虑Maybe Integer-“这里可能有一个Integer”或IO Integer-“ Integer程序执行时我会得到一个”）。

其他一些可能性：

• 乍一看，似乎D琐碎的对称举动使我们得出了非常类似的结论ComonadApply。我之所以说“非常喜欢”，很大程度上是因为Haskell Functor的功能强大，x /\ B y -> B (x /\ y)如果您正在寻找传统的必需方式，那将是一件尴尬的事情。

• 肯尼斯·弗纳（Kenneth Foner）的《功能性明珠：快速了解Comonads》（感谢dfeuer供参考）致力于在Haskell中表达直觉K4，涵盖了开发过程中的一些困难（包括上述功能强度问题）。

• 马特·帕森斯的分布式模态逻辑提供的intuitionistc S5一个Haskell，面向表示和它的一个解释，最初是由汤姆·墨菲七，在以下方面分布式计算：B x作为x制造用的计算，可以随时随地在网络上运行，并D x作为地址到x某个地方。

• 时态逻辑可通过Curry-Howard与功能反应式编程（FRP）相关联。关于起跑点的建议包括de Paiva和Eades III，《建设性时态逻辑》（Cativegorically）（2017年），以及Philip Schuster的博客，以及关于此的有趣的/ r / haskell主题。