为什么 ArrowApply 是证明与 Monads 等效的唯一选择？

Question

在这个问题下，leftarounabout留下了一个非常清楚的解释，为什么我们实际上考虑ArrowApply和Monad等价。

这个想法是在往返期间不丢失任何信息：

arrAsFunction :: Arrow k => k x y -> (x -> k () y)
arrAsFunction ? x = ? <<< arr (const x)

retrieveArrowFromFunction :: ? k x y .
          ArrowApply k => (x -> k () y) -> k x y
retrieveArrowFromFunction f = arr f' >>> app
 where f' :: x -> (k () y, ())
       f' x = (f x, ())

我（可能）明白，为什么我们开始谈论(x -> k () y)- 一个包裹\ ~() -> ...并不能成为一个伟大的箭头，因此我们希望它取决于环境。

我的问题是：我们如何确定以下函数不存在：

retrieveArrowFromFunction :: ? k x y .
          Arrow k => (x -> k () y) -> k x y

我尝试想出一些箭头，这些箭头会弄乱该类型的 Curry-Howard 对应关系。这是正确的引导吗？可以更轻松地完成吗？

Answer 1

这是一个非常简单的箭头。您可能会将其视为Writer幺半群上的一个类似箭头Any。

newtype K a b = K Bool

instance Category K where
    id = K False
    K x . K y = K (x || y)

instance Arrow K where
    arr _ = K False
    K x *** K y = K (x || y)

如果您了解这些定义的后果，您会发现first并second更改箭头的类型而不更改包含的Bool. 这意味着我们无法创建合法ArrowApply实例。以下定律决定了我们必须选择app = K False：

first (arr (...)) >>> app = id

但是下面的定律，选择g = K True，决定了我们必须选择app = K True：

first (arr (...)) >>> app = second g >>> app

矛盾。

将此观察结果提升到您的直接问题，我们无法定义

retrieve :: (x -> K () y) -> K x y

以不丢失信息的方式。事实上，我们甚至无法定义更单态（因此更容易实现）的函数

retrieveMono :: (Bool -> K () ()) -> K Bool ()

以不丢失信息的方式：参数类型有 4 个居民，而返回类型只有 2 个。

附录

你可能想知道我是如何想出这个反例的。在我看来，所问问题的核心是是否有任何Arrow不是ArrowApply. 我记得第一篇关于箭头的论文之一，由约翰休斯 (John Hughes)撰写的将 Monads 概括为箭头，作为一个激励示例，一个不能成为 monad 的箭头（因此也不能成为一个ArrowApply实例）。我翻出了论文，回顾了解析箭头的定义，并将其归结为无法变成一个ArrowApply或 monad的本质：我扔掉了箭头的类似函数的部分，观察到其余的它充当了一个花哨的幺半群，并选择了我能想到的最简单的非平凡幺半群来代替论文中令人兴奋的幺半群。