Functor.idr

Proposition

$M a y b e_{A n y}$ is a functor in $C o n t$

namespace Any
 
  public export
  mapMaybe : a =%> b -> Any.Maybe a =%> Any.Maybe b
  mapMaybe x = map x.fwd <! (\y, z => anyFunctorMap x.fwd x.bwd y z)
 
  public export
  MaybeF : Endo Cont
  MaybeF = MkFunctor Any.Maybe (\_, _ => Any.mapMaybe)
  -- proofs in appendix

In functional programming, the Maybe type can also be conceptualised as Maybe x = 1 + x where 1 is the unit (or terminal) type. This intuition also holds in the category of containers.

Proposition
There is a Maybe functor defined by $M a y b e_{1 +} (A, \overset{ˉ}{A}) \mapsto 1 + (A, \overset{ˉ}{A})$
MaybeCoprod : Endo Cont
MaybeCoprod = applyL {a = Cont, b = Cont} One CoprodContBifunctor

Those two previous definitions are isomorphic, because they are functors, we define a natural isomorphism between them.

Lemma

$M a y b e_{1 +}$ and $M a y b e_{A n y}$ are isomorphic.

AnyCoprodIso : ContIso (Any.Maybe x) (MaybeCoprod .mapObj x)
AnyCoprodIso = MkGenIso toCoprod fromCoprod toFrom fromTo
  where
    toCoprod : {0 x : Container} -> Any.Maybe x =%> MaybeCoprod .mapObj x
    toCoprod = maybeToCoprod <! (\case Nothing => absurd
                                       (Just y) => Aye)
 
    fromCoprod : {0 x : Container} -> MaybeCoprod .mapObj x =%> Any.Maybe x
    fromCoprod = coprodToMaybe <! (\case (<+ y) => absurd
                                         (+> y) => .unwrap)
 
    toFrom : {x : Container} ->
             (toCoprod {x} |%> fromCoprod {x}) <%≡%> identity (Any.Maybe x)
    toFrom = MkDepLensEq
        (\case Nothing => Refl
               (Just y) => Refl)
        (\case Nothing => \yx => absurd yx
               (Just y) => \(Aye z) => Refl)
 
    fromTo : {x : Container} ->
             (fromCoprod {x} |%> toCoprod {x}) <%≡%> identity (MaybeCoprod .mapObj x)
    fromTo = MkDepLensEq
        (\case (<+ ()) => Refl
               (+> x) => Refl)
        (\case (<+ ()) => \y => absurd y
               (+> x) => \_ => Refl)

Finally, there is a third way to define the maybe functor and that is by using the sequencing product and the maybe container $M a y b e C o n t$ \defref{def:maybecont}.

Proposition
There is a Maybe functor defined by $M a y b e_{▷} (A, \overset{ˉ}{A}) = M a y b e C o n t ⊳ (A, \overset{ˉ}{A})$
public export
MaybeSeq : Endo Cont
MaybeSeq = applyL {a = Cont, b = Cont} MaybeCont Cont.SequenceBifunctor

What if we didn’t use Any but it’s counterpart All? We get similar constructions with similar properties.

Proposition

$M a y b e_{A ll}$ is a functor in $C o n t$

namespace All
  public export
  mapMaybe : a =%> b -> All.Maybe a =%> All.Maybe b
  mapMaybe x = map x.fwd <! (\y, z => allFunctorMap x.fwd x.bwd y z)
 
  public export
  MaybeF : Endo Cont
  MaybeF = MkFunctor All.Maybe (\_, _ => All.mapMaybe)

Proposition
There is a Maybe functor defined by $M a y b e_{▶} c \mapsto M a y b e C o n t ▶ c$
  MaybeAllSeq : Endo Cont
  MaybeAllSeq = applyL {a = ContCart, b = Cont} MaybeCont ForallSeqBifunctor

Proposition
There is a Maybe functor defined by $M a y b e_{I +} c \mapsto I + c$
  MaybeCoprod : Endo Cont
  MaybeCoprod = applyL {a = Cont, b = Cont} I CoprodContBifunctor

Like before, $M a y b e_{A ll}$ , $M a y b e_{I +}$ and $M a y b e_{▶}$ are all isomorphic.

Lemma

$M a y b e_{I +}$ and $M a y b e_{▶}$ are isomorphic

Lemma

and $M a y b e_{A ll}$ and $M a y b e_{I +}$ are isomorphic

Container Compendium

Explorer

Functor.idr