Тип функции

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

Тип функции зависит от типа параметров и типа результата функции (точнее, неиспользуемого конструктора типа). · → ·, является типом высшего рода ). В теоретических установках и языках программирования , где функции определены в каррированной форме , таких как просто типизированное лямбда-исчисление тип функции зависит ровно от двух типов: домена A и диапазона B. , Здесь тип функции часто обозначается A → B , следуя математическому соглашению, или B. ^А , исходя из того, что существует ровно B ^А (экспоненциально многие) теоретико-множественные функции, отображающие A в B в категории множеств . Класс таких отображений или функций называется экспоненциальным объектом . Каррирование ; делает тип функции смежным с продукта типом это подробно рассматривается в статье о каррировании.

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

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

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

Язык		Обозначения	Пример подписи типа
С первоклассными функциями , параметрический полиморфизм	С#	Func<α1,α2,...,αn,ρ>	Func<A,C> compose(Func<B,C> f, Func<A,B> g);
	Хаскелл	α -> ρ	compose :: (b -> c) -> (a -> b) -> a -> c
	OCaml	α -> ρ	compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
	Скала	(α1,α2,...,αn) => ρ	def compose[A, B, C](f: B => C, g: A => B): A => C
	Стандартный ML	α -> ρ	compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
	Быстрый	α -> ρ	func compose<A,B,C>(f: (B) -> C, g: (A) -> B) -> (A) -> C
	Ржавчина	fn(α1,α2,...,αn) -> ρ	fn compose<A, B, C>(f: fn(A) -> B, g: fn(B) -> C) -> fn(A) -> C
С первоклассными функциями , без параметрического полиморфизма	Идти	func(α1,α2,...,αn) ρ	var compose func(func(int)int, func(int)int) func(int)int
	C++ , Objective-C , с блоками	ρ (^)(α1,α2,...,αn)	int (^compose(int (^f)(int), int (^g)(int)))(int);
Без первоклассных функций , параметрический полиморфизм	С	ρ (*)(α1,α2,...,αn)	int (*compose(int (*f)(int), int (*g)(int)))(int);
	С++11	Не уникальный. std::function<ρ (α1,α2,...,αn)> является более общим типом (см. ниже).	function<function<int(int)>(function<int(int)>, function<int(int)>)> compose;

Если посмотреть на пример сигнатуры типа, например C#, тип функции compose на самом деле Func<Func<A,B>,Func<B,C>,Func<A,C>>.

Из-за стирания типов в C++11 std::function, чаще используются шаблоны для параметров функций более высокого порядка и вывода типа ( auto) для замыканий .

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

Тип функции в языках программирования не соответствует пространству всех теоретико-множественных функций. Учитывая счетный бесконечный тип натуральных чисел в качестве области определения и логических значений в качестве диапазона, тогда существует несчетное бесконечное число (2 ^{ℵ ₀} = c ) теоретико-множественных функций между ними. Очевидно, что это пространство функций больше, чем количество функций, которые могут быть определены на любом языке программирования, поскольку существует только счетное количество программ (программа представляет собой конечную последовательность конечного числа символов) и одну из теоретико-множественных функций эффективно решает проблему остановки .

Денотационная семантика занимается поиском более подходящих моделей (называемых доменами ) для моделирования концепций языка программирования, таких как типы функций. Оказывается, что ограничения выражения набором вычислимых функций также недостаточно, если язык программирования позволяет записывать непрерывные вычисления (что имеет место, если язык программирования является полным по Тьюрингу ). Выражение должно быть ограничено так называемыми непрерывными функциями (соответствующими непрерывности в топологии Скотта , а не непрерывности в реальном аналитическом смысле). Но даже в этом случае множество непрерывных функций содержит параллельную функцию-ИЛИ , которая не может быть правильно определена во всех языках программирования.

См. также

• Декартова закрытая категория
• каррирование
• Экспоненциальный объект , теоретико-категорный эквивалент
• Первоклассная функция
• Функциональное пространство , теоретико-множественный эквивалент

Ссылки

• Пирс, Бенджамин К. (2002). Типы и языки программирования . Массачусетский технологический институт Пресс. стр. 99–100 . ISBN  9780262162098 .
• Митчелл, Джон К. Основы языков программирования . Массачусетский технологический институт Пресс.
• тип функции в n Lab
• Теория гомотопических типов: одновалентные основы математики , Программа одновалентных оснований, Институт перспективных исследований . См. раздел 1.2 .