En informática y lógica matemática , un tipo de función (o tipo flecha o exponencial ) es el tipo de variable o parámetro al que una función tiene o puede asignarse, o un argumento o tipo de resultado de una función de orden superior que toma o regresa Una función.
El tipo de función depende del tipo de parámetros y del tipo de resultado de la función (o, más exactamente, el constructor de tipos · → · no aplicado , es un tipo de tipo superior ). En entornos teóricos y lenguajes de programación donde las funciones se definen en forma curry , como el cálculo lambda simplemente escrito , un tipo de función depende exactamente de dos tipos, el dominio A y el rango B. Aquí un tipo de función a menudo se denota A → B , siguiendo una convención matemática, o B A , basándose en que existen exactamente B A (exponencialmente muchas) funciones teóricas de conjuntos asignaciones A a B en la categoría de conjuntos . La clase de tales aplicaciones o funciones se llama objeto exponencial . El acto de curry hace que el tipo de función sea adjunto al tipo de producto ; Esto se explora en detalle en el artículo sobre el curry.
El tipo de función puede considerarse un caso especial del tipo de producto dependiente , que, entre otras propiedades, engloba la idea de función polimórfica .
Al observar la firma de tipo de ejemplo de, por ejemplo, C#, el tipo de función composees en realidad Func<Func<A,B>,Func<B,C>,Func<A,C>>.
Debido al borrado de tipos en C++ 11 std::function, es más común usar plantillas para parámetros de funciones de orden superior e inferencia de tipos ( auto) para cierres .
El tipo de función en los lenguajes de programación no corresponde al espacio de todas las funciones de teoría de conjuntos. Dado el tipo contablemente infinito de números naturales como dominio y los booleanos como rango, entonces hay un número incontablemente infinito (2 ℵ 0 = c ) de funciones de teoría de conjuntos entre ellos. Claramente, este espacio de funciones es mayor que el número de funciones que se pueden definir en cualquier lenguaje de programación, ya que sólo existen un número contable de programas (un programa es una secuencia finita de un número finito de símbolos) y una de las funciones de la teoría de conjuntos. Resuelve eficazmente el problema de la detención .
La semántica denotacional se ocupa de encontrar modelos más apropiados (llamados dominios ) para modelar conceptos de lenguajes de programación como los tipos de funciones. Resulta que restringir la expresión al conjunto de funciones computables tampoco es suficiente si el lenguaje de programación permite escribir cálculos no terminantes (que es el caso si el lenguaje de programación es Turing completo ). La expresión debe limitarse a las llamadas funciones continuas (que corresponden a la continuidad en la topología de Scott , no a la continuidad en el sentido analítico real). Incluso entonces, el conjunto de funciones continuas contiene la función paralela o , que no se puede definir correctamente en todos los lenguajes de programación.