En los lenguajes de programación , el borrado de tipos es el proceso en tiempo de carga mediante el cual las anotaciones de tipos explícitas se eliminan de un programa, antes de que se ejecute en tiempo de ejecución . La semántica operativa 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 tipo. En el contexto de la programación genérica , lo opuesto al borrado de tipos se denomina cosificación . [1]
La operación inversa se denomina inferencia de tipos . Aunque el borrado de tipos puede ser una manera fácil de definir la escritura en lenguajes escritos implícitamente (un término escrito implícitamente está bien escrito si y sólo si es el borrado de un término lambda escrito explícitamente y bien escrito ), no proporciona una regla de inferencia para esta definición.