¿Hay alguna razón para tener un tipo de fondo en un lenguaje de programación?

Tomaré un ejemplo simple: C ++ vs Rust.

Aquí hay una función que se usa para lanzar una excepción en C ++ 11:

[[noreturn]] void ThrowException(char const* message,
                                 char const* file,
                                 int line,
                                 char const* function);

Y aquí está el equivalente en Rust:

fn formatted_panic(message: &str, file: &str, line: isize, function: &str) -> !;

En un asunto puramente sintáctico, el constructo de Rust es más sensible. Tenga en cuenta que la construcción de C ++ especifica un tipo de retorno , aunque también especifica que no va a regresar. Eso es un poco raro.

En una nota estándar, la sintaxis de C ++ solo aparecía con C ++ 11 (se colocaba en la parte superior), pero varios compiladores habían proporcionado varias extensiones durante un tiempo, por lo que las herramientas de análisis de terceros debían programarse para reconocerlas. Las diversas formas en que este atributo podría ser escrito. Tenerlo estandarizado es claramente superior.

Ahora, en cuanto al beneficio?

El hecho de que una función no regrese puede ser útil para:

• optimización: se puede eliminar cualquier código después de él (no volverá), no es necesario guardar los registros (ya que no será necesario restaurarlos), ...
• análisis estático: elimina varias vías de ejecución potenciales
• mantenibilidad: (ver análisis estático, pero por humanos)

La respuesta de Karl es buena. Aquí hay un uso adicional que no creo que nadie más haya mencionado. El tipo de

if E then A else B

debe ser un tipo que incluya todos los valores en el tipo de A y todos los valores en el tipo de B . Si el tipo de B es Nothing , entonces el tipo de expresión if puede ser el tipo de A . A menudo declararé una rutina

def unreachable( s:String ) : Nothing = throw new AssertionError("Unreachable "+s) 

para decir que no se espera que se alcance el código. Como su tipo es Nothing , unreachable(s) ahora se puede usar en cualquier if o (más a menudo) switch sin afectar el tipo de resultado. Por ejemplo

 val colour : Colour := switch state of
         BLACK_TO_MOVE: BLACK
         WHITE_TO_MOVE: WHITE
         default: unreachable("Bad state")

Scala tiene ese tipo de Nada.

Otro caso de uso para Nothing (como se menciona en la respuesta de Karl) es la Lista [Nothing] es el tipo de listas de cada miembro cuyos miembros tienen el tipo Nothing. Por lo tanto, puede ser el tipo de la lista vacía.

La propiedad clave de Nothing que hace que estos casos de uso funcionen es no que no tiene valores (aunque en Scala, por ejemplo; no tiene valores), es que es un subtipo de cualquier otro tipo.

Supongamos que tiene un idioma donde cada tipo contiene el mismo valor, llamémoslo () . En tal idioma, el tipo de unidad, que tiene () como su único valor, podría ser un subtipo de cada tipo. Eso no lo convierte en un tipo de fondo en el sentido que significaba el OP; El OP estaba claro que un tipo de fondo no contiene valores. Sin embargo, como es un tipo que es un subtipo de cada tipo, puede desempeñar la misma función que el tipo de fondo.

Haskell hace las cosas de manera un poco diferente. En Haskell, una expresión que nunca produce un valor puede tener el tipo forall a.a . Una instancia de este esquema de tipo se unirá con cualquier otro tipo, por lo que actúa efectivamente como un tipo de fondo, aunque Haskell (estándar) no tiene noción de subtipo. Por ejemplo, la función error del preludio estándar tiene un esquema de tipo forall a. [Char] -> a . Así que puedes escribir

if E then A else error ""

y el tipo de expresión será el mismo que el tipo de A , para cualquier expresión A .

La lista vacía en Haskell tiene el esquema de tipo forall a. [a] . Si A es una expresión cuyo tipo es un tipo de lista, entonces

if E then A else []

es una expresión con el mismo tipo que A . El tipo de [] es el mismo que el tipo [error ""] , que muestra que la lista vacía no es el único valor de su tipo.

  

Tal vez se repita para siempre, o tal vez lanza una excepción.

Suena como un tipo útil para tener en esas situaciones, por raro que sea.

Además, aunque Nothing (nombre de Scala para el tipo inferior) no puede tener valores, List[Nothing] no tiene esa restricción, lo que lo hace útil como el tipo de una lista vacía. La mayoría de los idiomas solucionan esto al hacer que una lista vacía de cadenas sea de un tipo diferente al de una lista vacía de enteros, lo que tiene sentido, pero hace que una lista vacía sea más detallada para escribir, lo cual es un gran inconveniente en un lenguaje orientado a listas.

Los tipos forman un monoide de dos maneras, haciendo juntos un semiring . Eso es lo que se llama tipos de datos algebraicos . Para los tipos finitos, este semired se relaciona directamente con el semiring de los números naturales (incluido el cero), lo que significa que cuenta cuántos valores posibles tiene el tipo (excluyendo los "valores no terminantes").

• El tipo inferior (lo llamaré Vacuous ) tiene valores cero ^† .
• El tipo de unidad tiene un valor. Llamaré tanto al tipo como a su único valor () .
• La composición (que la mayoría de los lenguajes de programación admiten de manera bastante directa, a través de registros / estructuras / clases con campos públicos) es una operación de producto . Por ejemplo, (Bool, Bool) tiene cuatro valores posibles, a saber, (False,False) , (False,True) , (True,False) y (True,True) .
  El tipo de unidad es el elemento de identidad de la operación de composición. P.ej. ((), False) y ((), True) son los únicos valores del tipo ((), Bool) , por lo que este tipo es isomorfo a Bool en sí mismo.
• Los tipos alternativos se descuidan un poco en la mayoría de los idiomas (los lenguajes OO los admiten con herencia), pero no son menos útiles. Una alternativa entre dos tipos A y B básicamente tiene todos los valores de A , más todos los valores de B , por lo tanto, sum type . Por ejemplo, Either () Bool tiene tres valores, los llamaré Left () , Right False y Right True .
  El tipo de abajo es el elemento de identidad de la suma: Either Vacuous A tiene solo valores de la forma Right a , porque Left ... no tiene sentido ( Vacuous no tiene valores).

Lo interesante de estos monoides es que, cuando introduces funciones en tu idioma, categoría de estos tipos con las funciones como morfismos es una categoría monoidal . Entre otras cosas, esto le permite definir funtores aplicativos y mónadas , que resultan ser una excelente abstracción para cálculos generales (posiblemente con efectos secundarios, etc.) dentro de términos puramente funcionales.

Ahora, en realidad puedes llegar bastante lejos preocupándote solo por un lado del problema (la composición monoide), entonces realmente no necesitas el tipo de fondo explícitamente. Por ejemplo, incluso Haskell durante mucho tiempo no tuvo un tipo de fondo estándar. Ahora que lo tiene, se llama Void .

Pero si considera la imagen completa, como una categoría cerrada bicartesiana , el sistema de tipos es en realidad es equivalente a todo el cálculo lambda, así que básicamente tienes la abstracción perfecta sobre todo lo posible en un lenguaje completo de Turing. Excelente para lenguajes integrados de dominio específicos, por ejemplo, hay un proyecto sobre la codificación directa de circuitos electrónicos de esta manera .

Por supuesto, bien puede decir que esto es todo el tontería general de los teóricos. No necesitas conocer la teoría de categorías para ser un buen programador, pero cuando lo haces, te ofrece formas poderosas y ridículamente generales de razonar sobre el código y evitar invariantes.

^† _{mb21 me recuerda que tenga en cuenta que esto no debe confundirse con valores inferiores . En lenguajes perezosos como Haskell, cada tipo contiene un “valor” inferior, denotado ⊥ . Esto no es una cosa concreta que pueda pasar de forma explícita, sino que es lo que se "devuelve", por ejemplo, cuando una función se repite para siempre. Incluso el tipo Void de Haskell "contiene" el valor inferior, por lo tanto el nombre. En ese sentido, el tipo inferior de Haskell realmente tiene un valor y su tipo de unidad tiene dos valores, pero en la discusión de la teoría de categorías esto generalmente se ignora.}

Es útil para el análisis estático documentar el hecho de que una ruta de código en particular no es accesible. Por ejemplo, si escribe lo siguiente en C #:

int F(int arg) {
 if (arg != 0)
  return arg + 1; //some computation
 else
  Assert(false); //this throws but the compiler does not know that
}
void Assert(bool cond) { if (!cond) throw ...; }

El compilador se quejará de que F no devuelve nada en al menos una ruta de código. Si Assert fuera marcado como no devuelto, el compilador no tendría que avisar.

En algunos idiomas, null tiene el tipo de fondo, ya que el subtipo de todos los tipos define muy bien para qué se usan los idiomas (a pesar de la leve contradicción de tener null en sí mismo y una función que se devuelve a sí misma, evitando la argumentos comunes sobre por qué bot debería estar deshabitado).

También se puede usar como catch-all en los tipos de función ( any -> bot ) para manejar el envío que salió mal.

Y algunos idiomas le permiten resolver bot como un error, que puede usarse para proporcionar errores de compilación personalizados.

Sí, este es un tipo bastante útil; Si bien su función sería mayoritariamente interna al sistema de tipos, hay ocasiones en que el tipo de fondo aparecerá abiertamente.

Considere un lenguaje de tipo estático en el que los condicionales son expresiones (de modo que la construcción if-then-else se duplica como el operador ternario de C y amigos, y podría haber una declaración de caso de múltiples vías similar). El lenguaje de programación funcional tiene esto, pero también ocurre en ciertos lenguajes imperativos (desde ALGOL 60). Entonces, todas las expresiones de rama deben producir finalmente el tipo de la expresión condicional completa. Uno podría simplemente requerir que sus tipos sean iguales (y creo que este es el caso del operador ternario en C), pero esto es demasiado restrictivo, especialmente cuando el condicional también se puede usar como una declaración condicional (sin devolver ningún valor útil). En general, se quiere que cada expresión de rama sea (implícitamente) convertible a un tipo común que será el tipo de la expresión completa (posiblemente con restricciones más o menos complicadas para permitir que ese tipo común se encuentre efectivamente por el complaciente, vea C ++, pero no voy a entrar en esos detalles aquí).

Hay dos tipos de situaciones en las que un tipo general de conversión permitirá la flexibilidad necesaria de tales expresiones condicionales. Ya se mencionó uno, donde el tipo de resultado es el tipo de unidad void ; este es naturalmente un supertipo de todos los demás tipos, y permitir que cualquier tipo se convierta (trivialmente) a él hace posible usar la expresión condicional como una declaración condicional. El otro involucra casos donde la expresión devuelve un valor útil, pero una o más ramas son incapaces de producir uno. Por lo general, plantean una excepción o implican un salto, y exigirles que (también) produzcan un valor del tipo de la expresión completa (desde un punto inalcanzable) sería inútil. Es este tipo de situación que puede manejarse con gracia dando cláusulas de aumento de excepción, saltos y llamadas que tendrán tal efecto, el tipo de fondo, el tipo que se puede convertir (trivialmente) en cualquier otro tipo.

Yo sugeriría escribir un tipo inferior como * para sugerir su convertibilidad a tipo arbitrario. Puede servir a otros fines útiles internamente, por ejemplo, cuando se intenta deducir un tipo de resultado para una función recursiva que no declara ninguna, el inferente de tipo podría asignar el tipo * a cualquier llamada recursiva para evitar una situación de gallina y huevo. ; el tipo real estará determinado por ramas no recursivas, y las recursivas se convertirán al tipo común de las no recursivas. Si hay no ramas no recursivas, el tipo seguirá siendo * , e indicará correctamente que la función no tiene forma posible de regresar de la recursión. Aparte de esto y como tipo de resultado de las funciones de lanzamiento de excepciones, se puede usar * como tipo de componente de secuencias de longitud 0, por ejemplo, de la lista vacía; de nuevo, si alguna vez se selecciona un elemento de una expresión de tipo [*] (necesariamente lista vacía), entonces el tipo resultante * indicará correctamente que esto nunca se puede devolver sin un error.