En la teoría de tipos y los lenguajes de programación , una variable de tipo es una variable matemática que se extiende sobre los tipos . Incluso en los lenguajes de programación que permiten variables mutables , una variable de tipo sigue siendo una abstracción, en el sentido de que no corresponde a algunas ubicaciones de memoria.
Los lenguajes de programación que admiten el polimorfismo paramétrico utilizan variables de tipo cuantificadas universalmente . Los lenguajes que admiten tipos existenciales hacen uso de variables de tipo cuantificadas existencialmente . Por ejemplo, el siguiente código OCaml define una función de identidad polimórfica que tiene un tipo cuantificado universalmente, que el intérprete imprime en la segunda línea:
# sea id x = x ;; val id : ' a -> ' a = < divertido >
En notación matemática, el tipo de función id
es, dónde es una variable de tipo.