Recursividad polimórfica

En la informática , la recursión polimórfico (también referido como Milner - Mycroft typability o el cálculo Milner-Mycroft ) se refiere a un recursiva paramétricamente polimórfica función donde hicieron los cambios de parámetros de tipo con cada invocación recursiva, en vez de permanecer constante. La inferencia de tipo para la recursividad polimórfica es equivalente a la semi-unificación y, por lo tanto, indecidible y requiere el uso de un semi-algoritmo o anotaciones de tipo suministradas por el programador . ^[1]

Ejemplo

Tipos de datos anidados

Considere el siguiente tipo de datos anidado :

datos  anidados  a  =  a  : <:  ( anidados  [ a ])  |  Epsilon infixr  5  : <:anidado  =  1  : <:  [ 2 , 3 , 4 ]  : <:  [[ 5 , 6 ], [ 7 ], [ 8 , 9 ]]  : <:  Epsilon

Una función de longitud definida sobre este tipo de datos será polimórficamente recursiva, ya que el tipo de argumento cambia de Nested aa Nested [a]en la llamada recursiva:

longitud  ::  Anidado  a  ->  Longitud int Epsilon = 0 longitud ( _ : <: xs ) = 1 + longitud xs           

Tenga en cuenta que Haskell normalmente infiere la firma de tipo para una función de apariencia tan simple como esta, pero aquí no se puede omitir sin desencadenar un error de tipo.

Tipos de mayor rango

Ver también: tipo de rango superior

Esta sección necesita expansión . Puedes ayudar agregando más . ( Mayo de 2012 )

Aplicaciones

Análisis de programas

En el análisis de programas basado en tipos, la recursividad polimórfica es a menudo esencial para obtener una alta precisión del análisis. Ejemplos notables de sistemas que emplean la recursividad polimórfica incluyen el análisis de tiempo de unión de Dussart, Henglein y Mossin ^[2] y el sistema de gestión de memoria basado en la región de Tofte-Talpin . ^[3] Como estos sistemas asumen que las expresiones ya se han escrito en un sistema de tipos subyacente (no es necesario que emplee la recursividad polimórfica), la inferencia se puede volver a hacer decidible.

Estructuras de datos, detección de errores, soluciones gráficas

Las estructuras de datos de programación funcional a menudo utilizan la recursividad polimórfica para simplificar las comprobaciones de errores de tipo y resolver problemas con desagradables soluciones temporales "intermedias" que devoran memoria en estructuras de datos más tradicionales, como árboles. En las dos citas que siguen, Okasaki (págs. 144-146) da un ejemplo de CONS en Haskell en el que el sistema de tipos polimórficos señala automáticamente los errores del programador. ^[4] El aspecto recursivo es que la definición de tipo asegura que el constructor más externo tiene un solo elemento, el segundo un par, el tercero un par de pares, etc. de forma recursiva, estableciendo un patrón de búsqueda automática de errores en el tipo de datos. Roberts (p. 171) da un ejemplo relacionado en Java , usando una clasepara representar un marco de pila. El ejemplo dado es una solución al problema de la Torre de Hanoi en el que una pila simula la recursividad polimórfica con una estructura de sustitución de pila anidada inicial, temporal y final. ^[5]

Ver también

• Polimorfismo de mayor rango

Notas

1. Henglein 1993 .
2. Dussart, Dirk; Henglein, Fritz ; Mossin, Christian. "Calificaciones de subtipo y recursión polimórfica: análisis de tiempo de unión polimórfica en tiempo polinomial" . Actas del 2º Simposio Internacional de Análisis Estático (SAS) .
3. Tofte, Mads ; Talpin, Jean-Pierre (1994). "Implementación del cálculo λ de llamada por valor usando una pila de regiones". POPL '94: Actas del 21º simposio ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación . Nueva York, NY, EE.UU .: ACM. págs. 188–201. doi : 10.1145 / 174675.177855 . ISBN 0-89791-636-0.
4. Chris Okasaki (1999). Estructuras de datos puramente funcionales . Nueva York: Cambridge. pag. 144. ISBN 978-0521663502.
5. Eric Roberts (2006). Pensar de forma recursiva con Java . Nueva York: Wiley. pag. 171 . ISBN 978-0471701460.

Otras lecturas

• Meertens, Lambert (1983). "Verificación incremental de tipos polimórficos en B" (PDF) . Simposio de ACM sobre principios de lenguajes de programación (POPL), Austin, Texas .
• Mycroft, Alan (1984). Esquemas de tipos polimórficos y definiciones recursivas . Simposio Internacional de Programación, Toulouse, Francia . Apuntes de conferencias en Ciencias de la Computación. 167 . págs. 217–228. doi : 10.1007 / 3-540-12925-1_41 . ISBN 978-3-540-12925-7.
• Henglein, Fritz (1993). "Inferencia de tipos con recursividad polimórfica". Transacciones ACM sobre lenguajes y sistemas de programación . 15 (2): 253–289. CiteSeerX  10.1.1.42.3091 . doi : 10.1145 / 169701.169692 .
• Kfoury, AJ ; Tiuryn, J .; Urzyczyn, P. (abril de 1993). "Tipo de reconstrucción en presencia de recursividad polimórfica". Transacciones ACM sobre lenguajes y sistemas de programación . 15 (2): 290–311. doi : 10.1145 / 169701.169687 . ISSN  0164-0925 .
• Michael I. Schwartzbach (junio de 1995). "Inferencia de tipo polimórfico" . Informe técnico BRICS-LS-95-3 .
• Emms, Martin ; Leiß, Hans (1996). "Ampliación del verificador de tipo para SML por recursividad polimórfica: una prueba de corrección" . Informe técnico 96-101 .
• Richard Bird y Lambert Meertens (1998). "Tipos de datos anidados" .
• C. Vasconcellos, L. Figueiredo, C. Camarao (2003). " Inferencia de tipo práctica para la recursividad polimórfica: una implementación en Haskell ". Revista de Ciencias de la Computación Universal .
• L. Figueiredo, C. Camarao. " Inferencia de tipo para definiciones recursivas polimórficas: una especificación en Haskell ".
• Hallett, J. J; Kfoury, AJ (julio de 2005). "Ejemplos de programación que necesitan recurrencia polimórfica" . Notas electrónicas en informática teórica . 136 : 57-102. doi : 10.1016 / j.entcs.2005.06.014 . ISSN  1571-0661 .

enlaces externos

• ML estándar con recursión polimórfica por Hans Leiß, Universidad de Munich

Recursividad polimórfica

Recursividad polimórfica

Este artículo relacionado con la programación de computadoras es un fragmento . Puedes ayudar a Wikipedia expandiéndolo .

• v
• t
• mi