Haskell is not category theory • Hacker News Board

Re: Haskell is not category theory

#51

Post by BoiledCabbage » Sat, Feb 04, 2023, 11:37 PM UTC

epgui wrote: post #22

BoiledCabbage wrote: post #19

Earlier quoted context omitted.

> A lot of category theory is fun to learn and knowing it will help you in many ways I agree with your statement except that part. W.r.t coding, learning functional programing will help you in many ways. Learning category theory will just allow you to say "ah I've seen that concept before" - but it won't really help much.

The number of times I’ve heard someone say that some academic topic was not helpful and they were right is close to zero. It’s a pretty good heuristic to not adopt that attitude.

While that is a great general rule, everyday life isn't generalities, it's specific cases.

Outside of game programming, topology isn't useful knowledge for software engineering. A clear exception to your rule above.

Being an strict adherent to a heuristic and not examining the specifics of a situation is in my opinion a poor habit. Superficially pattern matching will lead people down the wrong path more often.

Re: Haskell is not category theory

#52

Post by hackandthink » Sun, Feb 05, 2023, 2:30 PM UTC

contravariant wrote: post #34

Y_Y wrote: post #12

Earlier quoted context omitted.

Haskell isn't the functor police! It's on you to define good functors, proving them so would be a totally different endeavour and far more difficult. I would like to understand better the issue with product types though. What do you want to do that you can't currently. By the way, most of my knowledge about the connection between Haskell and Category Theory comes from here: https://bartoszmilewski.com/2014/10/28/cate…

Hmm, well calling it a problem might be a bit much, but it means that functions with more than argument require some additional care, and technically a stronger notion of functor. Say you have a multivariate function a: X x Y -> Z, and a functor F. This would give you a function F(a): F(X x Y) -> F(Z). Now this is not really multivariate any more as F(X x Y) is not a product, but products behave quite well in categor…

"you don't have a function a: X x Y -> Z, you've got a function a: X -> (Y => Z)"

Haskell has products. What's the problem with f':

ghci> f x y = x + y

ghci> f' (x,y) = x + y

ghci> f 1 2

3

ghci> f' (1,2)

3

ghci> :t f'

f' :: Num a => (a, a) -> a

ghci> :t f

f :: Num a => a -> a -> a

Re: Haskell is not category theory

#53

Post by Iceland_jack » Sun, Feb 05, 2023, 5:22 PM UTC

gowld wrote: post #18

Y_Y wrote: post #12

Earlier quoted context omitted.

Haskell isn't the functor police! It's on you to define good functors, proving them so would be a totally different endeavour and far more difficult. I would like to understand better the issue with product types though. What do you want to do that you can't currently. By the way, most of my knowledge about the connection between Haskell and Category Theory comes from here: https://bartoszmilewski.com/2014/10/28/cate…

What is an example of category-theory functor in Haskell, that isn't just an endofunctor? A functor F from C to D is a mapping that associates each object X in C to an object F(X) in D. In Haskell, C and D are both the same (Hask types), hence endofunctor (functor into self). In general a functor could be something like `prime_factorizaton:: Int -> [(Prime Int, Mulitplicity Int)]`, with morphisms being things like th…

  Either a :: Type -> Type

is a Haskell Functor (endofunctor), mapping (->) to (->).

  Either :: Type -> (Type -> Type)

is not an endofunctor, it maps a type to a type constructor and thus maps (->) to (~>) (natural transformations).

If you uncurried Either, you would also get a non-endofunctor which maps from (-×>) (product category) to (->).

  Either' :: (Type, Type) -> Type

Every function is a functor between equality, since equality satisfies congruence:

  isPrime :: Integer -> Bool

is a functor between (:~:) @Integer an (:~:) @Bool. Boolean negation is a function between "less than or equal" to "greater than or equal" categories; mapping (=):

  not :: Bool -> Bool

Re: Haskell is not category theory

#54

Post by dwohnitmok » Mon, Feb 06, 2023, 7:50 PM UTC

runevault wrote: post #17

dwohnitmok wrote: post #11

Earlier quoted context omitted.

I believe the heart of what you're asking is "why do we distinguish between codomain and range?" and relatedly why do we even need the concept of "surjectivity?" For example, the function f(x) = x + x could be thought of a non-surjective "endo-"function (endomorphism) `N -> N` (where N is the natural numbers) or it could be thought of as a surjective function from `N -> E` (where E is the even natural numbers). Why d…

Thank you for the incredibly thorough writeup. I've read it once but I can tell I'm going to need a few more passes at least before I fully grasp everything because there is a TON of nuance (which does not surprise me I know just enough to realize Category theory by nature is full of nuance). A question for you, do you think there would be any value in a programming language that DID include the need to concern itsel…

> A question for you, do you think there would be any value in a programming language that DID include the need to concern itself with the structural differences between two categories or are we getting into issues like too much boilerplate to encode anything useful territory and similar?

Maybe but I'm skeptical. There's something nice about bringing some notions of mathematical rigor to code, but I'd be cautious.

Most day-to-day engineering consists of broad, but shallow insights. Only a few parts of an application really require the deep insights that abstract mathematics would provide.

I think developers as a whole would benefit from a stronger theoretical math background because there are indeed a few crucial spots in an application where it's extremely helpful, but I'm not bullish around building a programming language explicitly atop say category theory, precisely because the majority of the work would probably only be made more brittle to future modifications with overly insightful code (in the sense of this article: https://www.hillelwayne.com/post/cleverness/)