# Why do we need containers?

#### admin

##### Administrator
Staff member
(As an excuse: the title mimics the title of <a href="https://stackoverflow.com/questions/28139259/why-do-we-need-monads">Why do we need monads?</a>)

There are <a href="http://www.sciencedirect.com/science/article/pii/S0304397505003373" rel="nofollow noreferrer">containers</a> (and <a href="http://strictlypositive.org/indexed-containers.pdf" rel="nofollow noreferrer">indexed</a> ones) (and <a href="https://pigworker.wordpress.com/2015/06/06/hasochistic-containers-a-first-attempt/" rel="nofollow noreferrer">hasochistic</a> ones) and <a href="http://www.ioc.ee/~james/papers/levitation.pdf" rel="nofollow noreferrer">descriptions</a>. But containers are <a href="http://mazzo.li/epilogue/index.html?p=324.html" rel="nofollow noreferrer">problematic</a> and to my very small experience it's harder to think in terms of containers than in terms of descriptions. The type of non-indexed containers is isomorphic to
Code:
``Σ``
— that's quite too unspecific. The shapes-and-positions description helps, but in

Code:
``````⟦_⟧ᶜ : ∀ {α β γ} -&gt; Container α β -&gt; Set γ -&gt; Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -&gt; Pos sh -&gt; A

Kᶜ : ∀ {α β} -&gt; Set α -&gt; Container α β
Kᶜ A = A ◃ const (Lift ⊥)``````

we are essentially using
Code:
``Σ``
rather than shapes and positions.

The type of strictly-positive free monads over containers has a rather straightforward definition, but the type of
Code:
``Freer``
monads looks simpler to me (and in a sense
Code:
``Freer``
monads are even better than usual
Code:
``Free``
monads as described in the <a href="http://okmij.org/ftp/Haskell/extensible/more.pdf" rel="nofollow noreferrer">paper</a>).

So what can we do with containers in a nicer way than with descriptions or something else?