Live data from Hacker News

Programming with Categories

brendanfong.com

111–113 of 113 posts

Re: Programming with Categories

#111
post #39

Earlier quoted context omitted.

Which is kind of ironic, because students take classes exactly because they feel 'immature' with respect to that subject.. Honestly, most of my smoothest educational experiences with hard topics assumed some immaturity on my part, and that that was OK

People don’t generally take category theory because they don’t really understand how proofs work or how to read definitions. The maturity required is about being able to cope with proving things and following proofs based on definitions which will probably seem somewhat bizarre at first and unmotivated at first. The immaturity you seem to talk about is people taking category theory because they don’t know category th…

When I first went from CT as an implementation detail of typed FP to studying CT on its own, I was very aggravated by this point: "where is there a functor that isn’t an endofunctor?"

Over time it has fallen away in two directions.

In one direction is that though you are always stuck in a category with types as objects and functions as arrows, that doesn't stop you from subdividing. This became more intuitive to me as I encountered more and more categories that are basically just Set with extra structure (just as the one we program in is basically Set with bottom). If you start putting extra structure on your arrows (that is something that carries around a function along with some extra proof-relevant structures, like say a way to show that some zero element in the domain under the function equals the zero element in the codomain and that multiplication is preserved under the function, now you have monoid-homomorphisms) then you end up in the general case with something that looks a lot like a binatural transformation of profunctors, which pretty cleanly encodes "exo"-functors between different sub-categories of the category with all types as objects and functions as arrows.

In the other direction is realizing that even imprecisely, there's quantifiable value in observing functors to and from the category of types and functions, say one between whiteboard diagrams and code, or between a specific problem domain and code, etc etc. If you have some other space with composable relationships that you want to preserve when you write code to correspond to it, or you have some other representation you want to produce based off some given codebase while preserving the structure of the code taken as input, you can gain a ton of conceptual leverage out of identifying a functor.

Re: Programming with Categories

#112
post #107

If you're interested in how Category theory and Algebra can inform the design of software, have a look at ZIO Prelude. https://github.com/zio/zio-prelude It's a brand new library for Scala that contains reusable mathematical structures. Still based on algebra and category theory, but it expresses them more or less differently than how they've been expressed in Haskell (and similar languages). For example, unlike Hask…

Are there any useful types that have `flatten` but not `map` or `contraMap`?

If I understood John's motivation from the video, it's that this enables the Flatten structure to be inspectable, because the innards are not hidden behind an opaque closure (A => F[B]), as is the case in regular Monad.

Btw, this is a problem that the "Selective applicative functor" too aims to alleviate.

You can read more about the inspectability problem (and Selective) at http://eed3si9n.com/selective-functor-in-sbt

The context there is sbt, which is a build tool, but I'm sure the inspectability plays role in many other areas. Note, how he contrasts "Applicative composition" and "Monadic composition".

Re: Programming with Categories

#113
post #78

Earlier quoted context omitted.

People don’t generally take category theory because they don’t really understand how proofs work or how to read definitions. The maturity required is about being able to cope with proving things and following proofs based on definitions which will probably seem somewhat bizarre at first and unmotivated at first. The immaturity you seem to talk about is people taking category theory because they don’t know category th…

Isn’t an endofunctor a morphism from/to the same category? So a functor would be any morphine from/to different categories, and that wouldn’t be an endofunctor? Endofunctor: A -> A, for category A Functor: A -> B, for categories A and B

In the typical functional programmers view of category theory, there is only one category of interest so all functors are endofunctors. My main issue is that category theory the thing being studied is categories plural and so I feel like the language of category theory is being used to only ever talk about a single category.

It feels like doing “group theory” entirely with the symmetric group of the integers. While it’s true that the group is very general and has interesting properties, the focus of group theory isn’t single groups but rather the relationships between groups.

Compare this to something like algebraic topology or Galois theory where you have a Galois correspondence (a functor) between objects you’re interested in and groups.

Post reply on HN