There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this means is that some pure higher order functions do not admit translation from pure to monadic arguments, or from monadic to applicative ones. While there are beautiful abstractions that collapse and rebuild enormous depths of pure recursion in a blink of an eye, traversing a filesystem is a pain.
I specifically have two examples back there on Stack Overflow that I will refer to now:
While there has been quite some impressive hand-waving and heuristic arguments that the precise translation is impossible, I'm still somewhat unhappy as a foundation for exact reasoning about such issues seems lacking.
In the first case above, it seems very plausible that we cannot have a function convergeM of type [m a] -> [m a] -- only of [m a] -> m [a], but I don't know how to go about obtaining an argument of ELI5 level of convincingness.
In the second case, it is shown that, going some way, we can reach a point where a monadic function is necessary, but there is still space to be suspicious: what if there is another way to go that will lead to an applicative function being needed instead?
I want to have some grasp on issues like this, some proven ground under my feet. Given that category theory does not support higher order functions, what can be done?
