After a long hiatus, diving back into Lambda the Ultimate is a bracing intellectual shock. I was reasonably au fait with Type Theory, and even had enough rudiments of Category Theory to make accurate analogies to code constructs, but to my horror I’ve realised that my knowledge has since evaporated from the saucer.
Anyway, a common refrain from the anti-eggheads is that the mathematically founded approaches are inferior because they won’t get through to the rank-and-file programmer. While I don’t despute the likely veracity of the latter portion of that contention, I ascribe responsibility quite differently.
There are lots of programmers whose knowledge is the rote memorisation of libraries, rather than fluency with fundamental concepts, and their difficulty with algebraic reasoning is what should be challenged. Mathematically-based approaches are clearer and simpler, than the esoterica that has been transmitted by immersion and osmosis; however these former approaches use logical implication rather than analogistic “reasoning”, and don’t pretend complexity doesn’t exist.
If monads – a solidly defined concept – were taught as unrelentingly as the vaguely specified and logically suspect object orientation, we would get far fewer complaints about how monads will never be able to compete with the latest fad du jour.