If they want a dependently typed language, why not use one? Lean is good, and I don't think it has any significant downside wrt Haskell other than more limited library ecosystem (but I guess AI can translate Haskell libraries to Lean very effectively).
Articles like this always make me wonder "there could be something interesting about this", but they always assume I know more math (or something) than I do.
Does anyone write about these kinds of topics in a more approachable manner, or is the math just so inherent to this, that I need to learn that first? (And if so, what do I need to read to learn that?)
I'll admit to only having read the first few chapters, but it came across as an approachable intro to the math.
Most of the functional programming-related math is very simple, especially when framing it/contextualizing it to programming (e.g. using data types instead of sets, interfaces instead of "algebras", etc).
There's two minor gotchas:
- functional programming's math is mostly rooted in algebra and category theory, whereas most math education from elementary through university focuses on analysis and calculus
- it is still math after all, and you're required to go step-by-step building definitions in a mathematical fashion. If you want to understand what a monad is, you need to understand what a functor is. To understand what a functor is, you need to understand what a type constructor (such as Array, List, Record or Option) and a map function are.
If you're interested, I have a (now archived) repository that explains the fundamentals of functional programming through TypeScript and fp-ts library, and it does so in a very strict mathematical, but very approachable regardless of education, fashion.
You could check the magma and semigroup paragraphs, they are short, to get a taste of it.
Obviously, it's math, so you're expected to learn those definitions (albeit they are very simple to understand and easy to remember) and practice it a bit by thinking/implementing a handful of magmas and semigroups, then moving on to concepts that build upon those (monoid, ordering, functor, etc) by adding more constraints.
I want to underline that fact that this stuff is not "read and move to the next chapter."
A lot of this kind of "machinery" in functional programming and category theory turns out to be essentially extremely abstract "superclasses" or "traits". In fact, many of them are too abstract to actually be defined in most programming languages. So they may appear as "design patterns" rather than actual definitions, if the language isn't quite expressive enough.
So to understand these ideas, you have to ask the questions:
1. Why this abstraction, and not a slightly different one?
2. What are some concrete examples of this abstraction? (Usually this feels like, "So, huh, familiar things X, Y and Z are all the same, viewed from this particular angle.")
3. What almost fits this abstraction, but not quite? And why?
4. Now that I see this pattern includes a whole bunch of interesting things, can I do anything useful with that?
A good example of (2) is realizing that futures, Rust's Result and Option, and Python's list/stream/etc compressions are almost the same thing, from a certain angle.
But it takes a while to collect all the related examples and to work through the connections carefully. The common patterns are usually really simple once you finally see them, which is part of the problem. They patterns are so abstract and cover so many things that it takes a while to work through the implications, and to decide if something is genuinely useful. Some very simple and widespread patterns will turn out to be boring, because they don't correspond to any problems you've ever seen.
The main issue I kept running into with Haskell is that the machinery feels haphazardly implemented.
Sure, the concept of a monoid makes sense, but (at least a few years ago) why isn't a Haskell monoid defined as an extension of a semigroup? And even these days: where's magma?
What makes monads special enough to warrant its own first-class syntax and dozens of predefined instances, while dealing with a Sum or Product monoid feels like an afterthought?
If functors are as basic and fundamental as they seem, why do they get an awkward "fmap" - with most standard types re-exporting it as plain "map"?
Programming in Haskell felt like I was dealing with a random collection of category theory concepts thrown together in a weekend, rather than a mature and well-designed programming language. I have no doubt that there's some very solid reasoning behind it all, but the Haskell documentation does an awful job answering the questions you stated. And let's not even mention giving them programmer-friendly names rather than something a German mathematician chose 150 years ago...
> thrown together in a weekend, rather than a mature
The fact that it wasn't thrown together in a weekend is the reason why we have both map and fmap, and why monoid wasn't originally an extension of semigroup (it is now). Haskell started out without that, then later added fmap and semigroup.
In any case, those are not real concerns when programming with Haskell. The actual concerns are more like "why do I have to wait for all this lens dependency stuff to compile just to fetch an url" or "why does the language server need so much ram"
If they want a dependently typed language, why not use one? Lean is good, and I don't think it has any significant downside wrt Haskell other than more limited library ecosystem (but I guess AI can translate Haskell libraries to Lean very effectively).
Articles like this always make me wonder "there could be something interesting about this", but they always assume I know more math (or something) than I do.
Does anyone write about these kinds of topics in a more approachable manner, or is the math just so inherent to this, that I need to learn that first? (And if so, what do I need to read to learn that?)
The author has a series of blog posts introducing category theory to programmers: https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
I'll admit to only having read the first few chapters, but it came across as an approachable intro to the math.
Most of the functional programming-related math is very simple, especially when framing it/contextualizing it to programming (e.g. using data types instead of sets, interfaces instead of "algebras", etc).
There's two minor gotchas:
- functional programming's math is mostly rooted in algebra and category theory, whereas most math education from elementary through university focuses on analysis and calculus
- it is still math after all, and you're required to go step-by-step building definitions in a mathematical fashion. If you want to understand what a monad is, you need to understand what a functor is. To understand what a functor is, you need to understand what a type constructor (such as Array, List, Record or Option) and a map function are.
If you're interested, I have a (now archived) repository that explains the fundamentals of functional programming through TypeScript and fp-ts library, and it does so in a very strict mathematical, but very approachable regardless of education, fashion.
You could check the magma and semigroup paragraphs, they are short, to get a taste of it.
Obviously, it's math, so you're expected to learn those definitions (albeit they are very simple to understand and easy to remember) and practice it a bit by thinking/implementing a handful of magmas and semigroups, then moving on to concepts that build upon those (monoid, ordering, functor, etc) by adding more constraints.
It's not read and move to the next chapter.
https://github.com/enricopolanski/functional-programming
I want to underline that fact that this stuff is not "read and move to the next chapter."
A lot of this kind of "machinery" in functional programming and category theory turns out to be essentially extremely abstract "superclasses" or "traits". In fact, many of them are too abstract to actually be defined in most programming languages. So they may appear as "design patterns" rather than actual definitions, if the language isn't quite expressive enough.
So to understand these ideas, you have to ask the questions:
1. Why this abstraction, and not a slightly different one?
2. What are some concrete examples of this abstraction? (Usually this feels like, "So, huh, familiar things X, Y and Z are all the same, viewed from this particular angle.")
3. What almost fits this abstraction, but not quite? And why?
4. Now that I see this pattern includes a whole bunch of interesting things, can I do anything useful with that?
A good example of (2) is realizing that futures, Rust's Result and Option, and Python's list/stream/etc compressions are almost the same thing, from a certain angle.
But it takes a while to collect all the related examples and to work through the connections carefully. The common patterns are usually really simple once you finally see them, which is part of the problem. They patterns are so abstract and cover so many things that it takes a while to work through the implications, and to decide if something is genuinely useful. Some very simple and widespread patterns will turn out to be boring, because they don't correspond to any problems you've ever seen.
The main issue I kept running into with Haskell is that the machinery feels haphazardly implemented.
Sure, the concept of a monoid makes sense, but (at least a few years ago) why isn't a Haskell monoid defined as an extension of a semigroup? And even these days: where's magma?
What makes monads special enough to warrant its own first-class syntax and dozens of predefined instances, while dealing with a Sum or Product monoid feels like an afterthought?
If functors are as basic and fundamental as they seem, why do they get an awkward "fmap" - with most standard types re-exporting it as plain "map"?
Programming in Haskell felt like I was dealing with a random collection of category theory concepts thrown together in a weekend, rather than a mature and well-designed programming language. I have no doubt that there's some very solid reasoning behind it all, but the Haskell documentation does an awful job answering the questions you stated. And let's not even mention giving them programmer-friendly names rather than something a German mathematician chose 150 years ago...
> thrown together in a weekend, rather than a mature
The fact that it wasn't thrown together in a weekend is the reason why we have both map and fmap, and why monoid wasn't originally an extension of semigroup (it is now). Haskell started out without that, then later added fmap and semigroup.
In any case, those are not real concerns when programming with Haskell. The actual concerns are more like "why do I have to wait for all this lens dependency stuff to compile just to fetch an url" or "why does the language server need so much ram"
I was hoping for applications.
I was hoping for Lean 4.