Container Compendium

Desc.idr

3 min read

The List Container

Containers, when interpreted as type descriptors, hold a shape for data in their first argument, and positions inside the aforementionned shape. In the case of list, the shape is given by a natural number which describes its length. The positions are all the possibles values for a given shape. Since the shape is the number of elements, the positions are given by a type that has the same number of inhabitants as the length of the list. This way, a list of 3 elements, hosts 3 values.

public export
ListCont : Container
ListCont = (len : Nat) !> Fin len

Again, using the extension \defref{def:extension} we obtain the corresponding functor in 

public export
TyList : Type -> Type
TyList = Ex ListCont

We can now construct inhabitants for our bespoke list type, for example, the constructors for the empty list, and the constructor for cons:

public export
Nil : TyList a
Nil = MkEx Z absurd
 
public export
Cons : a -> TyList a -> TyList a
Cons x ls = MkEx (S ls.ex1) (elimFin x ls.ex2)

Lemma

is isomorphic to List.

public export covering
tyListToList : TyList x -> List x
tyListToList (MkEx Z y) = []
tyListToList (MkEx (S n) y) = y FZ :: (tyListToList (MkEx n (y . FS)))
 
public export
listToTyList : List x -> TyList x
listToTyList [] = Nil
listToTyList (y :: xs) = Cons y (listToTyList xs)
 
public export covering
toFrom : {0 a : Type} -> (x : List a) -> tyListToList (listToTyList x) = x
toFrom [] = Refl
toFrom (x :: xs) = cong (x ::) (cong tyListToList exEta `trans` toFrom xs)
 
 
public export covering
0 fromTo : (v : TyList x) -> listToTyList (tyListToList v) = v
fromTo (MkEx Z f) = cong2Dep' MkEx Refl (allUninhabited _ _)
fromTo (MkEx (S n) f) = let
    pat = (fromTo (MkEx n (f . FS)))
  in exEqToEq $ MkExEq
      (cong S $ sym $ exP1 $ sym pat)
      (\xx => Calc $
           |~ elimFin
                 (f FZ)
                 ((listToTyList (tyListToList (MkEx n (f . FS)))).ex2)
                 xx
           ~~ elimFin
                 (f FZ)
                 ((MkEx {cont = ListCont} n (f . FS)).ex2)
                 (transport Fin (cong S (sym (exP1 (sym pat)))) xx)
              ...(rewrite pat in cong (elimFin (f FZ) (f . FS)) (sym $ applyTransport ? ?))
           ~~ elimFin
                 (f FZ)
                 (f . FS)
                 (transport Fin (cong S (sym (exP1 (sym pat)))) xx)
              ...(Refl)
           ~~ f (transport Fin (cong S (sym (exP1 (sym pat)))) xx)
              ...(elimFinF f ?)
      )
 
public export covering
tyListIso : TyList x ≅ List x
tyListIso = MkIso
  tyListToList
  listToTyList
  toFrom
  fromTo