3

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?

Zhiltsoff Igor
  • 1,812
  • 8
  • 24
  • The theoretical explanation is that `Monad` & `ArrowApply` denote the same structure: a strong monad in a Cartesian closed category (CCC). `ArrowApply` needs a CCC because it has a notion of “exponentials” (function types), allowing you to write `apply :: a (a x y, x) y`, `curry :: a (x, y) z -> a x (a y z)`, and `uncurry :: a x (a y z) -> a (x, y) z`, which 1. are exactly the operations added by a CCC on top of a Cartesian category (denoted by `Arrow`) and 2. enable you to [write `join` functions for Arrows](https://stackoverflow.com/a/62547612/246886) like `joinA :: a x (a x y) -> a x y`. – Jon Purdy Jul 09 '20 at 17:59

1 Answers1

5

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.

Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
  • Thank you for your answer! The paper you are speaking of - is it the "Generalising Monads to Arrows" by John Hughes? Besides, your counterexample is really nice, yet it clearly requires a good background. How productive is Curry-Howard correspondence for such problems in your experience? – Zhiltsoff Igor Jul 08 '20 at 16:41
  • 1
    @ZhiltsoffIgor Yes, that's the paper. It's not clear to me that C-H is particularly useful here. As an isomorphism, it has almost no computational content, so it's not clear that any question should be significantly easier to answer on one side or the other of the isomorphism. It is helpful in essentially only one sense: there is a big body of work on the "mathematical propositions" side of the isomorphism, so if the answer is *already well-known* there then it helps some. – Daniel Wagner Jul 08 '20 at 16:45
  • Is it possible to show that we have no other class which would allow more instances that will fit into the context of `retrieve`? I know it might be over-formalism, I am just interested how such proofs could be carried out. – Zhiltsoff Igor Jul 24 '20 at 10:31