I prefer http://web.jaguarpaw.co.uk/~tom/blog/posts/2012-09-02-what-i..., but that's probably because I wrote it.
I prefer http://web.jaguarpaw.co.uk/~tom/blog/posts/2012-09-02-what-i..., but that's probably because I wrote it.
I mean that quite literally: I can make neither heads nor tails of your write up. It looks like a bunch of text with funny characters to me. This write up, OTOH, is written in my language using idioms I understand and relates it to Haskell without involving too much of the machinery of the language.
I finally had to divorce the terms in my head, much like watching the film version of a book that I have read. They are..."related" but frustration will result from assuming they will be the same.
I'll say, here was one key to my understanding once I saw it. In a purely functional language you want everything to be referentially transparent. That is, an expression should be able to be substituted for its value at any given moment in time. At the very least, you'll want the ability to denote which parts of your program are referentially transparent and which aren't.
This can be expressed as utopian vision: in a purely functional language we'd like everything -- everything -- to be a value.
We now need some way of translating code with side effects into code that returns a value. The logical abstraction is to say that the "value" is not the work itself -- once the work is done it's out of the bag, after all -- but rather the "value" is the machine which can perform that work.
To a mathematician this screams "functor." If you want to move between the two spaces repeatedly this screams "adjoint functors." There's some work you want to do in Space A that's more easily expressed in Space B, so you take a thing in A, transform it to a thing in B, do the work in B, and then transform back to A.
Think in, e.g., Ruby:
sentence.split(' ').map(&:reverse).join(' ')
split(' ') and join(' ') aren't quite inverses of each other, but they are adjoint. These pairs take us from the land of space-separated strings to the land of arrays back to the land of space separated strings.You see that all the time in programming and mathematics. I sometimes call it the "Super Mario Brothers" maneuver when I'm trying to teach it to students. Mario wants to get to the end of the level, so he hits a block, goes up the vine to cloud land, runs through cloud land, and then comes back down.
split(' ') and join(' ') aren't quite inverses of each other, but they are adjoint.
Do you mean you think they are adjoint functors? How are they functors, between which categories?Anyhow, I was playing loose and I know it. If I were writing in a more serious context I'd cross all the t's and dot all the i's. To me the more important thing was this slow gnawing in my gut, seeing hints of natural transformations and adjoint functors here and there and thinking, "Oh come on, there has to be a way to connect these dots."
Non-functional languages like Ruby don't think in this way, so there are hole all over the language.
1. split(" ") is not a functor because (x+y).split(" ") is not equal to x.split(" ") + y.split(" "), for example:
"a BC".split(" ") == ["a", "BC"], but
"a B".split(" ") == ["a B"] and "C".split(" ") == ["C"].
(At least join(" ") is a functor, which here just means monoid homomorphism.) I guess this problem could be fixed by replacing String with StringsThatAreEitherEmptyOrEndInSpace (you need the empty string to be the identity for composition).2. They are not adjoint, even after fixing the monoids to make them homomorphisms! It's easy to easy that if f and g are adjoint monoid homomorphisms, with unit η and counit ε, then the functions m ⟼ ε f(m) and n ⟼ g(n) η are inverses of each other. This does not happen here since, for example, join(' ') is not injective.
Can you fix the example, maybe by regarding them as categories in some other way? My gut feeling is that this won't work, but I haven't thought about it very much.
If, as I suspect, this adjointness is wrong and not easily fixable, does it still have value as an explanation? I think that's a personality question, I find it more confusing than enlightening, but can imagine some people would find it helpful.
But yeah, it's not the greatest example. I don't mean to defend it as something rigorous.
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.Here's the original paper on monads, which I highly recommend: http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba...
So a matter of taste!
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.
(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.
I don't like your take because it refuses to take that deeper dive into the mathematical Monad, despite [alluding] to it. Knowing the relationship between `Monad` and `Category` the type classes is almost never useful in programming Haskell. Knowing the relationship between `Monad`, monads, and their categorical underpinning is a different matter.
I don't see how the general notion of category theoretical monad helps with this. In fact it's debatable whether the notion of monad is really the right treatment for universal algebra at all. Lawvere theories are much simpler and capture almost all of what you need. See: https://www.dpmms.cam.ac.uk/~martin/Research/Publications/20...
> Knowing the relationship between `Monad` and `Category` the type classes is almost never useful in programming Haskell.
I disagree. I use (<=<) all the time. It's basically (.) with the Kleisli wrapping and unwrapping done for you.
The category law account for the Monad laws is useful once you've already learned to think categorically, at which point a full definition is great and provides indications of the next places to examine. Defining that a "Monad is really a Category k with an identification between k a b and a -> k () b" seems most useful to people who could already write "Monads Made Difficult", but not those who are trying to struggle to see how all these connections play out.
Monads Made Difficult is difficult, but lays the groundwork for a lot of the categorical machinery that forms the environment where Monads were born. That's important.
Are you saying that "Monads Made Difficult", is useful to "those who are trying to struggle to see how all these connections play out"?
My position is that it's definitely not. I don't think it's even really useful to experts, because, wait for it ... Haskell Monads really have very little to do with category theoretical monads! If all you want to do is to know how Haskell Monads work than I think that level of generality is unhelpful. If, on the other hand, you want to learn category theory then this is a fine approach :)
(NB I'm not claiming my article is for beginners either)
I don't think either article is great place for a beginner, but instead am coming from a point of view toward learning "advanced" functional programming and getting a flavor for categorical/squiggol style thinking. To me, it was greatly helpful to just see the pure math approach and then realize Haskell Monads as a simple example and less useful to see categorical concepts played out in the simplified Haskell domain.
Categories just don't make nearly as much sense as objects when all you see them as is a convenient way to talk about composition rules. They're dramatically powerful when you connect them to preorders, databases, graphs, or homology. My biggest moment of categorical bliss came from seeing the Paths monad on graphs, even though that is far removed from the programming domain.
Mathematics is quite alluring, but the word most people would use there is 'alluding'.
'Alluding' means 'making oblique reference to', which seems to convey the intended meaning.
instance Category (->) where
id = Prelude.id
(.) = (Prelude..)Given that, I think it's great! :D
But the title of the article is "Monads made difficult", so I don't understand why you think this is a problem.