Functor polinomial (teoría de tipos)

En teoría de tipos , un functor polinomial (o functor contenedor ) es una especie de endofunctor de una categoría de tipos íntimamente relacionado con el concepto de tipos inductivos y coinductivos . Específicamente, todos los tipos W (o tipos M) son (isomorfos a) álgebras iniciales (o coalgebras finales ) de dichos functores.

Los functores polinomiales se han estudiado en el contexto 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 al 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 signatura ^{[ 2 ]} o contenedor . ^{[ 3 ]} El functor polinomial asociado al contenedor ( A , B ) se define de la siguiente manera: ^{[ 4 ] [ 5 ] [ 6 ]}

${\displaystyle {\begin{aligned}P:U&\longrightarrow U\\X&\longmapsto \sum _{a:A}(B(a)\to X)\end{aligned}}}$

Cualquier functor naturalmente isomorfo a P se denomina functor contenedor . ^{[ 7 ]} La acción de P sobre las funciones se define por

${\displaystyle {\begin{aligned}P:(X\to Y)&\longrightarrow (PX\to PY)\\f\qquad &\longmapsto \left((a,g)\mapsto (a,g\circ f)\right)\end{aligned}}}$

Tenga en cuenta que esta asignación solo es verdaderamente funtorial en teorías de tipos extensionales (ver #Propiedades ).

En las teorías de tipos intensionales, tales funciones no son verdaderamente functores, porque el tipo universo no es estrictamente una categoría (el campo de la teoría de tipos homotópicos se dedica a explorar cómo el tipo universo se comporta más como una categoría superior ). Sin embargo, es functor hasta igualdades proposicionales, es decir, los siguientes tipos identidad están habitados:

${\displaystyle {\begin{aligned}P(f\circ g)&=Pf\circ Pg\\P({\mathsf {id}}_{X})&={\mathsf {id}}_{PX}\end{aligned}}}$

para cualesquiera funciones f y g y cualquier tipo X , donde${\displaystyle {\mathsf {id}}_{X}}$es la función identidad en el tipo X . ^{[ 8 ]}

• Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Contenedores: Construcción de tipos estrictamente positivos" . Theoretical Computer Science . 342 (1): 4. CiteSeerX 10.1.1.166.34 . doi : 10.1016/j.tcs.2005.06.002 . 
• Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (12 de abril de 2015). Árboles no bien fundados en la teoría de tipos homotópicos . Actas Internacionales Leibniz en Informática (LIPIcs). Vol.  38. págs. 17–30 . arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN  9783939897873. S2CID 15020752 . 
• Programa de Fundamentos Univalentes (2013). Teoría de tipos homotópicos: Fundamentos Univalentes de las Matemáticas . Instituto de Estudios Avanzados. pág.  159.
• Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2012-01-18). "Tipos inductivos en la teoría de tipos homotópicos". arXiv : 1201.3898 [ math.LO ].
• Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2015-04-21). "Álgebras iniciales de homotopía en teoría de tipos". arXiv : 1504.05531 [ math.LO ].

• Una extensa colección de notas sobre functores polinomiales.