Tipo funcional

Tipo funcional ( tipo de flecha , exponencial ) en informática  : el tipo de una variable o parámetro , cuyo valor o cuál puede ser una función ; o el tipo del argumento o valor devuelto de una función de orden superior que acepta o devuelve una función.

El tipo de función depende de los tipos de parámetros y del tipo de resultado de la función. En otras palabras, es un tipo del tipo más alto o, más precisamente, un constructor de tipo no aplicado " ". En modelos teóricos y lenguajes que soportan currying , como el cálculo lambda de tipo simple , el tipo de función depende exactamente de dos tipos: dominio y dominio de valor . En este caso, el tipo de función, siguiendo la tradición matemática, suele escribirse como (en los lenguajes de programación prácticos - ), o como , lo que implica que existen exactamente funciones de teoría de conjuntos que corresponden a . En términos de la correspondencia de Curry-Howard, la habitabilidad de un tipo funcional es equivalente a la demostrabilidad de una implicación lógica . A -> B

Un tipo de función se puede considerar como un caso especial de un producto dependiente de tipos . Entre otras propiedades, tal representación conlleva la idea de una función polimórfica .

Lenguajes de programación

La siguiente tabla resume la sintaxis utilizada en varios lenguajes de programación para los tipos de funciones, así como los ejemplos de firmas de tipos correspondientes para la función de composición de funciones .

Lenguaje de programación Notación Tipo Firma Ejemplo
Con soporte para características de primera clase ,
polimorfismo paramétrico 		C++11 std::function<ρ (α1,α2,...,αn)> function<function<int(int)>(function<int(int)>, function<int(int)>)> compose;
C# Func<α1,α2,...,αn,ρ> Func<A,C> compose(Func<A,B> f, Func<B,C> g);
Vamos func(α1,α2,...,αn) ρ var compose func(func(int)int, func(int)int) func(int)int
Haskell α -> ρ compose :: (a -> b) -> (b -> c) -> a -> c
Objective-C /C/C++ con bloques ρ (^)(α1,α2,...,αn) int (^compose(int (^f)(int), int (^g)(int)))(int);
OCaml α -> ρ compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
Scala (α1,α2,...,αn) => ρ def compose[A, B, C](f: B => C, g: A => B): A => C
ML estándar α -> ρ compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
Sin características de primera clase ,
polimorfismo paramétrico 		xi ρ (*)(α1,α2,...,αn) int (*compose(int (*f)(int), int (*g)(int)))(int);

Tenga en cuenta que en el ejemplo de C# , la función composees de tipo " Func< Func<A,B>, Func<B,C>, Func<A,C> >".

Semántica denotacional

El tipo funcional en los lenguajes de programación no corresponde al espacio de todas las funciones de teoría de conjuntos. Si tomamos el tipo infinito contable de números naturales como el dominio de definición y el tipo de números booleanos como el dominio de valores, entonces hay un número incontable (  es el poder del continuo ) funciones teóricas de conjuntos entre ellos. Obviamente, este conjunto de funciones es ciertamente más amplio que el conjunto de funciones definido en los lenguajes de programación, ya que solo hay un conjunto contable de programas (donde el programa es una cadena finita de caracteres de un conjunto finito).

La semántica denotacional está buscando modelos más apropiados (llamados regiones ), incluso para modelar conceptos de lenguaje de programación como el tipo de función. En semántica denotacional, se cree que es conveniente no limitarse solo a las funciones computables , sino usar cualquier función continua de Scott en conjuntos parcialmente ordenados , que también pueden modelar cálculos no finales (y los que surgen en cualquier Turing - lenguaje completo). Los medios de la teoría de áreas utilizados en la semántica denotacional son bastante expresivos, por ejemplo, la función continua de Scott está modelada por " parallel or" , que no está definida en todos los lenguajes de programación.

Véase también

Enlaces

 Tipos de datos
Ininterpretable
Numérico
Texto
Referencia
Compuesto
resumen
Otro
Temas relacionados