Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Distributive Algebra #361

Merged
merged 75 commits into from
Mar 13, 2020
Merged

Distributive Algebra #361

merged 75 commits into from
Mar 13, 2020

Conversation

robrix
Copy link
Contributor

@robrix robrix commented Mar 3, 2020

Building on #359, this PR replaces the monad homomorphism passed to alg with an initial state and a well-behaved distributive law, obviating the need for the Effect class altogether.

@robrix robrix mentioned this pull request Mar 3, 2020
4 tasks
@robrix robrix changed the title Distributive algebra Distributive Algebra Mar 3, 2020
@robrix robrix marked this pull request as ready for review March 12, 2020 12:31
Copy link
Contributor Author

@robrix robrix left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🚀

Comment on lines -85 to +127
send = alg id . inj
send sig = runIdentity <$> alg (fmap Identity . runIdentity) (inj sig) (Identity ())
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similar to #359, we pass in the identity arrow. This time, however, that arrow isn’t a monad homomorphism but rather a distributive law over the Identity context.

Comment on lines +80 to +85
alg
:: Functor ctx
=> Handler ctx n m -- ^ A 'Handler' lowering computations inside the effect into the carrier type @m@.
-> sig n a -- ^ The effect signature to be interpreted.
-> ctx () -- ^ The initial state.
-> m (ctx a) -- ^ The interpretation of the effect in @m@.
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Relative to thread and #359, this signature is somewhat different:

  1. We use the Handler type synonym to make it clear what the purpose of the distributive law is.

  2. We take the initial context in the final position, after the signature. This makes it clear that this is an algebra from sig n a to ctx () -> m (ctx a), remembering that the handler reduces (context-borne) actions in n to (context-bearing) actions in m, i.e. we have what is essentially sig (ctx ~> m :.: ctx) ~> ctx ~> m :.: ctx).

Comment on lines -109 to +153
alg hom = \case
Ask k -> \ r -> hom (k r) r
Local f m k -> \ r -> hom (k (hom m (f r))) r
alg hdl sig ctx = case sig of
Ask k -> \ r -> hdl (k r <$ ctx) r
Local f m k -> \ r -> hdl (fmap k (hdl (m <$ ctx) (f r))) r
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We lose LambdaCase with the new parameter ordering, but it could be recovered by writing this tacitly in the context functor, e.g. writing the initial action as a continuation from ctx () and then composing continuations with >=>. I’ve opted not to do that here because it doesn’t make the instances any clearer.

Comment on lines -39 to +40
-- | A @Handler@ is a function that interprets effects described by @sig@ into the carrier monad @m@.
newtype Handler sig m = Handler
{ runHandler :: forall s n x . Monad n => (forall y . n y -> InterpretC s sig m y) -> sig n x -> InterpretC s sig m x }
-- | An @Interpreter@ is a function that interprets effects described by @sig@ into the carrier monad @m@.
newtype Interpreter sig m = Interpreter
{ runInterpreter :: forall ctx n s x . Functor ctx => Handler ctx n (InterpretC s sig m) -> sig n x -> ctx () -> InterpretC s sig m (ctx x) }
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was never a handler (which is what we call functions like runState), but rather an interpreter which now takes a handler.

Comment on lines -77 to +76
:: (forall n x . Monad n => (forall y . n y -> StateC s m y) -> s -> eff n x -> m (s, x))
:: (forall ctx n x . Functor ctx => Handler ctx n (StateC s m) -> eff n x -> s -> ctx () -> m (s, ctx x))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As with the context, the state s should follow the signature: runInterpretState interprets eff into (stateful) arrows modulo ctx.

dst :: NonDetC Identity (n a) -> m (NonDetC Identity a)
dst = runIdentity . runNonDet (liftA2 (liftA2 (<|>))) (Identity . runNonDetA . hom) (pure (pure empty))
dst :: NonDetC Identity (NonDetC m a) -> m (NonDetC Identity a)
dst = runIdentity . runNonDet (liftA2 (liftA2 (<|>))) (Identity . runNonDetA) (pure (pure empty))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Decomposing the distributive laws (by passing them separately to thread) allows you to understand both in isolation more easily.

Comment on lines 14 to -19
deriving instance Functor m => Functor (Catch e m)

instance Effect (Catch e) where
thread ctx handler (Catch m h k) = Catch (handler (m <$ ctx)) (handler . (<$ ctx) . h) (handler . fmap k)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not only do we no longer require the Effect instance, but we also don’t require the Functor instance. I intend to remove it in a future PR.

Comment on lines -55 to +58
alg hom = \case
L eff -> Labelled (alg (runLabelled . hom) (L (runLabelled eff)))
R sig -> Labelled (alg (runLabelled . hom) (R sig))
alg hdl = \case
L eff -> Labelled . alg (runLabelled . hdl) (L (runLabelled eff))
R sig -> Labelled . alg (runLabelled . hdl) (R sig)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here’s a cute example of an algebra point-free in the context.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Request for docs: Manual implementation of Effect instances
1 participant