Converting between algebraic effects and monads

monads.u

-- 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