Функциональный тип ( стрелочный тип , экспоненциал ) в информатике — тип переменной или параметра , значением которой или которого может быть функция ; либо тип аргумента или возвращаемого значения функции высшего порядка , принимающей или возвращающей функцию.

Функциональный тип зависит от типов параметров и типа результата функции. Другими словами, это тип высшего рода , или, более точно, неприменённый конструктор типов « ${\displaystyle \cdot \to \cdot }$ ». В теоретических моделях и языках с поддержкой каррирования , например в просто типизированном лямбда-исчислении , функциональный тип зависит ровно от двух типов: области определения ${\displaystyle A}$ и области значений ${\displaystyle B}$ . В этом случае функциональный тип, следуя математической традиции, обычно записывают как ${\displaystyle A\to B}$ (в практических языках программирования — A -> B ), или как ${\displaystyle B^{A}}$ , подразумевая, что существует ровно ${\displaystyle |B|^{|A|}}$ , отображающих ${\displaystyle A}$ на ${\displaystyle B}$ . С точки зрения соответствия Карри — Ховарда обитаемость функционального типа ${\displaystyle A\to B}$ эквивалентна доказуемости логической импликации ${\displaystyle A\Rightarrow B}$ .

Функциональный тип можно рассматривать как частный случай зависимого произведения типов . Среди прочих свойств, такое представление несёт в себе идею полиморфной функции .

Языки программирования

В следующую таблицу сведён синтаксис, используемый в различных языках программирования для функциональных типов, а также соответствующие примеры сигнатуры типа для функции композиции функций .

Язык программирования		Нотация	Пример
С поддержкой первоклассных функций , параметрического полиморфизма	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);
	Go	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++ с блоками	ρ (^)( α 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
	Standard ML	α -> ρ	compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
Без первоклассных функций , параметрического полиморфизма	Си	ρ (*)( α 1 , α 2 ,..., α n )	int (*compose(int (*f)(int), int (*g)(int)))(int);

Следует обратить внимание, что в примере на C# функция compose имеет тип « Func< Func<A,B>, Func<B,C>, Func<A,C> > ».

Денотационная семантика

Функциональный тип в языках программирования не соответствует пространству всех теоретико-множественных функций. Если принять счётно бесконечный тип натуральных чисел в качестве области определения и тип булевых чисел в качестве области значений, то существует несчётное количество ( ${\displaystyle 2^{\aleph _{0}}={\mathfrak {c}}}$ — мощность континуума ) теоретико-множественных функций между ними. Очевидно, это множество функций заведомо шире множества функций, определимых в языках программирования, так как существует лишь счётное множество программ (где программа представляет собой конечную цепочку из символов конечного набора).

занимается поиском более подходящих моделей (называемых ), в том числе, для моделирования таких понятий языков программирования как функциональный тип. В денотационной семантике считается, что целесообразно не ограничиваться лишь вычислимыми функциями , а использовать любые непрерывные по Скотту функции на частично упорядоченных множествах , которыми возможно смоделировать также и (а таковые возникают во всяком полном по Тьюрингу языке). Средства теории областей, используемые в денотационной семантике, достаточно выразительны, например, непрерывной по Скотту функцией моделируется « parallel or » , определимый далеко не во всех языках программирования.

См. также

• Декартово замкнутая категория
• Экспоненциал — эквивалент в теории категорий
• Функции первого класса

Ссылки

• Бенджамин Пирс . Types and Programming Languages. — The MIT Press. — С. 99-100.
• . . — The MIT Press, 1996.
• (англ.) . Institute for Advanced Study (2013). — раздел 1.2