Container (type theory)

<h2 id="categorical-aspects">Categorical aspects</h2>

<p>The extension of a container is an <a href="/facts/Endofunctor/l2u3rIBE">endofunctor</a>. It takes a function g to
</p>

λ
        (
        s
        ,
        f
        )
        .
        (
        s
        ,
        g
        ∘
        f
        )
      
    
    {\displaystyle \lambda (s,f).(s,g\circ f)}

<p>This is equivalent to the familiar map g in the case of lists, and does something similar for other containers.
</p>
<h2 id="indexed-containers">Indexed containers</h2>

<p>Indexed containers (also known as dependent polynomial functors) are a generalisation of containers, which can represent a wider class of types, such as vectors (sized lists).<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a>
</p><p>The element type (called the <i>input type</i>) is indexed by shape and position, so it can vary by shape and position, and the extension (called the <i>output type</i>) is also indexed by shape.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Container_(abstract_data_type)/gsC5UcqD">Container (abstract data type)</a></li>
<li><a href="/facts/Polynomial_functor_(type_theory)/FJtQNgcp">Polynomial functor (type theory)</a></li></ul>

<h2 id="external-links">External links</h2>
<ul><li><a href="https://web.archive.org/web/20160428024201/http://sneezy.cs.nott.ac.uk/containers/blog/">Container Types</a> blog</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Michael Abbott; Thorsten Altenkirch; Neil Ghani (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 3–27. CiteSeerX 10.1.1.166.34. doi:10.1016/j.tcs.2005.06.002. <a href="https://doi.org/10.1016%2Fj.tcs.2005.06.002" target="_blank">https://doi.org/10.1016%2Fj.tcs.2005.06.002</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Michael Abbott; Thorsten Altenkirch; Neil Ghani (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 3–27. CiteSeerX 10.1.1.166.34. doi:10.1016/j.tcs.2005.06.002. <a href="https://doi.org/10.1016%2Fj.tcs.2005.06.002" target="_blank">https://doi.org/10.1016%2Fj.tcs.2005.06.002</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. "Indexed Containers" (PDF). Unpublished manuscript. Retrieved 2008-10-30. {{cite journal}}: Cite journal requires |journal= (help)CS1 maint: multiple names: authors list (link) <a href="/wiki/Conor_McBride" target="_blank">/wiki/Conor_McBride</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Container (type theory) open-in-new

Container (type theory)