Arrows to arrows, categories to queries (2025)(reasonablypolymorphic.com)
86 points by firstbase 4 days ago | 9 comments
[–] sleepyams 4 days ago
[–] psuedobrain 3 days ago
`CoChoice` is defined in the Haskell profunctors package. If I had to make an unsubstantiated guess, I would say that CoChoice corresponds to cofixpoints/corecursion and CoStrong/ArrowLoop (not shown here but has type `((a, d) ~> (b, d)) -> (a ~> b)`) corresponds to fixpoints/recursion. Like yccs27 was saying, this would mean that cochoice corresponds to apomorphims and costrong corresponds to paramorphisms, though I'm really not sure. `CoStrong` seems to require laziness so it seems like costrong and cochoice should be flipped.
[–] solomonb 2 days ago
I'm interested in what you are doing with Poly. Can you share more?
I'm pretty fascinated by Poly and have done some work a while back on a poly type theory (amongst other poly projects).
[–] yccs27 4 days ago
For me the `cochoice` function feels like a recursion scheme, possibly a hylomorphism of some functor?
[–] sleepyams 4 days ago
Yes, I think these are related-ish, also to traces on symmetric monoidal categories. If you have any algebraic/categorical formalization of wiring diagrams, this is essentially taking a block with inputs A and C and outputs B and C and connecting the C output to the C input with a self-loop.
[–] yccs27 4 days ago
How does the use of arrows instead of functions actually help here? If you have a terminal object aka unit type `()`, then arrows `() ~> a` are equivalent to elements of `a`.
[–] deterministic 2 days ago
What an excellent read! Love it.
[–] skavi 4 days ago
bold to lead with an example that makes no sense at all.
[–] whateveracct 4 days ago
to you..maybe you're not the target audience. you don't have the prerequisites hehe
It was cool to read about "co-choice", although I looked up that term and couldn't really find it used anywhere, do you have a source? (Also I think there is a typo in the type signature in the code block in this section. The codomain of `cochoiceHask` should be `b` right?) The idea of building a loop from a function `Either a c -> Either b c` is very interesting. It reminds me of some of the ideas in the book "Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory" by Joseph E. Stoy, which you should check out if you haven't.