En informática y lógica matemática , un tipo de función (o tipo de flecha o exponencial ) es el tipo de una variable o parámetro al que se le ha asignado o puede asignar una función , o un tipo de argumento o resultado de una función de orden superior que toma o devuelve una función.
Un tipo de función depende del tipo de los parámetros y del tipo de resultado de la función (este, o más precisamente el constructor de tipo · → · no aplicado , es un tipo de clase superior ). En entornos teóricos y lenguajes de programación donde las funciones se definen en forma currificada , como el cálculo lambda de tipos simples , 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 la convención matemática, o B A , según la existencia de exactamente B A (exponencialmente muchas) funciones de teoría de conjuntos que mapean A a B en la categoría de conjuntos . La clase de tales mapas o funciones se llama objeto exponencial . El acto de currificar hace que el tipo de función sea adjunto al tipo de producto ; esto se explora en detalle en el artículo sobre currificación.
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 la 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 utilizar 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 infinito numerable de los números naturales como dominio y los booleanos como rango, entonces hay un número infinito numerable (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 solo existen un número numerable de programas (siendo un programa una secuencia finita de un número finito de símbolos) y una de las funciones de teoría de conjuntos resuelve efectivamente el problema de detención .
La semántica denotacional se ocupa de encontrar modelos más apropiados (llamados dominios ) para modelar conceptos del lenguaje 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 restringirse 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 puede definirse correctamente en todos los lenguajes de programación.