En teoría de tipos , se dice que un sistema de tipos tiene la propiedad de tipo principal si, dado un término y un entorno, existe un tipo principal para este término en este entorno, es decir, un tipo tal que todos los demás tipos para este término en este entorno son una instancia del tipo principal.
La propiedad de tipo principal es deseable para un sistema de tipos, ya que proporciona una manera de tipificar expresiones en un entorno determinado con un tipo que abarca todos los tipos posibles de las expresiones, en lugar de tener varios tipos posibles incomparables. La inferencia de tipos para sistemas con la propiedad de tipo principal generalmente intentará inferir el tipo principal.
Por ejemplo, el sistema ML tiene la propiedad de tipo principal y los tipos principales para una expresión se pueden calcular mediante el algoritmo de unificación de Robinson , que se utiliza en el algoritmo de inferencia de tipos de Hindley-Milner . Sin embargo, muchas extensiones del sistema de tipos de ML, como la recursión polimórfica , pueden hacer que la inferencia del tipo principal sea indecidible. Otras extensiones, como los tipos de datos algebraicos generalizados de Haskell , destruyen la propiedad de tipo principal del lenguaje, lo que requiere el uso de anotaciones de tipo o que el compilador "adivine" el tipo deseado entre varias opciones.
La propiedad de tipificación principal requiere que, dado un término, exista una tipificación (es decir, un par con un contexto y un tipo) que sea una instancia de todas las tipificaciones posibles del término. La propiedad de tipificación principal se puede confundir con la propiedad de tipo principal, pero son distintas. La propiedad de tipo principal se basa en el contexto como entrada para determinar el tipo, pero la propiedad de tipificación principal genera el contexto como resultado. [1]