Функційний тип

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

Функційний тип залежить від типів параметрів та типу повертаного значення функції. Іншими словами, це тип вищого роду. У теоретичних моделях і мовах з підтримкою каррування, наприклад в просто типізованому лямбда-численні^[en], функційний тип залежить від двох типів: області визначення $A$ та області значень $B$ . У цьому випадку функційний тип, слідуючи математичної традиції, зазвичай записують як $A\to B$ , або як $B^{A}$ , маючи на увазі, що існує рівно $|B|^{|A|}$ теоретико-множинних функцій, відображаючих $A$ на $B$ .

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

Мови програмування

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

Мови програмування		Нотація	Приклад сигнатури типу
З підтримкою функцій першого класу, параметричного поліморфізму	C++11	`std::function<ρ (α₁,α₂,...,α_n)>`	`function<function<int(int)>(function<int(int)>, function<int(int)>)> compose;`
	C#	`Func<α₁,α₂,...,α_n,ρ>`	`Func<A,C> compose(Func<A,B> f, Func<B,C> g);`
	Go	`func(α₁,α₂,...,α_n) ρ`	`var compose func(func(int)int, func(int)int) func(int)int`
	Haskell	`α -> ρ`	`compose :: (a -> b) -> (b -> c) -> a -> c`
	Objective-C	`ρ (^)(α₁,α₂,...,α_n)`	`int (^compose(int (^f)(int), int (^g)(int)))(int);`
	OCaml	`α -> ρ`	`compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c`
	Scala	`(α₁,α₂,...,α_n) => ρ`	`def compose[A, B, C](f: B => C, g: A => B): A => C`
	Standard ML	`α -> ρ`	`compose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c`
Без першокласних функцій, параметричного поліморфізму	C	`ρ (*)(α₁,α₂,...,α_n)`	`int (compose(int (f)(int), int (*g)(int)))(int);`

Слід звернути увагу, що в прикладі на C# функція compose має тип «Func< Func<A,B>, Func<B,C>, Func<A,C> >».

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

Функційний тип в мовах програмування не відповідає простору всіх теоретико-множинних функцій. Якщо прийняти зліченний тип натуральних чисел як область визначення і тип булевих чисел як область значень, то існує незлічена кількість теоретико-множинних функцій між ними. Очевидно, ця множина функцій ширше множини функцій, визначених в мовах програмування, так як існує лише зліченна множина програм (де програма являє собою кінцевий ланцюжок із символів кінцевого набору).

Денотаціонна семантика займається пошуком більш відповідних моделей, яких називають областями, в тому числі, для моделювання таких понять мов програмування як функційний тип. У денотаціонной семантиці вважається, що доцільно не обмежуватися лише обчислюваною функцією, а використовувати будь-які неперервні за Скоттом функції^[en] на частково впорядкованих множинах, якими можливо змоделювати також й обчислення, що не закінчуються. Засоби теорії областей, які використовуються в денотаціонной семантиці, досить виразні, наприклад, безперервної по Скотту функцією моделюється «parallel or», визначний далеко не у всіх мовах програмування.

Див. також

Функція першого класу

Посилання

Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program (англ.). Institute for Advanced Study. 2013. — розділ 1.2

Функційний тип

Мови програмування

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

Див. також

Посилання

Portal di Ensiklopedia Dunia