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, ())
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
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?
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)
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
But the following law, choosing g = K True, determines that we must choose app = K True:
first (arr (...)) >>> app = second g >>> app
Contradiction.
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 ()
in a way that does not lose information: the argument type has 4 inhabitants, while the return type has only 2.
Addendum
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.