tomjaguarpaw / Arrows2

Ideas for the next generation of Haskell's Arrow notation
12 stars 0 forks source link

Convincingly demonstrate the Monads are actually needed #3

Open tomjaguarpaw opened 4 years ago

tomjaguarpaw commented 4 years ago

What do we really want Monad for that we can't do with ArrowChoice?

lexi-lambda commented 4 years ago

ArrowChoice is actually very restrictive: it allows the computation graph to have conditional branches, but the graph itself still has to be completely statically known. This means, for example, it is impossible to do something as simple as traverse_ in an arrow, since that requires dynamically spawning a new branch in the graph for each element of the data structure.

Theoretically, I think you can get that power back with ArrowLoop, since you can use that to implement iteration. However, few arrows actually support an ArrowLoop instance that satisfies all the laws, anyway. A more useful operation is something like

class ArrowChoice arr => ArrowAlign arr where
  aligned :: (Traversable t, Align t) => arr (e, a) b -> arr (e, t a) (t b)

which is closely related to my keyed operation from https://github.com/ghc-proposals/ghc-proposals/pull/303. A generalization of keyed itself can be expressed as

class ArrowChoice arr => ArrowKeyed arr where
  keyed :: (TraversableWithIndex k t, AlignWithIndex k t) => arr (e, k, a) b -> arr (e, t a) (t b)

which allows a limited form of dynamic dependencies in which it is possible to compare consecutive executions of the same dependency graph. This is very useful for my use case—build caching—but it isn’t clear if it’s useful more generally.

tomjaguarpaw commented 4 years ago

it is impossible to do something as simple as traverse_ in an arrow

I don't understand what you mean. traverse and traverse_ only require an Applicative which an Arrow certainly is. Could you give an example of something to do with traverse_ that fails in ArrowChoice?

lexi-lambda commented 4 years ago

Sorry, you’re technically right, but there’s a distinction I’m making I wasn’t clear about. The type of traverse in some arrow arr is this:

traverse :: Traversable t => (b -> arr a c) -> t b -> arr a (t c)

That seems like it might be useful, but it isn’t actually nearly as useful as it seems. What you really want is an operation of this type:

traverseA :: Traversable t => arr a b -> arr (t a) (t b)

The trouble is, with ordinary traverse, the t b argument isn’t an input to the arrow, it’s an input to the arrow constructor function. That means the t b argument can’t actually come from the output of a previous arrow at all—it has to be a statically known value. That kind of defeats the purpose of traverse entirely.

tomjaguarpaw commented 4 years ago

Ha, yes, I see!

lexi-lambda commented 4 years ago

I take it all back: you can get traverseA from ArrowChoice alone. All it takes is the right choice of applicative functor:

data Traversal a r b
  = Done b
  | Yield a !(r -> Traversal a r b)

instance Functor (Traversal a r) where
  fmap f = \case
    Done x -> Done (f x)
    Yield v k -> Yield v (fmap f . k)

instance Applicative (Traversal a r) where
  pure = Done
  tf <*> tx = case tf of
    Done f -> fmap f tx
    Yield v k -> Yield v ((<*> tx) . k)

traversal :: Traversable t => t a -> Traversal a b (t b)
traversal = traverse (flip Yield Done)

traverseA :: (ArrowChoice arr, Traversable t) => arr (e, a) b -> arr (e, t a) (t b)
traverseA f = second (arr traversal) >>> go where
  go = proc (e, as) -> case as of
    Done bs -> returnA -< bs
    Yield a k -> do
      b <- f -< (e, a)
      go -< (e, k b)

I have not been able to find this in any existing literature, but it might be well-known, and I just wasn’t looking in the right places.

tomjaguarpaw commented 4 years ago

Once upon a time, Edward Kmett told me how to apply a lens to an arrow. The idea is that you can use Context to convert

Functor f => (a -> f b) -> c -> f d

into

Arrow p => LensLike (Context a b) s t a b -> p a b -> p s t

(using only the Strong and Profunctor properties of Arrow). Context is Context (b -> t) a. Your Traversal is a version of this for multiple items instead of one. Presumably Edward's idea presumably extends to converting

Applicative f => (a -> f b) -> c -> f d

into

Arrow p => LensLike (Traversal a b) s t a b -> p a b -> p s t

using only the Strong, Profunctor and Applicative properties of Arrow. This is missing the e argument, but adding that argument doesn't change that the structure is Strong, Profunctor and Applicative, so the same construction will go through.

tomjaguarpaw commented 4 years ago

Ah, https://pursuit.purescript.org/packages/purescript-profunctor-lenses/5.0.0/docs/Data.Lens.Types#t:Traversal and https://pursuit.purescript.org/packages/purescript-profunctor-lenses/5.0.0/docs/Data.Lens.Internal.Wander#t:Wander suggest that it's Stong and Choice that are needed, which is consistent with your ArrowChoice constraint.

tomjaguarpaw commented 4 years ago

Anyway, the executive summary is that this is an application of a profunctor-style traversal.

Ericson2314 commented 4 years ago

I think "Selective Applicative Functors" are very close to ArrowChoice.

it allows the computation graph to have conditional branches, but the graph itself still has to be completely statically known.

I think the basic idea is graphs created dynamically that really only make finite choices can be squashed into one giant static graph that includes the decision tree on the previously-dynamic decisions.

tomjaguarpaw commented 4 years ago

I believe that the following is the same construction as Alexis's (though I haven't actually carried out the analysis to verify that!)

https://github.com/ekmett/profunctors/pull/40/files

Ericson2314 commented 4 years ago

Yeah that looks like the same construction. I would do it different with https://hackage.haskell.org/package/categories-style classes, but that is a fine way to do it with Arrow as it exists today.


To get back to your original question while Monad i more powerful, I think it's wildly overused, and we shouldn't feel dangerously heretical coming to conclusion that other weaker classes will almost always do.

tomjaguarpaw commented 4 years ago

So that is minor evidence against our hypothesis that Monads are actually needed.