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

49

Un tipo de fondo es una construcción que aparece principalmente en la teoría de tipos matemáticos. También se llama el tipo vacío. Es un tipo que no tiene valores, pero es un subtipo de todos los tipos.

Si el tipo de retorno de una función es el tipo inferior, eso significa que no regresa. Período. Tal vez se repita para siempre, o tal vez arroje una excepción.

¿Cuál es el punto de tener este tipo extraño en un lenguaje de programación? No es tan común, pero está presente en algunos, como Scala y Lisp.

GregRos
fuente
2
@SargeBorsch: ¿estás seguro de eso? Por supuesto, uno no puede en C definir explícitamente un voiddato ...
Basile Starynkevitch
3
@BasileStarynkevitch no hay valores de tipo void, y el tipo de unidad debe tener un valor. Además, como señaló, ni siquiera puede declarar un valor de tipo void, eso significa que ni siquiera es un tipo, solo un caso de esquina especial en el idioma.
Sarge Borsch
2
Sí, la C es extraña en esto, especialmente en cómo se escriben los tipos de puntero y puntero de función. Pero voiden Java es casi lo mismo: no es realmente un tipo y no puede tener valores.
Sarge Borsch
3
En la semántica de los idiomas con un tipo de fondo, no se considera que el tipo de fondo no tenga valores, sino que tiene un valor, el valor de fondo, que representa un cálculo que nunca se completa (normalmente). Dado que el valor inferior es un valor de cada tipo, el tipo inferior puede ser un subtipo de cada tipo.
Theodore Norvell
44
@BasileStarynkevitch Common Lisp tiene el tipo nulo que no tiene valores. También tiene el tipo nulo que tiene un solo valor, el símbolo nil(también conocido como ()), que es un tipo de unidad.
Joshua Taylor

Respuestas:

33

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

Aquí hay una función utilizada 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, la construcción Rust es más sensata. Tenga en cuenta que la construcción C ++ especifica un tipo de retorno , aunque también especifica que no va a volver. Eso es un poco raro.

En una nota estándar, la sintaxis de C ++ solo apareció con C ++ 11 (se agregó en la parte superior), pero varios compiladores habían estado proporcionando varias extensiones durante un tiempo, por lo que las herramientas de análisis de terceros tuvieron que programarse para reconocer las diversas formas Este atributo podría ser escrito. Tenerlo estandarizado es obviamente claramente superior.


Ahora, en cuanto al beneficio?

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

  • optimización: se puede podar cualquier código después (no volverá), no es necesario guardar los registros (ya que no será necesario restaurarlos), ...
  • análisis estático: elimina una serie de posibles rutas de ejecución
  • mantenibilidad: (ver análisis estático, pero por humanos)
Matthieu M.
fuente
66
voiden su ejemplo de C ++ define (parte de) el tipo de función, no el tipo de retorno. Restringe el valor al que se permite la función return; cualquier cosa que se pueda convertir a vacío (que no es nada). Si la función returns no debe ir seguida de un valor. El tipo completo de la función es void () (char const*, char const*, int, char const *). + 1 para usar en char constlugar de const char:-)
Más claro
44
Sin embargo, eso no significa que tenga más sentido tener un tipo de fondo, solo que tiene sentido anotar funciones sobre si regresan o no como parte del lenguaje. En realidad, dado que las funciones pueden no regresar debido a diferentes razones, parece mejor codificar la razón de alguna manera en lugar de usar un término general, como el concepto relativamente reciente de anotar funciones en función de sus efectos secundarios.
GregRos
2
En realidad, hay una razón para hacer que "no regrese" y que "tenga tipo X de retorno" independiente: compatibilidad con versiones anteriores para su propio código, ya que la convención de llamada puede depender del tipo de retorno.
Deduplicador
es parte [[noreturn]] de la sintaxis o una adición de funcionalidad?
Zaibis
1
[cont.] En general, solo diría que una discusión sobre las ventajas de ⊥ tiene que definir qué califica como una implementación de ⊥; y no creo que un sistema de tipos que no tenga ( a → ⊥) ≤ ( ab ) sea una implementación útil de ⊥. Entonces, en este sentido, el SysV x86-64 C ABI (entre otros) simplemente no permite implementar ⊥.
Alex Shpilkin
26

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 Ay todos los valores en el tipo de B. Si el tipo de Bes Nothing, entonces el tipo de la ifexpresión puede ser el tipo de A. A menudo declaro una rutina

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

decir que no se espera alcanzar el código. Dado que su tipo es Nothing, unreachable(s)ahora se puede usar en cualquiera ifo (más a menudo) switchsin 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 Lista [Nada] es el tipo de listas de cada uno de cuyos miembros tiene el tipo Nada. Por lo tanto, puede ser el tipo de la lista vacía.

La propiedad clave de Nothingesto hace que estos casos de uso funcionen no es que no tenga 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 dicho lenguaje, el tipo de unidad, que tiene ()como único valor, podría ser un subtipo de cada tipo. Eso no lo convierte en un tipo inferior en el sentido que significaba el OP; el OP dejó 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 el mismo papel que un tipo inferior.

Haskell hace las cosas un poco diferente. En Haskell, una expresión que nunca produce un valor puede tener el esquema de tipo forall a.a. Una instancia de este esquema de tipo se unificará con cualquier otro tipo, por lo que efectivamente actúa como un tipo de fondo, aunque Haskell (estándar) no tiene noción de subtipo. Por ejemplo, la errorfunción del preludio estándar tiene un esquema de tipo forall a. [Char] -> a. Entonces 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 Aes 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.

Theodore Norvell
fuente
¿Cuál es la diferencia entre el tipo forall a . [a]y el tipo [a]en Haskell? ¿Las variables de tipo no están cuantificadas universalmente en las expresiones de tipo Haskell?
Giorgio
@Giorgio En Haskell, la cuantificación universal está implícita si está claro que está buscando un esquema de tipo. Ni siquiera puede escribir forallen el estándar Haskell 2010. Escribí la cuantificación explícitamente porque este no es un foro de Haskell y algunas personas podrían no estar familiarizadas con las convenciones de Haskell. Por lo tanto, no hay diferencia, excepto que forall a . [a]no es estándar, mientras que lo [a]es.
Theodore Norvell
19

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

  • El tipo inferior (lo llamaré Vacuous) tiene valores cero .
  • El tipo de unidad tiene un valor. Llamaré tanto al tipo como a su valor único ().
  • La composición (que la mayoría de los lenguajes de programación admite de forma bastante directa, a través de registros / estructuras / clases con campos públicos) es una operación del 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. Por ejemplo, ((), False)y ((), True)son los únicos valores de tipo ((), Bool), por lo que este tipo es isomorfo a Boolsí mismo.
  • Los tipos alternativos son algo descuidados en la mayoría de los idiomas (los idiomas OO los apoyan con herencia), pero no son menos útiles. Una alternativa entre dos tipos Ay Bbásicamente tiene todos los valores de A, además de todos los valores de B, por lo tanto, el tipo de suma . Por ejemplo, Either () Booltiene tres valores, voy a llamarlos Left (), Right Falsey Right True.
    El tipo inferior es el elemento de identidad de la suma: soloEither Vacuous A tiene valores de la forma , porque no tiene sentido ( no tiene valores).Right aLeft ...Vacuous

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

Ahora, en realidad puede llegar bastante lejos si se preocupa solo por un lado del problema (el monoide de composición), entonces realmente no necesita el tipo de fondo explícitamente. Por ejemplo, incluso Haskell no tuvo durante mucho tiempo un tipo de fondo estándar. Ahora sí, se llama Void.

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

Por supuesto, bien puedes decir que esto es una tontería general de todos los teóricos . No es necesario que conozca la teoría de categorías para ser un buen programador, pero cuando lo hace, le brinda formas poderosas y ridículamente generales de razonar sobre el código y probar invariantes.


mb21 me recuerda que tenga en cuenta que esto no debe confundirse con los valores inferiores . En lenguajes perezosos como Haskell, cada tipo contiene un "valor" inferior, denotado . Esto no es algo concreto que puedas pasar explícitamente, sino que es lo que se "devuelve", por ejemplo, cuando una función se repite para siempre. Incluso el Voidtipo de Haskell "contiene" el valor inferior, de ahí el nombre. Desde ese punto de vista, el tipo de fondo de Haskell realmente tiene un valor y su tipo de unidad tiene dos valores, pero en la discusión de teoría de categorías esto generalmente se ignora.

a la izquierda
fuente
"El tipo inferior (lo llamaré Void)", que no debe confundirse con el valor bottom , que es miembro de cualquier tipo en Haskell .
mb21
18

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

Suena como un tipo útil para tener en esas situaciones, aunque sean raros.

Además, aunque Nothing(el 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 resuelven esto haciendo una lista vacía de cadenas de un tipo diferente que 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.

Karl Bielefeldt
fuente
12
“La lista vacía de Haskell es un constructor de tipos”: seguramente lo relevante aquí es más que polimórfica o sobrecargada , es decir, las listas vacías de diferentes tipos son valores distintos, pero los []representa a todos y se instan El tipo específico según sea necesario.
Peter LeFanu Lumsdaine
Es interesante: Si intenta crear una matriz vacía en el intérprete Haskell, se obtiene un valor muy definido con un tipo muy indefinida: [a]. Del mismo modo, los :t Left 1rendimientos Num a => Either a b. En realidad, evaluar la expresión fuerza el tipo de a, pero no de b:Either Integer b
John Dvorak
55
La lista vacía es un constructor de valores . Un poco confuso, el constructor de tipos involucrado tiene el mismo nombre pero la lista vacía en sí misma es un valor, no un tipo (bueno, también hay listas de nivel de tipo, pero ese es un tema completamente diferente). La parte que hace que la lista vacía funcione para cualquier tipo de lista es la implícita forallen su tipo forall a. [a],. Hay algunas maneras agradables de pensar forall, pero lleva un tiempo darse cuenta realmente.
David
@PeterLeFanuLumsdaine Eso es exactamente lo que significa ser un constructor de tipos. Simplemente significa que es un tipo con un tipo diferente de *.
GregRos
2
En Haskell []es un constructor de tipos y []es una expresión que representa una lista vacía. Pero eso no significa que "la lista vacía de Haskell sea un constructor de tipos". El contexto deja en claro si []se está utilizando como tipo o como expresión. Supongamos que declaras data Foo x = Foo | Bar x (Foo x); ahora puede usarlo Foocomo un constructor de tipos o como un valor, pero es casualidad que haya elegido el mismo nombre para ambos.
Theodore Norvell
3

Es útil para el análisis estático documentar el hecho de que una ruta de código 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 Fno devuelve nada en al menos una ruta de código. Si Assertse marcara como no devuelto, el compilador no necesitaría avisar.

usr
fuente
2

En algunos idiomas, nulltiene el tipo inferior, ya que el subtipo de todos los tipos define muy bien para qué lenguajes usan nulo (a pesar de la leve contradicción de nullser ambos mismos y una función que se devuelve, evitando los argumentos comunes sobre por qué botdebería estar deshabitada).

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

Y algunos idiomas le permiten resolverlo realmente botcomo un error, que puede usarse para proporcionar errores de compilación personalizados.

Telastyn
fuente
11
No, un tipo de fondo no es el tipo de unidad. Un tipo de fondo no tiene ningún valor, por lo que una función que devuelve un tipo de fondo no debería devolver (es decir, lanzar una excepción o bucle indefinidamente)
Basile Starynkevitch
@BasileStarynkevitch: no estoy hablando del tipo de unidad. El tipo de unidad se asigna a voididiomas comunes (aunque con semánticas ligeramente diferentes para el mismo uso), no null. Aunque también tiene razón en que la mayoría de los idiomas no modelan nulo como el tipo inferior.
Telastyn
3
@TheodoreNorvell: las primeras versiones de Tangent hicieron eso, aunque yo soy su autor, así que quizás sea una trampa. No tengo los enlaces guardados para otros, y ha pasado un tiempo desde que hice esa investigación.
Telastyn
1
@Martijn Pero puede usar null, por ejemplo, comparar un puntero para nullobtener un resultado booleano. Creo que las respuestas muestran que hay dos tipos distintos de tipos inferiores. (a) Idiomas (p. ej., Scala) donde el tipo que es un subtipo de cada tipo representa cálculos que no ofrecen ningún resultado. Esencialmente es un tipo vacío, aunque técnicamente a menudo está poblado por un valor inferior inútil que representa la no determinación. (b) Idiomas como Tangente, en el que el tipo inferior es un subconjunto de cualquier otro tipo porque contiene un valor útil que también se encuentra en cualquier otro tipo: nulo.
Theodore Norvell
44
Es interesante que algunos idiomas tengan un valor con un tipo que no pueda declarar (común para el literal nulo), y otros tengan un tipo que pueda declarar pero que no tenga valores (un tipo inferior tradicional), y que cumplan roles algo comparables .
Martijn
1

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

Considere un lenguaje de tipo estático en el que los condicionales son expresiones (por lo que la construcción if-then-else se duplica como el operador ternario de C y amigos, y puede 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 enunciado 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 el compilador encuentre efectivamente ese tipo común, cf. C ++, pero no 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 unidadvoid; Esto es naturalmente un supertipo de todos los otros tipos, y permitir que cualquier tipo se convierta (trivialmente) en él hace posible usar la expresión condicional como declaración condicional. El otro involucra casos en los que la expresión devuelve un valor útil, pero una o más ramas son incapaces de producir uno. Por lo general, plantearán una excepción o implicarán un salto, y requerirles que (también) produzcan un valor del tipo de la expresión completa (desde un punto inalcanzable) no tendría sentido. Es este tipo de situación la que se puede manejar con gracia al dar cláusulas, saltos y llamadas de aumento de excepciones que tendrán ese efecto, el tipo inferior, el único tipo que puede convertirse (trivialmente) en cualquier otro tipo.

Sugeriría escribir un tipo inferior *para sugerir su convertibilidad a tipo arbitrario. Puede tener otros propósitos útiles internamente, por ejemplo, cuando se intenta deducir un tipo de resultado para una función recursiva que no declara ninguno, el inferenciador 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 no hay ramas no recursivas, el tipo permanecerá *e indicará correctamente que la función no tiene forma alguna de regresar de la recursividad. Aparte de esto y como 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; nuevamente, si alguna vez se selecciona un elemento de una expresión de tipo [*](lista necesariamente vacía), el tipo resultante *indicará correctamente que esto nunca puede regresar sin un error.

Marc van Leeuwen
fuente
Entonces, ¿es la idea que var foo = someCondition() ? functionReturningBar() : functionThatAlwaysThrows()podría inferir el tipo de fooas Bar, ya que la expresión nunca podría producir nada más?
supercat
1
Acaba de describir el tipo de unidad, al menos en la primera parte de su respuesta. Una función que devuelve el tipo de unidad es la misma que se declara que regresa voiden C. La segunda parte de su respuesta, donde habla de un tipo para una función que nunca regresa, o una lista sin elementos, eso es realmente el tipo de fondo! (A menudo se escribe como en _|_lugar de *. No estoy seguro de por qué. Quizás porque parece un fondo (humano) :)
andrewf
2
Para evitar dudas: 'no devuelve nada útil' es diferente de 'no regresa'; el primero está representado por el tipo de Unidad; el segundo por el tipo de fondo.
andrewf
@andrewf: Sí, entiendo la distinción. Mi respuesta es un poco larga, pero el punto que quería señalar es que el tipo de unidad y el tipo de fondo juegan (diferentes pero) roles comparables para permitir que ciertas expresiones se usen de manera más flexible (pero aún así segura).
Marc van Leeuwen
@supercat: Sí, esa es la idea. Actualmente en C ++ que es ilegal, aunque sería válida si functionThatAlwaysThrows()fueron reemplazados por una explícita throw, debido al lenguaje especial en la Norma. Tener un tipo que haga esto sería una mejora.
Marc van Leeuwen
0

En algunos idiomas, puede anotar una función para decirle tanto al compilador como a los desarrolladores que una llamada a esta función no se devolverá (y si la función está escrita de una manera que pueda regresar, el compilador no lo permitirá ) Es algo útil de saber, pero al final puede llamar a una función como esta como cualquier otra. El compilador puede usar la información para la optimización, para dar advertencias sobre el código muerto, etc. Por lo tanto, no hay una razón muy convincente para tener este tipo, pero tampoco hay una razón muy convincente para evitarlo.

En muchos idiomas, una función puede devolver "void". Lo que eso significa exactamente depende del idioma. En C significa que la función no devuelve nada. En Swift, significa que la función devuelve un objeto con un solo valor posible, y dado que solo hay un valor posible, ese valor toma cero bits y en realidad no requiere ningún código. En cualquier caso, eso no es lo mismo que "fondo".

"bottom" sería un tipo sin valores posibles. Nunca puede existir. Si una función devuelve "bottom", en realidad no puede regresar, porque no hay ningún valor de tipo "bottom" que pueda devolver.

Si un diseñador de idiomas lo desea, entonces no hay razón para no tener ese tipo. La implementación no es difícil (puede implementarla exactamente como una función que devuelve nula y marcada como "no regresa"). No puede mezclar punteros a funciones que regresan al fondo con punteros a funciones que devuelven vacío, porque no son del mismo tipo).

gnasher729
fuente