En la teoría de tipos , una teoría dentro de la lógica matemática , el tipo base 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 tachuela hacia arriba (⊥).
Cuando el tipo bottom está deshabitado , una función cuyo tipo de retorno es bottom no puede devolver ningún valor, ni siquiera el valor único de un tipo de unidad . En un lenguaje de este tipo, el tipo bottom puede, por lo tanto, conocerse como el tipo cero , nunca o vacío que, en la correspondencia de Curry–Howard , corresponde a la falsedad.
Sin embargo, cuando el tipo inferior está habitado, entonces es diferente del tipo vacío.
En los sistemas de subtipificación, 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 un sistema de tipos es sólido , el tipo inferior está deshabitado y un término de tipo inferior representa una contradicción lógica. En tales sistemas, normalmente no se hace distinción entre el tipo inferior y el tipo vacío , y los términos pueden usarse indistintamente.
Si el tipo inferior está habitado, sus términos normalmente corresponden a condiciones de error, como comportamiento indefinido, recursión infinita o errores irrecuperables.
En Cuantificación limitada con Bottom , [1] Pierce dice que "Bot" tiene muchos usos:
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.La mayoría de los lenguajes más utilizados no tienen una forma de indicar el tipo de base. Hay algunas excepciones notables.
En Haskell , el tipo inferior se llama Void. [3]
En Common Lisp , el tipo NIL, no contiene valores y es un subtipo de cada tipo. [4] El tipo nombrado NILa veces se confunde con el tipo nombrado NULL, que tiene un valor, es decir, 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 retornan normalmente, también se usa 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. Por lo tanto , , 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 funciones que se garantiza que nunca volverán, por ejemplo, al llamarlas panic!()o realizar un bucle indefinidamente. También es el tipo de ciertas palabras clave de flujo de control, como breakand return, que no producen un valor pero que, no obstante, se pueden usar como expresiones. [5]
En Ceilán , el tipo inferior es Nothing. [6] 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{}. [7]
En TypeScript , el tipo inferior es never. [8] [9]
En JavaScript con anotaciones del compilador de cierre , el tipo inferior es !Null(literalmente, un miembro no nulo del Null tipo 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), [10] mientras que typing.NoReturn(introducido en la versión 3.5) se puede utilizar como el tipo de retorno de funciones que no retornan específicamente (y se duplicó como el tipo inferior general antes de la introducción de Never). [11]
En Kotlin , el tipo inferior es Nothing. [12]
En D , el tipo inferior es noreturn. [13]
En Dart , desde la versión 2.12 con la actualización de seguridad de nulidad de sonido, el Nevertipo se introdujo como el tipo inferior. Antes de eso, el tipo inferior solía ser Null. [14] [15]