En la teoría de tipos , una teoría dentro de la lógica matemática , el tipo inferior es el tipo que no tiene valores. También se denomina tipo cero o vacío y, a veces, se indica con el símbolo de tachuela hacia arriba (⊥).
Una función cuyo tipo de retorno es inferior no puede devolver ningún valor, ni siquiera el tipo de unidad de tamaño cero . Por lo tanto, una función cuyo tipo de retorno es el tipo inferior no puede regresar. En la correspondencia Curry-Howard , el tipo inferior corresponde a la falsedad.
En los sistemas de subtipificación, el tipo inferior es el subtipo de todos los tipos. [1] (Sin embargo, lo contrario no es cierto: un subtipo de todos los tipos no es necesariamente el tipo inferior). Se usa para representar el tipo de retorno de una función que no devuelve un valor: por ejemplo, uno que se repite para siempre , señala una excepción o salidas.
Debido a que el tipo de fondo se usa para indicar la falta de un retorno normal, generalmente no tiene valores. Contrasta con el tipo superior , que abarca todos los valores posibles en un sistema, y un tipo de unidad , que tiene exactamente un valor.
Los lenguajes más utilizados no tienen una forma de denotar explícitamente el tipo vacío. Hay algunas excepciones notables.
Desde Haskell2010, Haskell admite tipos de datos vacíos. Por tanto, permite la definición data Empty(sin constructores). El tipo Emptyno está del todo vacío, ya que contiene programas que no terminan y la undefinedconstante. La undefinedconstante se usa a menudo cuando desea que algo tenga el tipo vacío, porque undefinedcoincide con cualquier tipo (por lo que es una especie de "subtipo" de todos los tipos), e intentar evaluar undefinedhará que el programa se anule, por lo tanto, nunca devuelve una respuesta .