Haskell Style Arrows

Stream: batteries

[Shreyas Srinivas]

Does lean have Haskell style Arrows? I am aware that Mathlib has the mathematical version of Arrows, but I wonder if that is the right thing to use for computational purposes, because I don't understand the underlying comma categories very well.

[Shreyas Srinivas]

I am aware that with Monads, there is a LawfulMonad and a Monad, and the latter is used for programming stuff.

[Eric Meinhardt]

I'll let others speak to what's currently in batteries/what might be soon, but in the meantime — what are you looking for and what do you want to accomplish when you say "Haskell Style Arrows"? (It's also perfectly OK to only have a partial answer or to not know! I started really learning about Arrows by trying (failing) to port them into Lean 4 :sweat_smile:)

There are lots of things in more or less vaguely categorical Haskell that supervene on the same construction (e.g. Applicative vs. the typeclass sometimes called Monoidal — see the end of McBride & Paterson's article introducing Applicative), plus there are simplifications made by feature/library authors for a mix of reasons ranging from "doing something more general than this would incur more friction for all the other use cases that we the feature authors currently are guessing people would plausibly use this for" to "expressing something at a certain level of generality is not possible [in Haskell]". In the case of Arrow specifically, while I'm not privy to the exact thought process that went into John Hughes making the Arrow typeclass as he did, a present or future Lean programmer has the benefit of 2+ decades of hindsight (downstream of Arrow, among other things) and the ambient setting of a much more expressive programming language.

1. Do you just want "closed Cartesian category" combinators (dup, swap, ***, &&&, |||, +++, first, second, fst, snd, curry, uncurry...) you can use with garden-variety functions for point-free style?

2. Do you want machinery to express categorical EDSLs? If so, you probably don't want a direct port of Arrow per se, chiefly because of the arr method. Either way, if you're after categorical EDSLs, how fine-grained of a typeclass hierarchy do you want? Do you want the "substructural" typeclasses that might let you write e.g. an elegant logic programming or probabilistic programming library interface? Is the way that Control.Arrow carves things up really what you're after?

3. Overlapping with other questions: are there particular (categorical ± ergonomic) properties you have in mind that you want an Arrow-like abstraction to capture?

4. Are you sure you don't want a library that takes profunctors (and, again, does that mean more like the Haskell profunctors library simplification, or something more expansive?) as primitive and categories (and hence Hughes's Arrow typeclass) as derived?

[Shreyas Srinivas]

So the correct answer is "I am exploring". The original Hughes paper had a parser example. But Ross Patterson's chapter in the fun of programming book gave some nice examples. One problem I am trying to solve in more than one way is composing multi input and multi output functions into pipelines. Ofc there are some simpler ways to accomplish the task. Arrow-like structures were used in certain hardware papers dealing with synchronous circuits, but these aren't enough for asynchronous circuits with combinatorial delays. What I am really looking for in the end are arrows with some state. I already have a case study on verifying these circuits that is to be ready for submission soon.

[Shreyas Srinivas]

Profunctors don't have a straightforward way to loop anything.

[Shreyas Srinivas]

My interest in categorical anything is limited to pragmatism.