4 ms·
As someone who studies both CS and pure math, it's quite interesting when I see posts that take a very operational reading of functors and monads, instead of it
by siraben 5y ago
As someone who studies both CS and pure math, it's quite interesting when I see posts that take a very operational reading of functors and monads, instead of its shorter and more precise categorical definition (as a mapping from one category to another that acts homomorphically over morphisms). That's not necessarily wrong, but it's an important thing to keep in mind when learning category theory through a programming context (e.g. Category Theory for Programmers by Milewski). When I tried to learn category theory in this way, past a certain point the abstractions felt too unnatural and arbitrary (e.g. lack of examples for adjunctions and free objects), whereas a good mathematical treatment of category theory would provide plenty of examples across different areas of mathematics such as algebra, topology and logic.
I strongly agree with valenterry's comment[1] here, that post gives is an approximate definition of functors, even omitting the functor law. In particular, it is explaining what an endofunctor is (in the context of FP, you mostly deal with one category anyway). Furthermore, even in Haskell, there is no such thing as the category of Haskell types[0] (because of things like divergence and partiality).
For the curious, I've recommended Program Design By Calculation[2] to a number of people to show how category theory can be used as a powerful tool to reason about programs in an FP context while not compromising on the mathematics (the target audience is undergrad CS majors).
EDIT: In particular, I have a bit of issue with this sentence after stating the signature of fmap, since it does not reference lawfulness.
> This is the full definition. There is no additional hidden machinery that Haskell is somehow automatically invoking when you "use a Functor".
[0] http://math.andrej.com/2016/08/06/hask-is-not-a-category/ http://math.andrej.com/2016/08/06/hask-is-not-a-category/
[1] https://news.ycombinator.com/item?id=27638565 https://news.ycombinator.com/item?id=27638565
[2] https://www4.di.uminho.pt/~jno/ps/pdbc.pdf https://www4.di.uminho.pt/~jno/ps/pdbc.pdf
- drdeca 5y agoDo you happen to know of any programming language which has explicit support for multiple categories?
- hiker 5y agoLean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes. [0] https://leanprover.github.io/programming_in_lean/#01_Introduction.html https://leanprover.github.io/programming_in_lean/#01_Introdu... [1] https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category/default.lean#L92 https://github.com/leanprover-community/mathlib/blob/master/...
- ebingdom 5y ago> Furthermore, even in Haskell, there is no such thing as the category of Haskell types[0] (because of things like divergence and partiality). Divergence and partiality can easily be modeled by the category of complete partial orders and Scott-continuous maps. This is what you learn in, e.g., a course on domain theory and/or denotational semantics. Andrej Bauer is mainly arguing that Hask isn't a category because no one has formally specified it. For example, we would need to come up with a policy on when two arrows are considered equal, and it's not clear what that notion of equality should be.
- siraben 5y agoRight, domain theory and denotational semantics let you talk about ⊥ in an order-theoretic setting, and I think it's also rich in connections between topology and lambda calculus. Though it might be the case that if functors already pose a pedagogical conundrum for programmers, Scott-continuity might be even harder to get across. A quote from Bauer's post is particularly relevant: > [I am arguing against] the fact that some people find it acceptable to defend broken mathematics on the grounds that it is useful. Non-broken mathematics is also useful, as well as correct. Good engineers do not rationalize broken math by saying “life is tough”.
- catgary 5y agoBrauer has clearly had a different experience with classical mechanics and engineering physics courses than I did…
- bcrosby95 5y agoBecause most people suck at taking abstract mathematical concepts and seeing how they could apply to code. Including me. Let's take the definition of a function: > A function is a relation for which each value from the set the first components of the ordered pairs is associated with exactly one value from the set of second components of the ordered pair. Cool, I have no idea what the fuck this means and how it is useful to me. Oh wait, I use them every day.
- siraben 5y agoThat is the first definition stated in first-order logic, sure. But the operational reading of a (computable) function being something that takes in input and produces an output (via some algorithm) is still correct. It is possible to be both clear and correct with operational analogies. However, monads and functors don't readily admit an easy operational reading like functions.
- hiker 5y ago> Cool, I have no idea what the fuck this means and how it is useful to me. > Oh wait, I use them every day. Do you really? Do the `functions` you use even fit the above definition? I bet you can think of infinite number of functions (bool -> bool). The above definition admits only 4 such functions.
- bb010g 5y agoThere are only 4 (2**2) such pure functions. For type (Bool -> IO Bool), there are infinite (∞**2) such pure functions.