Tipo variable

En la teoría de tipos y en los lenguajes de programación , una variable de tipo es una variable matemática que abarca varios 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 ninguna ubicación 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 utilizan 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:

#  deja que  id  x  =  x ;; 
val  id  :  ' a  ->  ' a  =  < fun >

En notación matemática, el tipo de la función ides , donde es una variable de tipo. ${\displaystyle \paratodos aa\a a}$${\estilo de visualización a}$

• Sistema F