Borrado de tipo

En los lenguajes de programación , el borrado de tipos es el proceso en tiempo de carga mediante el cual se eliminan las anotaciones de tipo explícitas de un programa, antes de su ejecución en tiempo de ejecución . La semántica operacional que no requiere que los programas vayan acompañados de tipos se denomina semántica de borrado de tipos , en contraste con la semántica de paso de tipos . La semántica de borrado de tipos es un principio de abstracción que garantiza que la ejecución en tiempo de ejecución de un programa no dependa de la información de tipos. En el contexto de la programación genérica , lo opuesto al borrado de tipos se denomina reificación . ^{[ 1 ]}

La operación inversa se denomina inferencia de tipos . Si bien el borrado de tipos puede ser una forma sencilla de definir la tipificación en lenguajes con tipado implícito (un término con tipado implícito está bien tipado si y solo si es el borrado de un término lambda con tipado explícito y bien tipado ), no proporciona reglas de inferencia para esta definición.

• Plantilla (C++)
• Problemas con el borrado de tipos (en Genéricos en Java )
• Monomorfización
• Polimorfismo de tipo

• Crary, Karl; Weirich, Stephanie ; Morrisett, Greg (2002). "Polimorfismo intensional en la semántica de borrado de tipos". Journal of Functional Programming . 12 (6): 567– 600. CiteSeerX 10.1.1.5.4507 . doi : 10.1017/S0956796801004282 .