I wonder if starting with the functor and the free monad is actually helping here - it seems like a lot of work with the potential for pitfalls. Would it be better to start by defining a canonical representation for the effect (r->a for reader, [message] for logging) and then defining the injection from that into Free and then defining the inverse such that Free composition does the correct thing (i.e. doing the “normalization by evaluation” in reverse). Or equivalently, just defining what monadic bind does for our type i.e. not using the Free construct at all?
The main advantage of the Free construct is that we have composition by Functor composition. But that only punts the problem of composition to the interpreter. I’m not sure whether “‘algebraic” as defined here is equivalent to being distributive/commutative, but effects that commute with / distribute over each other are trivial to handle in any number of ways. The difficult part is when they don’t, e.g. when combining try/catch with logging, it’s not at all clear whether we should skip a log message in an operation that’s skipped due to an exception. In mtl-land the order of stacking the monads expresses the order in which their effects will be applied, and it’s cumbersome because it forces the user to actually express that. The linked paper seems to duck the problem by saying that catch is not an algebraic effect. “the denotation of a blurb of code is the composition of the denotation of its pieces” helps us not at all because the denotation of a try/catch and the denotation of a log don’t compose.
Straightforward composition of effects that distribute is pretty trivial (I did so in scalaz-transfigure; I did require the user to use type annotations to express the desired order but that could easily be dropped), and “distributes over any monad” effects can be expressed straightforwardly via a typeclass; I don’t know whether this page represents innovation in terms of doing it efficiently (less interested in that). But I think it’s completely ducking the really relevant question, which is finding good ways to express effects that don’t necessarily distribute.
The problem is how do you know to start with r -> a or [message]? That was not obvious to me, but this gives me a systematic approach to getting there. Which is the linked paper? I’m not seeing a link :)
r -> a
Sorry, I meant http://gallium.inria.fr/blog/lawvere-theories-and-monads/ .
To me it’s more natural to think “I want a reader, this is r -> a” than to think “I want a reader, this is something that obeys the law (get >>= (λ s → get >>= λ s' → k s s' )) ≃ (get >>= λ s → k s s ). I guess if you have an algebraic definition rather than an extensional one and you can’t see a type that "happens” to be the quotient you want then the technique would be useful - I’m just not convinced that would happen in practice.
(get >>= (λ s → get >>= λ s' → k s s' )) ≃ (get >>= λ s → k s s )