Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Personally, I found the Haskell in this article far harder than the math, which was more or less trivial to anyone who knows some category theory. For instance, the following

    newtype (FComp g f) x = FComp { unCompose :: g (f x) }

    instance (Functor b c f, Functor a b g) => Functor a c (FComp g f) where
      fmap f (FComp xs) = FComp $ fmap (fmap f) xs
just does not parse easily at all to my mind. In fact, I don't see how someone who doesn't know Haskell could possibly understand the above truly. unCompose isn't even ever used.



And for me, as someone experienced with programming languages but only casually poking at the math, it didn't take that long to learn Haskell's syntax, but syntax that gratuitously uses η and μ (which look vaguely like mirror images of each other) is confusing, and I expect I would have a hard time remembering which is which (of course, I would probably learn to read Greek letters instinctively after spending some time reading them). And after at least 10 minutes, I cannot figure out what "Tμ" in "μ∘Tμ" means, syntactically, while no matter how confusing the Haskell code, it can at least be parsed unambiguously.

So a matter of taste!


It's really not the syntax that's the issue. It's the fact that the author of the article is embedding the category-theoretic concepts into the language at the type level, so wrapper types like Id and FComp have to be introduced as "hacks" to represent functors.

My main takeaway from this article is that at the end of the day Haskell is a programming language and not the most natural setting for abstract mathematics, even if there are many connections between the two areas.


On the other hand, embedding mathematics in the types of a language has equivalence with writing theorems (writing the values in that language with proving them) so it's not such an unnatural setting in at least one way.


Funnily, η and μ are chosen precisely because they are mirror images of one another—their functionalities are in some sense mirror images of one another as well. η approaches a single-layer of T from the bottom and μ approaches it from the top!

(Edit: extra funnily, I actually flipped these two in my first writeup. This one is corrected, but I wanted to leave the note!)

The real trouble with parsing mathematics is that the syntax is overloaded at every opportunity. This is nice once you're in the same "mathematical mindset" as the author because it's a way for the author to focus your attention purely on the most important concepts being discussed (and everyone expects that there will be a laborious translation step once you start trying to prove things with more rigor). That said, until you are it's a bear and a half.

For instance, T is a functor which means it acts on both objects and maps in the source category. So if T : A -> B and x : Ob(A) then Tx is an object in Ob(B) and T was being used here as an object map. But, if y is also an object in Ob(A) (also written as y : Ob(A)) and there's an arrow in A called f : x -> y (which you might also write as f : A(x,y) --- serious TMTOWTDI) then Tf is an arrow in B like Tf : Tx -> Ty.

So to parse Tμ. If T is an endofunctor T : X -> X, then for any object A : Ob(X), "μ : TTA -> TA" is an arrow in X(A, TA), thus Tμ is an arrow in X(TTTA, TTA).

To parse μ.Tμ note that . is function composition, we just have Tμ as an arrow in X(TTTA, TTA). If we follow that with an application of μ then we have μ.Tμ as an arrow in X(TTTA, TA).

(Edit: also worth noting, for more feeling of parallelism between μ and η, if you, like I did, replace μ with η in the above you get Tη : X(TA, TTA) and η.Tη as (TA, TTTA).)

In more Haskelly notation, Tμ is (fmap join :: (Monad t, Functor t) => t (t (t a))) -> t (t a)) and μ.Tμ is (join . fmap join :: (Monad t, Functor t) => t (t (t a)) -> t a) where I specialized all the types to be operating on the same endofunctor/monad.


Yeah, some of the syntax was confusing for me, too, but I trusted that it was equivalent to the mathematical statements.

Here's the original paper on monads, which I highly recommend: http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba...




Consider applying for YC's Fall 2025 batch! Applications are open till Aug 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: