Definition.idr

Maybe Functors

There are two Maybe functors in $\mathcal{C}ont$ and 3 ways to define them each. We start with the most straightforward definition.

Definition

The “Maybe any” functor $Mayb{e}_{Any}(A,\bar{A})\mapsto (m:MaybeA,Any\bar{A}m)$ maps queries into queries that can fail, and responses into responses that must be present.

namespace Any
  public export
  Maybe : Container -> Container
  Maybe c = (x : Maybe c.request) !> Any c.response x

Definition

The “Maybe all” functor $Mayb{e}_{All}(A,\bar{A})\mapsto (m:MaybeA,All\bar{A}m)$ maps queries into queries that can fail, and responses into optional responses.

namespace All
  public export
  Maybe : Container -> Container
  Maybe c = (x : Maybe c.request) !> All c.response x

Those definitions rely on the All \defref{def:maybe-all} and Any \defref{def:maybe-any} types that transform a predicate to run conditionally on a Maybe value.