Closed KingoftheHomeless closed 4 years ago
coool! how the heck does this work? and what is it useful for?
So I've discovered a few issues with this, but first a lengthy explanation of how this works:
So the cataSem
combinator transforms Sem r a
into its church encoding; Sem r
is the free monad of the functor Union r (Sem r)
, and cataSem
allows us to do folding over the layers of Union r (Sem r)
that Sem r
represents.
The premise is that we use cataSem
to fold Sem (ErrorFuture e ': r) a
to m (Either e a)
, where m
is the internal monad, from the innermost Union (ErrorFuture e ': r) (Sem (ErrorFuture e ': r))
to the outermost Union (ErrorFuture e ': r) (Sem (ErrorFuture e ': r))
; i.e. from the last action to the first.
This is reflected in the base case: a -> m (Either e a)
, which represents the end of the computation, and the inductive step:
Union (ErrorFuture e ': r) (Sem (ErrorFuture e ': r)) (m (Either e a))
-> m (Either e a)
The inner m (Either e a)
represents what we've already folded: i.e. the rest of the computation past the action that the Union (ErrorFuture e ': r) (Sem (ErrorFuture e ': r))
represents. Thus, ex
of the Union
's Weaving
actually has type f x -> m (Either e a)
; a continuation!
So cataSem
enables talking about continuations of Sem r
, in a way that's more expressive than Codensity (Sem r)
, but doesn't necessarily require the problematic type variable of ContT s (Sem r)
.
In this case, we use cataSem
in order to catch exceptions of the continuation. Throwing an exception is straight-forward: if the Union
is ThrowPast e
, then we simply return pure (Left e)
, discarding the (inaccessible) continuation. If the Union
is CatchFuture
, we first run the continuation by providing Nothing
: ex (Nothing <$ s)
. We then check if this results in an exception raised by ThrowPast e
; and if it does, we rerun the continuation, providing the exception to it; ex (Just e <$ s)
. This is only done once to make the effect flexible.
Coroutine
was problematic since its functorial state needed to be stacks of continuations delimited by yield
s and receive
s, and thus higher-order effects only applied up until the first yield
/receive
. ErrorFuture
doesn't need to represent that, so it doesn't have the same problem.
Now the problems:
So the point was that this should've been a unproblematic continuation-based effect, which would be useful for a lot of continuation-based stuff. One example would be that it's possible to emulate knot
using this. However, the more I look at it, the more I realize that it's actually very similar to runContViaFresh
: runContViaFresh
also functions by catching exceptions on continuations, the differences are that runContViaFresh
does so through combining ContT s
with an Error
effect, while this does it via cataSem
. And indeed, runErrorFuture
inherits a problem that runContViaFresh
needed to fix: a catchFuture
within an argument to a higher-order action won't catch exceptions after the higher-order action. So this isn't as nice as I first thought.
I'm going to look at this a bit more, but ultimately, it might be too problematic/too similar to runContViaFresh
to be worth including. Although perhaps I can make use of cataSem
to make the implementation of runContViaFresh
prettier.
I've abandoned this. The weave
abstraction hates continuations, and I hate it in return.
Here's an interesting effect, made possible using the same kind of machinery the abandoned Coroutine effect used, but with a functorial state that actually behaves sensibly with higher-order effects: