Computability? - Category theory

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Sandy Maguire

I'm working my way through Bartosz right now, and I'm struck by how little of this category stuff feels computable. e.g. if the product in Set is defined through the universal mapping or through a limit, it still feels like you need to do infinite amounts of work to actually distinguish the product object? Am I missing something here?

Sandy Maguire

I guess more generally I'm concerned about what feels like handwaving --- and I'm not sure if it's my understanding that's doing the handwaving or if it's the material itself

Kit Langton

I feel like there could stand to be a Category Theory for Programmers that skews significantly closer to the Programmers side of things. I'm afraid Bartosz is too incurably cursed by the curse of knowledge to be able to dumb himself down the necessary amount (for me at least—though I'm always willing to give his book another try as I love his talks and personality).

Apologies if that's not what you meant by computability :) I'm out of my depth here

Sandy Maguire

i feel the same way --- though coming at this as a programmer :)

Sandy Maguire

computability meaning, eg: the product diagrams give me a way to verify that something is a product. but there doesn't seem to be any machinery that will locate a product in a category

Sandy Maguire

nobody has shown me an algorithm i can throw at a category and eventually get the product type out

Sandy Maguire

short of pick every X, A, B, Z, then pick every f:X->A, g:X->B, etc, and see if the product diagram holds

Sandy Maguire

for infinite sized things, determining the answer here is equivalent to solving the halting problem

Kit Langton

Not to give you any more book ideas :P But I'd love a version of a Category Theory book that explores as many possible concepts via programmatic "witnesses" (like this bit from Thinking With Types for example). This leverages my extant programming experience to catapult an intuitive understanding of isomorphisms up and over my brain walls. It decidedly does not stultify me with eldritch math symbols or lingo.

Maybe a has a canonical sum-of-products form as Either () a. This can be proven via an isomorphism:

toCanonical :: Maybe a -> Either () a
toCanonical Nothing = Left ()
toCanonical (Just a) = Right a

fromCanonical :: Either () a -> Maybe a
fromCanonical (Left ()) = Nothing
fromCanonical (Right a) = Just a
toCanonical and fromCanonical convert between Maybe a and Either () a without losing any information. This witnesses an isomorphism between the two types.

I was expecting similar examples in Bartosz's book, but alas, there weren't nearly as many as I'd hoped for. The cute little explosives-wielding piggies could only help so much.

Sandy Maguire

i'd pay money for that. Maybe @tel could write one

Sandy Maguire

but alas he is not here

Leonardo Taglialegne

Explosive wielding piggies are really cute tho

Ohad Kammar

@Sandy Maguire

computability meaning, eg: the product diagrams give me a way to verify that something is a product. but there doesn't seem to be any machinery that will locate a product in a category

For me that's a feature, allowing very different implementations/instances of the concept of, say, a product. Having a uniform interface for a collection of important concept that you won't be able to recognize mechanically can be /really/ useful. It's useful
especially when you apply it in the negative: showing that a certain category doesn't have products means that, no matter how much you look for it, you won't find it.

Sandy Maguire

that's a really interesting perspective