Re:Arrows to arrows, categories to queries (2025)
by yccs27 on Wednesday November 04, 2026 @08:01AM
(#50364967)
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`.
Re:Arrows to arrows, categories to queries (2025)
by sleepyams on Wednesday November 04, 2026 @08:18AM
(#50365146)
Nice, I've also been playing around with creating a programming language based on some concepts in category theory, but I've been focusing more on the concept of polynomial functors. I know there is somewhat of a stigma against category theory on Hacker News for some reason, but it's cool to see people inspired to create new languages inspired by category theoretic ideas.
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.
Re:Arrows to arrows, categories to queries (2025)
by sleepyams on Wednesday November 04, 2026 @09:25AM
(#50365954)
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.
Re:Arrows to arrows, categories to queries (2025)
by psuedobrain on Wednesday November 04, 2026 @03:31PM
(#50371098)
`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 (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.
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.
I'm pretty fascinated by Poly and have done some work a while back on a poly type theory (amongst other poly projects).