En la teoría de tipos , los contenedores son abstracciones que permiten representar de manera uniforme varios "tipos de colección", como listas y árboles . Un contenedor ( unario ) se define por un tipo de formas S y una familia de tipos de posiciones P, indexadas por S. La extensión de un contenedor es una familia de pares dependientes que consta de una forma (de tipo S) y una función de posiciones de esa forma al tipo de elemento. Los contenedores pueden verse como formas canónicas para los tipos de colección. [1]
Para las listas, el tipo de forma son los números naturales (incluido el cero). Los tipos de posición correspondientes son los tipos de números naturales menores que la forma, para cada forma.
Para los árboles, el tipo de forma es el tipo de árboles de unidades (es decir, árboles sin información en ellos, solo estructura). Los tipos de posición correspondientes son isomorfos a los tipos de rutas válidas desde la raíz hasta los nodos particulares de la forma, para cada forma.
Tenga en cuenta que los números naturales son isomorfos a las listas de unidades. En general, el tipo de forma siempre será isomorfo a la familia de tipos de contenedor no genérico original (lista, árbol, etc.) aplicada a la unidad.
Una de las principales motivaciones para introducir la noción de contenedores es admitir la programación genérica en un entorno de tipificación dependiente . [1]
Aspectos categóricos
La extensión de un contenedor es un endofunctor . Se necesita una función g
para
Esto es equivalente a lo familiar map g
en el caso de las listas, y hace algo similar para otros contenedores.
Contenedores indexados
Los contenedores indexados (también conocidos como functores polinomiales dependientes ) son una generalización de contenedores, que pueden representar una clase más amplia de tipos, como los vectores (listas de tamaño). [2]
El tipo de elemento (llamado tipo de entrada ) está indexado por forma y posición, por lo que puede variar según la forma y la posición, y la extensión (llamada tipo de salida ) también está indexada por forma.
Ver también
Referencias
- ^ a b Michael Abbott; Thorsten Altenkirch; Neil Ghani (2005). "Contenedores: Construyendo tipos estrictamente positivos". Informática Teórica . 342 (1): 3-27. doi : 10.1016 / j.tcs.2005.06.002 .
- ^ Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride y Peter Morris. "Contenedores indexados" (PDF) . Manuscrito inédito . Consultado el 30 de octubre de 2008 . Cite journal requiere
|journal=
( ayuda )CS1 maint: varios nombres: lista de autores ( enlace )
enlaces externos
- Blog de tipos de contenedores