En informática , la recursividad polimórfica (también conocida como tipificación Milner - Mycroft o cálculo de Milner-Mycroft ) se refiere a una función recursiva paramétricamente polimórfica donde el parámetro de tipo cambia con cada invocación recursiva realizada, en lugar de permanecer constante. La inferencia de tipos para la recursión polimórfica es equivalente a la semiunificación y, por lo tanto, es indecidible y requiere el uso de un semialgoritmo o anotaciones de tipo proporcionadas por el programador . [1]
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 -> Int longitud Epsilon = 0 longitud ( _ :<: xs ) = 1 + longitud xs Tenga en cuenta que Haskell normalmente infiere la firma de tipo para una función tan simple como esta, pero aquí no se puede omitir sin provocar un error de tipo.
En el análisis de programas basado en tipos, la recursividad polimórfica suele ser esencial para obtener una alta precisión del análisis. Ejemplos notables de sistemas que emplean recursividad polimórfica incluyen el análisis del tiempo de enlace de Dussart, Henglein y Mossin [2] y el sistema de gestión de memoria basado en la región Tofte-Talpin . [3] Como estos sistemas asumen que las expresiones ya han sido escritas en un sistema de tipos subyacente (no es necesario que emplee recursión polimórfica), la inferencia puede volver a ser decidible.
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 los árboles. En las dos citas que siguen, Okasaki (págs. 144-146) ofrece 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 tenga un solo elemento, el segundo un par, el tercero un par de pares, etc. de forma recursiva, estableciendo un patrón automático de búsqueda de errores en el tipo de datos. Roberts (p. 171) ofrece un ejemplo relacionado en Java , utilizando una clase para 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 recursión polimórfica con una estructura de sustitución de pila anidada inicial, temporal y final. [5]