Desc.idr

The Maybe container

In categories of containers by Abbott etc, Containers are used as descriptions for data structures that carry values. The Maybe type is one of them and can be described as a container using the extension on containers Ex : Container -> Type -> Type.

To define the Maybe container, we need to define a boolean predicate. This is nothing more than a dependent type that is indexed over a boolean value, and that is inhabited with a trivial value when the boolean is true.

public export
data IsTrue : Bool -> Type where
  TT : IsTrue True

Using this predicate, we build the Maybe container by setting the shapes as Bool and the positions with our IsTrue predicate.

Definition

The maybe container is given by a boolean and a predicate that this boolean is valued to True.

public export
MaybeCont : Container
MaybeCont = (isJust : Bool) !> IsTrue isJust

Using this container with the extension \defref{def:extension}, we obtain the Maybe functor in $\mathcal{S}et$.

public export
Maybe : Type -> Type
Maybe = Ex MaybeCont

Just like the Maybe type of Prelude, we can define Just and Nothing constructors

public export
Just : (x : a) -> Desc.Maybe a
Just x = MkEx True (\_ => x)
 
public export
Nothing : Desc.Maybe a
Nothing = MkEx False absurd

And we can even prove that they are isomorphic.

Lemma

Prelude.Maybe and $[[MaybeCont]]$ are isomorphic

fromDesc : Desc.Maybe a -> Prelude.Maybe a
fromDesc (MkEx False p) = Nothing
fromDesc (MkEx True p) = Just (p TT)
 
toDesc : Prelude.Maybe a -> Desc.Maybe a
toDesc Nothing = Nothing
toDesc (Just x) = Just x
 
toFromEq : {0 a : Type} -> (x : Prelude.Maybe a) -> fromDesc (toDesc x) === x
toFromEq Nothing = Refl
toFromEq (Just x) = Refl
 
0 fromToEq : {0 a : Type} -> (x : Desc.Maybe a) -> toDesc (fromDesc x) === x
fromToEq (MkEx True p) = cong (MkEx True) (funExt $ \TT => Refl)
fromToEq (MkEx False p) = cong (MkEx False) (allUninhabited _ _)
 
public export
MaybeIso : Desc.Maybe a ≅ Prelude.Maybe a
MaybeIso = MkIso fromDesc toDesc toFromEq fromToEq

Sometimes it is helpful to define the maybe container as $1+I$

MaybeCont' : Container
MaybeCont' = One + I