monads
Joined 12 years ago
Joined 12 years ago
I actually criticise the illusion (that the book and the series bring) that the category theory is "the ultimate source" of motivation in FP languages.
On one hand, it's direct (and very natural) to reproduce some categorical structures in a FP language (e.g. Haskell, ML) since such a language is around functions and values. I doubt that such categorical structures should be considered patterns.
On other hand, Haskell or ML does not come from the category theory, it comes from PCF as a language which is created to make program correctness proving is "easy".
I dont want to mean someone using this book to prove mathematical theorems, I just want to say that it's superficial (about both category theory and computer science), and does not bring sufficient knowledge upon that we can build nontrivial results.
I find the ubiquitous idea is that "category theory" is more prestigous than "set theory", and some programmers, instead of seriously learning mathematics, think that learning category theory would fill up their lack of knowledge (in mathematics). It's quite contrary since category theory alone (i.e. without context) is trivial.
Let's be honest: read this book and the series of the author, and try to use the acquired knowledge to prove some (even simple) mathematical theorems.
> ...accepting the existence of the reals means that there are numbers that exist but can never be described ...we can never interact with these numbers even conceptually
is also full of vagueness: what is "be described"/"interact"?
Conceptually, a "pure" function is something as `A -> B`, so all information about its internal (e.g. side effects) lost: we put something of type A but we can only observe a result of type B.
The idea of computation monads is to attach the result type of the function with a "constructor" T, then the type T B is used to "restore" (or to reason about) the lost information.
In composing such functions, T X (for some result type X) is all information we need, then this explains naturally the third rule of the Kleisli triple `f: A -> T B; g: B -> T C`: A -> T C
I have a similar impression when reading posts elsewhere about categorical structures in programming: they are repetitive and mostly trivial (actually, the category theory without context is trivial).