En la teoría de tipos , la cuantificación acotada (también polimorfismo acotado o genérico restringido ) se refiere a cuantificadores universales o existenciales que están restringidos ("acotados") para abarcar solo los subtipos de un tipo particular. La cuantificación limitada es una interacción de polimorfismo paramétrico con subtipificación . La cuantificación limitada se ha estudiado tradicionalmente en el entorno funcional de System F <:, pero está disponible en lenguajes orientados a objetos modernos que admiten polimorfismo paramétrico ( genéricos) como Java , C # y Scala .
El propósito de la cuantificación limitada es permitir que las funciones polimórficas dependan de algún comportamiento específico de los objetos en lugar de la herencia de tipos . Asume un modelo basado en registros para clases de objetos, donde cada miembro de la clase es un elemento de registro y todos los miembros de la clase son funciones con nombre. Los atributos de objeto se representan como funciones que no toman ningún argumento y devuelven un objeto. El comportamiento específico es entonces algún nombre de función junto con los tipos de argumentos y el tipo de retorno. La cuantificación acotada permite considerar todos los objetos con tal función. Un ejemplo sería una minfunción polimórfica que considera todos los objetos que son comparables entre sí.
La cuantificación acotada por F o la cuantificación acotada recursivamente , introducida en 1989, permite una tipificación más precisa de funciones que se aplican en tipos recursivos. Un tipo recursivo es aquel que incluye una función que lo usa como tipo para algún argumento o su valor de retorno. [1]
Este tipo de restricción de tipo se puede expresar en Java con una interfaz genérica. El siguiente ejemplo demuestra cómo describir tipos que se pueden comparar entre sí y usar esto como información de escritura en funciones polimórficas . La Test.minfunción utiliza una cuantificación acotada simple y no conserva el tipo de los tipos asignados, a diferencia de la Test.Fminfunción que utiliza la cuantificación acotada por F.