Skip to content

Instantly share code, notes, and snippets.

@pchiusano

pchiusano/monads.u

Last active Apr 24, 2020
Embed
What would you like to do?
Converting between algebraic effects and monads
-- This gist shows how we can use abilities to provide nicer syntax for any monad.
-- We can view abilities as "just" providing nicer syntax for working with the
-- free monad.
ability Monadic f where
eval : f a -> a
-- Here's a monad, encoded as a first-class value with
-- two polymorphic functions, `pure` and `bind`
type Monad f = Monad (forall a . a -> f a) (forall a b . f a -> (a -> f b) -> f b)
use Monad Monad
Monad.pure : Monad f -> a -> f a
Monad.pure = cases Monad pure _ -> pure
Monad.bind : Monad f -> f a -> (a -> f b) -> f b
Monad.bind = cases Monad _ bind -> bind
-- Just as we can interpret `Free f a` into `f a` given a monad
-- for `f`, we can interpret a `'{Monadic f} a` into `f a` given
-- a monad for `f`.
--
do : Monad f -> '{Monadic f} a -> f a
do m actions = match m with
Monad pure bind ->
go = cases
{a} -> pure a
{Monadic.eval fa -> k} -> bind fa (a -> handle k a with go)
handle !actions with go
use Optional
optionalMonad : Monad Optional
optionalMonad =
bind : Optional a -> (a -> Optional b) -> Optional b
bind oa f = match oa with
None -> None
Some a -> f a
Monad Some bind
> do optionalMonad 'let
x = eval (Some 1)
1 + eval (Some 2)
--- output
I found and typechecked these definitions in ~/unison7/u.u. If you do an `add` or `update`,
here's how your codebase would change:
⍟ These new definitions are ok to `add`:
type Monad f
ability Monadic f
Monad.bind : Monad f -> f a -> (a -> f b) -> f b
Monad.pure : Monad f -> a -> f a
do : Monad f -> '{Monadic f} a -> f a
optionalMonad : Monad Optional
Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels.
42 | > do optionalMonad 'let
Some 3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.