Tipo inferior

En la teoría de tipos , una teoría dentro de la lógica matemática , el tipo inferior de un sistema de tipos es el tipo que es un subtipo de todos los demás tipos. ^{[ 1 ]}

Cuando existe dicho tipo, a menudo se representa con el símbolo de flecha hacia arriba (⊥).

Cuando el tipo inferior está vacío , una función cuyo tipo de retorno es inferior no puede devolver ningún valor, ni siquiera el único valor de un tipo unitario . En dicho lenguaje, el tipo inferior puede denominarse, por lo tanto, tipo cero , nunca o vacío, que, en la correspondencia de Curry-Howard , corresponde a la falsedad.

Sin embargo, cuando el tipo inferior está ocupado, entonces es diferente del tipo vacío.

Si un sistema de tipos es correcto , el tipo inferior está vacío y un término de tipo inferior representa una contradicción lógica. En tales sistemas, normalmente no se distingue entre el tipo inferior y el tipo vacío , y ambos términos pueden usarse indistintamente.

En los sistemas de subtipado, el tipo inferior es un subtipo de todos los tipos. ^{[ 1 ]} Es dual al tipo superior , que abarca todos los valores posibles en un sistema.

Si el tipo inferior está ocupado, sus términos suelen corresponder a condiciones de error como comportamiento indefinido, recursión infinita o errores irrecuperables.

En Cuantificación acotada con Bottom , ^{[ 1 ]} Pierce dice que "Bot" tiene muchos usos:

1. En un lenguaje con excepciones , un tipo natural para la construcción raise es raise  ∈  exception  ->  Bot , y de forma similar para otras estructuras de control. Intuitivamente, Bot aquí es el tipo de cálculos que no devuelven una respuesta.
2. El tipo Bot es útil para tipar los "nodos hoja" de estructuras de datos polimórficas. Por ejemplo, List(Bot) es un buen tipo para nil.
3. Bot es un tipo natural para el valor " puntero nulo " (un puntero que no apunta a ningún objeto) de lenguajes como Java: en Java , el tipo nulo es el subtipo universal de los tipos de referencia . nulles el único valor del tipo nulo; y se puede convertir a cualquier tipo de referencia. ^{[ 2 ]} Sin embargo, el tipo nulo no es un tipo inferior como se describió anteriormente, no es un subtipo de inty otros tipos primitivos.
4. Un sistema de tipos que incluya tanto Top como Bot parece ser un objetivo natural para la inferencia de tipos , permitiendo que las restricciones sobre un parámetro de tipo omitido se capturen mediante un par de límites: escribimos S<:X<:T para significar "el valor de X debe estar en algún punto entre S y T". En tal esquema, un parámetro completamente sin restricciones está limitado inferiormente por Bot y superiormente por Top.

La mayoría de los lenguajes de programación más utilizados no tienen una forma de indicar el tipo inferior. Existen algunas excepciones notables.

• En Haskell , el tipo inferior se llama Void. ^{[ 3 ]}
• En Common Lisp , el tipo NILno contiene valores y es un subtipo de cada tipo. ^{[ 4 ]} El tipo llamado NILa veces se confunde con el tipo llamado NULL, que tiene un solo valor, a saber, el símbolo NILmismo.
• En Scala , el tipo inferior se denota como Nothing. Además de su uso para funciones que simplemente lanzan excepciones o que no retornarán normalmente, también se utiliza para tipos parametrizados covariantes . Por ejemplo, List de Scala es un constructor de tipo covariante, por lo que es un subtipo de para todos los tipos A. Así que el de Scala , el objeto para marcar el final de una lista de cualquier tipo, pertenece al tipo .List[Nothing]List[A]NilList[Nothing]
• En Rust , el tipo inferior se denomina tipo never y se denota por !. Está presente en la firma de tipo de las funciones que garantizan que nunca retornarán, por ejemplo, al llamar a panic!()o iterar indefinidamente. También es el tipo de ciertas palabras clave de control de flujo, como breaky return, que no producen un valor pero que, sin embargo, se pueden usar como expresiones. ^{[ 5 ]}
• En C y C++ , no existe un tipo inferior, pero una función que no devuelve se anota con , en una función que sí devuelve . ^{[ 6 ]}[[noreturn]]void
• En Ceylon , el tipo inferior es Nothing. ^{[ 7 ]} Es comparable a Nothingen Scala y representa la intersección de todos los demás tipos, así como un conjunto vacío.
• En Julia , el tipo inferior es Union{}. ^{[ 8 ]}
• En TypeScript , el tipo inferior es never. ^{[ 9 ] [ 10 ]}
• En JavaScript con anotaciones de Closure Compiler , el tipo inferior es !Null(literalmente, un miembro no nulo del Nulltipo de unidad ).
• En PHP , el tipo inferior es never.
• En las anotaciones de tipo estático opcionales de Pythontyping.Never , el tipo inferior general es (introducido en la versión 3.11), ^{[ 11 ]} mientras que typing.NoReturn(introducido en la versión 3.5) se puede usar como tipo de retorno de funciones que no devuelven específicamente (y también se usó como tipo inferior general antes de la introducción de Never). ^{[ 12 ]}
• En Kotlin , el tipo inferior es Nothing. ^{[ 13 ]}
• En D , el tipo inferior es noreturn. ^{[ 14 ]}
• En Dart , desde la versión 2.12 con la actualización de seguridad de nulo de sonido , el Nevertipo se introdujo como el tipo inferior. Antes de eso, el tipo inferior solía ser Null. ^{[ 15 ] [ 16 ]}

• Contradicción
• Parada por fallo
• Yaya
• Tipo superior
• Valor indefinido
• Tipo de unidad
• Tipo vacío

• Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . MIT Press . ISBN 0-262-16209-1.