Hacker News new | ask | show | jobs
by empath75 3358 days ago
Monads.
1 comments

Not to be pedantic, but if someone understands monoids well from abstract algebra and someone else says:

"By the way, in addition to all the existing monoids you know (Ints under '+', strings, lists...), functions under function composition also form a monoid. Here's an example."

Isn't that pretty much getting them to the same place? Do they really need a study of category theory?

Function composition is a monoid, but it is not a monad, even though the words sound similar. So it's not really getting them to the same place, but I'm not going to offer any opinion on whether someone needs to study category theory.

Not quite function composition, but given a type a, (a ->) is a monad (the so called "reader monad"). We have

   return :: x -> (a -> x)
   return x = \a -> x
   
   (>>=) :: (a -> x) -> (x -> (a -> y)) -> (a -> y)
   m >>= f  = \a -> f (m a) a
(Incidentally, these are two of the Łukasiewicz axioms for propositional calculus.)

It is a functor with

   fmap :: (x -> y) -> (a -> x) -> (a -> y)
   fmap f m = \a -> f (m a)
In the case x=y, then fmap takes the monoid of functions on x to the monoid of functions on (a -> x).

Venturing into more abstract territory, "a monad is a monoid in the category of endofunctors of a category C." (This has never helped me with understanding how to use monads in Haskell.) Basically, the choice of endofunctor is the type constructor for the monad, the unit map is `return` and the composition map is `join`.

> return :: x -> (a -> x)

> return x = \a -> x

>

> (>>=) :: (a -> x) -> (x -> (a -> y)) -> (a -> y)

> m >>= f = \a -> f (m a) a

>(Incidentally, these are two of the Łukasiewicz axioms for propositional calculus.)

Also the K and S in SKI combinator calculus https://en.wikipedia.org/wiki/SKI_combinator_calculus

The Wikipedia article mentions "The combinators K and S correspond to two well-known axioms". I wonder whether Schönfinkel and Curry had Łukasiewicz's axioms in mind when creating it? I'm finding it difficult to find the history of either the combinators or the axioms.
Isn't the identity monad isomorphic to normal functions? In that sense normal functions are a monad.
I checked that while I was writing my comment, and I don't believe there is such an isomorphism. For the identity monad, we have the following functions:

   return :: a -> a
   return = id

   join :: a -> a
   join = id
If this were isomorphic to the function composition monoid, there would be some way to interpret join as function composition, but I don't see it. Please show me if you know the isomorphism! (My thinking is a bit fuzzy on this, but it appears to me that the identity monad is actually isomorphic to a trivial monoid --- if you want, you can model the trivial monoid as the one-element set {0} under addition.)

Bind is

   (>>=) :: a -> (a -> b) -> b
   (>>=) = flip id
that is, function application. Still no function composer in sight, though.
At this point I admit I'm way beyond my depth.

This article seems to imply a correlation between the fish operator (<=<) and composition. Specifically his section on Kleisli monad.

http://www.haskellforall.com/2012/08/the-category-design-pat...

But I don't know the space well enough to know if that's answering your question.

It's true that the Kleisli category gives a composition law from a monad, but let's not lose sight: the point isn't whether there is a conceivable way to compose things, but whether a monad is just a monoid of functions under composition.

Monads are like a monoid at the type level plus a bunch of coherence rules. For every type a, there is a "composition" m (m a) -> m a and a "unit" a -> m a. (Compare with a monoid, where there is a composition m x m -> m and a unit {1} -> m.) Also, the composition must be natural in the sense that whenever there is a map f :: a -> b then you have a bunch of "commuting squares": the composition m (m a) -> m (m b) -> m b must equal m (m a) -> m a -> m b and the composition a -> m a -> m b must equal a -> b -> m b. (Some of these maps are fmap f or fmap (fmap f).)

The naturality thing is important and shows up quite a lot, and category theory was invented to understand naturality. It's sort of a higher higher order functional programming.

Functions of type A -> A for some A form a monoid under composition, but functions of arbitrary type don't. The nifty phrase "a monad is just a monoid in the category of endofunctors" doesn't refer to the function composition monoid, but something much stranger, where the "composition" operation has type m (m a) -> m a, and the "identity" operation has type a -> m a. To understand how that can be seen as a monoid, note that the composition operation composes two effects on the same computation, and the identity operation adds an empty effect.
> note that the composition operation composes two effects on the same computation, and the identity operation adds an empty effect.

Thanks - While I did have this vague idea, and it says it from the types, seeing it written out in this way was clarifying.