(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
— that's quite too unspecific. The shapes-and-positions description helps, but in
we are essentially using
rather than shapes and positions.
The type of strictly-positive free monads over containers has a rather straightforward definition, but the type of
monads looks simpler to me (and in a sense
monads are even better than usual
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?
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:
Σ
Code:
⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A
Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)we are essentially using
Code:
ΣThe type of strictly-positive free monads over containers has a rather straightforward definition, but the type of
Code:
Freer
Code:
Freer
Code:
FreeSo what can we do with containers in a nicer way than with descriptions or something else?