为什么在证明与 Monad 等价时，ArrowApply 是唯一的选择？

Under 这个问题 https://stackoverflow.com/questions/59869399/why-does-mutual-yielding-make-arrowapply-and-monads-equivalent-unlike-arrow-and, 左转 https://stackoverflow.com/users/745903/leftaroundabout left 一个非常清楚的解释 https://stackoverflow.com/a/59897265/11143763 why we actually考虑ArrowApply and 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

我尝试想出一些箭头，这会弄乱该类型的库里-霍华德对应关系。这是正确的引导吗？可以更容易地完成吗？

这是一个非常简单的箭头。你可能会认为它是一个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 and 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 个居民。

Addendum

你可能想知道我是如何想出这个反例的。在我看来，问题的核心是是否存在Arrow这也不是一个ArrowApply。我记得第一篇关于箭头的论文，将单子推广到箭头 http://www.cse.chalmers.se/%7Erjmh/Papers/arrows.pdf约翰·休斯 (John Hughes) 提出了一个激励性的例子，一个箭头不能成为单子（因此也不能是单子）ArrowApply实例）。我翻出了这篇论文，回顾了解析箭头的定义，并将其归结为使它不可能变成一个ArrowApply或单子：我扔掉了箭头的类似函数的部分，观察到它的其余部分充当了一个奇特类型的幺半群，并选择了我能想到的最简单的非平凡幺半群来取代论文中令人兴奋的幺半群。