I’ve been thinking. Arrows are nicer than Monads for static analysis. The main issue with a Monad is that the bind expects a function that outputs the next effect. The reason why this is an issue is because we can’t really unpack the lambda / function to see what possible effects it can return.
The arr from the Arrow type class gives off a similar smell to me as it explicitly requires that an Arrow supports embedding of this opaque lambda that will resist any kind of static analysis.
Wouldn’t it make more sense to make arr lift a category into an arrow?
Although, now that I’m writing this out, I realize that Category is not an Arrow so I’m not sure my proposition of lifting a Category into an Arrow really makes sense, but still. It feels like e.g. arr :: (cat b c) -> a b c would be nicer in some way and allow for better static analysis of Arrow based programs.
A commonly held view, but for an alternative view consider how Opaleye can possibly rewrite monadic expressions to SQL, which of course requires static analysis.
Well, I’ve said that Arrows are nicer for static analysis, not that it’s not possible for Monads :P.
Depending on the context we choose we can simply “ignore” the function in this case, but it still feels unsatisfying.
I could choose that the cat should be an instance of my interface, and then I can switch the implementation from some data structure to a function depending on whether I want to run the program or analyze it.
You can do this with monads also. It’s a bit strange, isn’t it, given that you can embed arbitrary functions? That’s why I recommend looking at how Opaleye does it!
Well, it’s true that bind is implemented using arrow notation, but that’s detail, it’s not an essential part of the instance. It’s probably worth noting that any Arrow that can instantiate lateral is actually a Monad.
I’m not quite sure what you mean, but probably not. In Opaleye as it stands there isn’t really a “computation” option, just a data structure option (that’s not to say there couldn’t be the former).
I’ve just scanned it briefly, but if the monad is only used to produce a data structure, then that’s certainly very “statically analyzable”.
When looking at the arr implementation I’ve seen the arrow is applied to the input alongside the mempty for the data structure so I thought there’s something else going on.
I think the theoretically nicest answer to this question is going to be something along the lines of Conal Elliott’s “Compiling to Categories,” I think a reasonable intermediate step would be to focus on compiling arrow notation this way, not necessarily arbitrary Haskell code. In fact, this is what Overloaded.Categories does, although it doesn’t support Cartesian closed categories yet. I played around with multiple existing implementations of the CtC idea and always ran into limitations, but I do feel like it’s the future that we should want to be heading toward. What I’m suggesting is not very different from the much older Generalized Arrows work, either.
I remember how exciting it was when Conal Elliot announced CtC back in 2016. I thought that WAS the future about to happen. A breakthrough in software architecture powered by introspection into code using categories and type classes. A renaissance of eDSLs. The mother of syntax sugars that would even dwarf the do notation, Haskell leapfrogging other languages by lightyears…
I’m unsure if anyone’s still interested in this topic, but perhaps symmetric monoidal categories may be the right abstraction. They’re discussed in Arnaud Spiwack and Jean-Philippe Bernardy’s paper, “Evaluating Linear Functions to Symmetric Monoidal Categories”. The associated haskell library linear-smc isn’t well-documented, but I found reading the paper to be fairly useful for understanding the basics.
I’ve just skimmed it, but I don’t think this addresses my initial issue about being able to embed pure functions. It kind of seems like this paper just lifts the usual monad vs arrow static analysis argument into the freer world.
