函数类型

在计算机科学和数理逻辑中，函数类型（或箭头类型或指数）是指一个函数已经或可以被分配到的变量或参数的类型，或者是一个高阶函数获取或返回函数的参数或结果类型。一个函数的类型取决于参数的类型和函数的结果类型（它，或者更准确地说，未应用的类型构造器--→--，是一个高阶类型）。在理论环境和编程语言中，函数是以咖喱形式定义的，比如简单类型的lambda微积分，一个函数类型正好取决于两种类型，即域A和范围B。在这里，一个函数类型通常按照数学惯例表示为A→B，或者BA，因为在集合类别中正好存在BA（指数级数量）集合理论函数映射A到B。这种映射或函数的类别被称为指数对象。咖喱的行为使得函数类型与乘积类型相邻；这将在关于咖喱的文章中详细探讨。函数类型可以被认为是从属产品类型的一个特例，在其他属性中，它包含了多态函数的概念。

在几种编程语言中用于函数类型的语法可以被总结出来，包括高阶函数组合函数的类型签名示例。当查看例如C#的示例类型签名时，函数compose的类型实际上是Func<Func<A,B>,Func<B,C>,Func<A,C>>。由于C++11的std::function中的类型擦除，对于高阶函数参数使用模板，对于闭包使用类型推理（auto）是比较常见的。

编程语言中的函数类型并不对应于所有集合论函数的空间。考虑到自然数作为域和布尔作为范围的可数无限类型，那么在它们之间存在着不可数的无限数量（2ℵ0=c）的集合论函数。显然，这个函数空间大于任何编程语言中可以定义的函数数量，因为只存在可数的程序（一个程序是由有限数量的符号组成的有限序列），其中一个集合论函数有效地解决了停止的问题。指称语义学关注的是寻找更合适的模型（称为域）来模拟编程语言的概念，如函数类型。事实证明，如果编程语言允许编写非终止的计算，那么将表达限制在可计算函数的集合上也是不够的(如果编程语言是图灵完备的，那就是这种情况)。表达必须限制在所谓的连续函数(对应于斯科特拓扑学中的连续性，而不是真实分析意义上的连续性)。即使如此，连续函数的集合也包含平行或函数，它不能在所有编程语言中被正确定义。