Monad.idr

Maybe Monads

The main contribution of this work is in this module: Monads on containers.

While monads on containers aren’t a surprising fact in itself, it is noteworthy to see that they provide us with similar capabilities than monads on types and functions, but in the realm of bidirectional programming.

The first step in defining our maybe monad is to chose the maybe functor for which we are going to carry out the proof. For pedagical purposes, we start with proving that the functor written using data types in idris \defref{prop:maybe-functor-idris} is a monad. Then we will prove that $Maybe⊳\_$ is a monad via the $⊳$ monoid.

Monads are identified by their unit : 1 -> m a and mult : m (m a) -> m a operation. Here m is Maybe ▷ and 1 is the identity functor on containers defined as Unit :- Void. With this knowledge, we build the unit mapping:

unit : (a : Container) -> a =%> Any.Maybe a
unit _ = Just <! (\x, y => y.unwrap)

We now need to prove that just is natural, that is, given any other morphism m : a =%> b, composing unit after m is the same as functorially mapping m after unit: $m;{\text{unit}}_b={\text{unit}}_a;Mayb{e}_{Any}(m)$. Or graphically, the following diagram commutes:

Programatically it means we need to implement the function:

%unbound_implicits off
MaybeAnyIsNatural : {0 a, b : Container} ->
                    (m : a =%> b) ->
                    m |%> unit b <%≡%> unit a |%> mapHom Any.MaybeF a b m
MaybeAnyIsNatural (fwd <! bwd) = MkDepLensEq
    (\arg => Refl)
    (\arg, wrg => Refl)

Thankfully the proofs are quite simple.

Those two functions are enough to define the first part of our monad: the unit natural transformation:

unitNT : Functor.idF Cont =>> Any.MaybeF
unitNT = MkNT
    unit
    (\_, _, arg => depLensEqToEq (MaybeAnyIsNatural arg))

The second part is the multiplication natural transformation, which states that for any monad $m$ we have $m(ma)\to ma$, in our case, this takes the form of a morphism

public export
mult : (x : Container) -> Any.Maybe (Any.Maybe x) =%> Any.Maybe x
mult container = joinMaybe <! anyJoin

It is left to prove that join is natural, we do the same as we did for unit:

JoinIsNatural : {0 a, b : Container} ->
    (m : a =%> b) ->
    mapHom Any.MaybeF (Any.Maybe a) (Any.Maybe b) (mapHom Any.MaybeF a b m) |%> mult b
    <%≡%> mult a |%> mapHom Any.MaybeF a b m

Which is the expected naturality square $\text{MaybeAny}(\text{MaybeAny}(m));mult=mult;(\text{MaybeAny}(m))$.

The proof of this square is a bit more involved and is left in appendix.

joinNT : (Any.MaybeF ⨾⨾ Any.MaybeF) =>> Any.MaybeF
joinNT = MkNT
  mult
  (\a, b, m => depLensEqToEq (joinCommutes a b m))

Equipped with those two natural transformation, and the MaybeAny functor, we have proven that our functor is also a monad. We can make sure of that fact by building a value of type Monad \defref{def:monad}

MaybeAnyMonad : Monad Cont Any.MaybeF
MaybeAnyMonad = MkMonad
  { unit = unitNT
  , mult = joinNT
  , square = \c => depLensEqToEq (monadSquare c)
  , identityLeft = \c => depLensEqToEq $ MkDepLensEq (\_ => Refl) (\_, _ => Refl)
  , identityRight = \c => depLensEqToEq $ MkDepLensEq
      (\case Nothing => Refl
             (Just x) => Refl)
      (\case Nothing => \x => absurd x
             (Just x) => \(Aye y) => Refl)
  }
  where
    monadSquare : (x : Container) ->
                  (Any.mapMaybe (mult x) |%> mult x)
                  <%≡%>
                  (mult (Any.Maybe x) |%> mult x)
    monadSquare x = MkDepLensEq
        (\case Nothing => Refl
               (Just y) => Refl)
        (\case Nothing => \y => absurd y
               (Just y) => \_ => Refl)

Maybe Monad arising from the Maybe Monoid

All this effort can be saved by deriving the monad instance from the monoidal structor of $MaybeCont$ in $\mathcal{C}ont$.

First we build a self-action in $\mathcal{C}ont$ from the monoidal structure of $⊳$.

MaybeMonoidAction : Action Cont Cont SequenceMonoidal
MaybeMonoidAction = monoidalSelfAction SequenceMonoidal

Then we turn the action into a lax-action and use that to produce the monad. The monoid object is given by the fact that $MaybeCont$ is a monoid with regards to the $⊳$ monoidal structure in $\mathcal{C}ont$

namespace Any
  public export
  MaybeMonad : Monad Cont MaybeSeq
  MaybeMonad =
    MonadFromLaxAction ? ? Cont Cont SequenceMonoidal
      (relax MaybeMonoidAction) Cont.MaybeMonoidCompose

We do the same for the All.Maybe monad as the partially applied functor $MaybeCont▶\_$.

namespace All
  MaybeMonad : Monad Cont MaybeAllSeq
  MaybeMonad =
    MonadFromLaxAction Container Container ContCart Cont
      Cart.SequenceMonoidal
      ForallLaxAction
      Cart.MaybeMonoidCompose