Cuantificación acotada

En teoría de tipos , la cuantificación acotada (también polimorfismo acotado o genericidad restringida ) se refiere a cuantificadores universales o existenciales que están restringidos ("acotados") para abarcar solo los subtipos de un tipo particular. La cuantificación acotada es una interacción del polimorfismo paramétrico con la subtipificación . La cuantificación acotada 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 .

Descripción general

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 . Supone un modelo basado en registros para las 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 los objetos se representan como funciones que no toman argumentos y devuelven un objeto. El comportamiento específico es entonces un nombre de función junto con los tipos de los argumentos y el tipo de retorno. La cuantificación limitada considera todos los objetos con dicha función. Un ejemplo sería una minfunción polimórfica que considera todos los objetos que son comparables entre sí. ^{[ cita requerida ]}

Cuantificación limitada por f

La cuantificación acotada por F o cuantificación acotada recursivamente , introducida en 1989, permite una tipificación más precisa de funciones que se aplican a tipos recursivos. Un tipo recursivo es aquel que incluye una función que lo utiliza como tipo para algún argumento o su valor de retorno.^[1]

Ejemplo

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 utilizar esto como información de tipificación en funciones polimórficas . La Test.minfunción utiliza cuantificación acotada simple y no garantiza que los objetos sean comparables entre sí, a diferencia de la Test.fMinfunción que utiliza cuantificación acotada F.

En notación matemática, los tipos de las dos funciones son

mín: ∀ T, ∀ S ⊆ {comparar con: T → int}. S → S → S

fMín: ∀ T ⊆ Comparable[T]. T → T → T

dónde

Comparable[T] = {compararCon: T → int}

Interfaz  comparable < T > { 

    int compararCon ( T otro );  

}

La clase pública Integer implementa Comparable < Integer > {     

    @Override 
public int compareTo ( Entero otro ) { // ... } }        
        
    


La clase pública String implementa Comparable < String > {     

    @Override 
public int compareTo ( String otro ) { // ... }        
        
    

}

public class Test { public static void main ( String [] args ) { final String a = min ( "gato" , "perro" ); final Integer b = min ( 10 , 3 ); final Comparable c = min ( "gato" , 3 ); // Lanza ClassCastException en tiempo de ejecución final String str = fMin ( "gato" , "perro" ); final Integer i = fMin ( 10 , 3 ); // final Object o = fMin("gato", 3); // No compila } public static < S extends Comparable > S min ( S a , S b ) { if ( a . compareTo ( b ) <= 0 ) { return a ; } else { return b ; } } public static < T extends Comparable < T >> T fMin ( T a , T b ) { if ( a . compareTo ( b ) <= 0 ) { return a ; } de lo contrario { devolver b ; } }   
    
         
             
             
              
             
             
        
    
    
              
            
             
          
             
        
    
    
              
            
             
          
             
        
    

}

Véase también

Notas

^ Polimorfismo limitado por F para programación orientada a objetos. Canning, Cook , Hill, Olthof y Mitchell . http://dl.acm.org/citation.cfm?id=99392

Referencias

Cardelli, Luca ; Wegner, Peter (diciembre de 1985). "Sobre la comprensión de los tipos, la abstracción de datos y el polimorfismo" (PDF) . ACM Computing Surveys . 17 (4): 471–523. CiteSeerX 10.1.1.117.695 . doi :10.1145/6041.6042. ISSN 0360-0300. S2CID 2921816.
Peter S. Canning, William R. Cook , Walter L. Hill, John C. Mitchell y William Olthoff. "Polimorfismo limitado por F para programación orientada a objetos". En Conferencia sobre lenguajes de programación funcional y arquitectura informática , 1989.
Benjamin C. Pierce "Tipos de intersección y polimorfismo acotado". Lecture Notes in Computer Science 664 , 1993.
Gilad Bracha , Martin Odersky , David Stoutamire y Philip Wadler . "Hacer que el futuro sea seguro para el pasado: agregar genericidad al lenguaje de programación Java". En Programación orientada a objetos: sistemas, lenguajes, aplicaciones (OOPSLA). ACM, octubre de 1998.
Andrew Kennedy y Don Syme . "Diseño e implementación de genéricos para .NET Common Language Runtime". En Diseño e implementación de lenguajes de programación , 2001.
Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . MIT Press. ISBN 978-0-262-16209-8.Capítulo 26: Cuantificación acotada