Functor.idr

List Functors in

Like Maybe, there are multiple ways to define the List functor in containers. The first one is using a “direct” style and use the definitions in $\mathcal{S}et$ to build a monad on containers. This is Any.List

Definition

The “Any” List functor in containers is given by $List(A,\bar{A})=(xs:ListA,Any\bar{A}xs)$

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

  public export
  mapList : a =%> b -> List a =%> List b
 
  public export
  ListF : Cont ->> Cont
  ListF = MkFunctor Any.List (\_, _ => mapList) ?bb ?cc
 
  match : List a =%> One + (a * List a)
  match =
      matchFwd <! matchBwd
      where
        matchFwd : List a.msg -> () + (a.msg * List a.msg)
        matchFwd [] = <+ ()
        matchFwd (x :: xs) = +> (x && xs)
 
        matchBwd :
          (xs : List (a .request)) -> (One + (a * List a)).res (matchFwd xs) -> Any (a .response) xs
        matchBwd [] x = absurd x
        matchBwd (y :: xs) (<+ x) = Here x
        matchBwd (y :: xs) (+> x) = There x
 
  export
  reduce : (a * b =%> b) ->
           One =%> b ->
           Any.List a =%> b
  reduce m initial =
    let handleRec : a * List a =%> b
        handleRec = identity a ~*~ (assert_total $ reduce m initial) |%> m
    in match |%>
      (initial
      ~+~
      handleRec |%> dia)

Just like Maybe, we can also define the list functor using our sequence product ▷.

Definition

The “Any” List functor as a the $ListCont⊳\_$ functor

public export
Forany : Container -> Container
Forany = (ListCont ▷)

And we prove that they are isomorphic.

Lemma

Forany and List are isomorphic

ForanyListIso : (c : Container) -> ContIso (Forany c) (Any.List c)

Proving that Forany is a functor is easy done by applying the $⊳$ bifunctor to the $ListCont$ container.

public export
ForanyFunctor : Endo Cont
ForanyFunctor = applyBifunctor {a = Cont, b = Cont} ListCont SequenceBifunctor

Any in $\mathcal{S}et$ has a counterpart, All, we use that counterpart to build the other list functor on containers.

Definition

The “All” List functor on containers is given by $List(A,\bar{A})=(xs:ListA,All\bar{A}xs)$

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

  public export
  mapList : a =%> b -> All.List a =%> All.List b
  mapList lens = map lens.fwd <! composeMap
    where
      composeMap : (xs : List a.request) ->
                   All b.response (map lens.fwd xs) ->
                   All a.response xs
      composeMap [] ys = []
      composeMap (x :: xs) (y :: ys) = lens.bwd x y :: composeMap xs ys
 
  export
  elimI : All.List I =%> I
  elimI = const () <! elimBwd
    where
     elimBwd : (x : List ()) -> () -> All (\x => ()) x
     elimBwd [] y = []
     elimBwd (x :: xs) y = () :: elimBwd xs y
 
  public export
  ListF : Cont ->> Cont
  ListF = MkFunctor All.List ?ww ?ee ?rr

This definition is isomorphic to the partially applied bifunctor $ListCont▶\_$.

Proposition

The “Forall” list functor on containers is given by $List(A,\bar{A})=ListCont▶(A,\bar{A})$

public export
Forall : Container -> Container
Forall = (ListCont ▶)

And we prove that they are the same.

Lemma

$Foralla=ListCont▶a$ is Isomorphic to $List(A,\bar{A})=(ls:ListA,All\bar{A}ls)$

The statement that Forall is a functor is given by the partially applied action $ListCont▶\_$

public export
ForallFunctor : Endo Cont
ForallFunctor = applyL {a = ContCart, b = Cont} ListCont ForallSeqBifunctor