[tw1010]

This is excellent. But man, I don't think I can ever go back to not feeling like there's a huge pedagogical gap between the local maxima the functional programming explanations engineers are typically exposed to, and the much higher (though probably still not a global maxima) point that pure mathematicians have been adapted into. I just wish we'd embrace the geometric (topological, differential geometrical) threads that a lot of these concepts (like lifts etc) are connected to, instead of being arbitrarily tied to a pedagogy textured by the sociological context that coding originated from (i.e. heavily influenced by logicians etc).

[uryga]

What threads do you mean? (The only thing that comes to mind is HoTT stuff, but that's kind of over my head for now)

[AlexCoventry]

What's an example of a coding problem which would benefit from all that abstraction?

[tw1010]

While I sympathize with your sentiment – and share the mindset during my day job – I believe that this type of "what practical applications does this have"-thinking is making us short-sighted and preventing us from being able to move past our current local maxima, to cross the adaptive valley[1].

I'm not expecting the whole engineering field to start exploring the question of what pure mathematics (and not some watered down for-engineers version) can do to fundamentally transform the the way programmers think and talk about what it is they do. But the fact that there are almost zero people from the geometric side of pure mathematics (though again, there are plenty of logicians) working together with everyday programmers, that's what I wish I saw more of every time I see one of these explanations of functional programming that seem almost always to be pedagogically colored by logicians hands.

[1] https://www.edge.org/response-detail/23879

[AlexCoventry]

Cross the valley, sure, but what points to the valley right now? Useful abstractions arise out of concrete issues with present approaches. What are some of the concrete issues in software development which this abstraction could help with?

[0xdeadbeefbabe]

Games