当证明与Monad等效时，为什么ArrowApply是唯一的选择? [英] Why is ArrowApply an only option when proving equivalence with Monads?

问题描述

在这个问题， leftarounabout 左 a相当清楚的解释为什么我们实际上考虑 ArrowApply 和 Monad 等效.

Under this question, leftarounabout left a pretty clear explanation why we actually consider ArrowApply and Monad equivalent.

该想法是在往返期间不丢失任何信息:

The idea is in not losing any information during round trips:

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)-包装好的 \〜()->... 并不是很好的箭头，因此我们希望它取决于环境.

I (probably) understand, why we started speaking of (x -> k () y) - a wrapped \ ~() -> ... does not make a great arrow, therefore we would like it to depend on the environment.

我的问题是:我们如何确定以下功能不存在:

My question is: how can we be sure that the following function does not exist:

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

我尝试提出一些箭头，这些箭头会弄乱该类型的Curry-Howard对应关系.这是正确的线索吗?可以更容易做到吗?

I tried coming up with some arrows which would mess up the Curry-Howard correspondence for the type. Is this a proper lead? Could it be done more easily?

推荐答案

这是一个非常简单的箭头.您可能会认为它是类同的 Any 上类似于 Writer 的箭头.

Here is a very simple arrow. You might think of it as a Writer-like arrow on the monoid 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 :

If you work through the consequences of these definitions, you will find that first and second change the type of an arrow without changing the contained Bool. This means we cannot create a lawful ArrowApply instance. The following law determines that we must choose app = K False:

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

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

But the following law, choosing g = K True, determines that we must choose app = K True:

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

矛盾.

将此观察结果带入您的直接问题，我们无法定义

Lifting this observation to your direct question, we cannot define

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

不会丢失信息.确实，我们甚至不能定义更单态(因此更易于实现)的功能

in a way that does not lose information. Indeed, we cannot even define the more monomorphic (and therefore easier to implement) function

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

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

in a way that does not lose information: the argument type has 4 inhabitants, while the return type has only 2.

附录

您可能想知道我是如何提出这个反例的.我认为，要问的问题的核心是是否有任何 Arrow ，它也不是 ArrowApply .我记得关于箭头的第一批论文之一，将Monads概括为箭头举了一个激励人的例子，它不能做成单子箭头(因此也不能是 ArrowApply 实例).我挖了论文，回顾了解析箭头的定义，并将其归结为无法变成 ArrowApply 或monad的本质:我丢弃了箭头，观察到它的其余部分充当了花式类型的类人动物，并选择了我想到的最简单的非平凡的类人动物来代替本文中令人兴奋的类人动物.

You might wonder how I came up with this counterexample. In my opinion, the core of the question being asked is whether there is any Arrow which is not also an ArrowApply. I recalled that one of the first papers on arrows, Generalising Monads to Arrows, by John Hughes, had as a motivating example an arrow which could not be made a monad (and therefore must also not be an ArrowApply instance). I dug up the paper, reviewed the definition of the parsing arrow, and boiled it down to the essence of what made it impossible to turn into an ArrowApply or monad: I threw away the function-like part of the arrow, observed that the rest of it acted as a fancy-typed monoid, and picked the simplest non-trivial monoid I could think of to replace the exciting monoid in the paper.

这篇关于当证明与Monad等效时，为什么ArrowApply是唯一的选择?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！