En teoría de tipos , un funtor polinomial (o funtor contenedor ) es una especie de endofuntor de una categoría de tipos que está íntimamente relacionada con el concepto de tipos inductivos y coinductivos . Específicamente, todos los tipos W (resp. tipos M) son (isomorfos a) álgebras iniciales (resp. coalgebras finales ) de dichos funtores.
Los funtores polinómicos se han estudiado en el marco más general de un pretopos con tipos Σ; [1] este artículo trata únicamente de las aplicaciones de este concepto dentro de la categoría de tipos de una teoría de tipos estilo Martin-Löf .
Sea U un universo de tipos, sea A : U , y sea B : A → U una familia de tipos indexada por A . El par ( A , B ) a veces se denomina firma [2] o contenedor . [3] El funtor polinomial asociado al contenedor ( A , B ) se define de la siguiente manera: [4] [5] [6]
Cualquier funtor naturalmente isomorfo a P se llama funtor contenedor . [7] La acción de P sobre funciones está definida por
Tenga en cuenta que esta asignación no solo es verdaderamente funcional en las teorías de tipos extensionales (ver #Propiedades ).
En las teorías de tipos intensionales, tales funciones no son realmente funtores, porque el tipo de universo no es estrictamente una categoría (el campo de la teoría de tipos de homotopía se dedica a explorar cómo el tipo de universo se comporta más como una categoría superior ). Sin embargo, es funcional hasta igualdades proposicionales, es decir, se habitan los siguientes tipos de identidad: