Функціональний тип
Функціональний тип (функційний тип, стрілочний тип, експоненціал) у інформатиці — тип змінної або параметра, значенням якої або якого може бути функція; або тип аргументу чи повертаємого значення функції вищого порядку, приймаючий або повертаючий функцію.
Функціональний тип залежить від типів параметрів та типу повернення значення функції. Іншими словами, це тип вищого роду. У теоретичних моделях и мовах з підтримкою каррування, наприклад в просто типизованному лямбда-численні, функціональний тип залежить від двох типів: області визначення та області значень . У цьому випадку функціональний тип, слідуючи математичної традиції, зазвичай записують як (у практичних мовах програмування — A -> 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 | ρ (^)(α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 | |
| Без першокласних функцій,
параметричного поліморфізму |
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> >».
Денотаціонна семантика
Функціональний тип в мовах програмування не відповідає простору всіх теоретико-множинних функцій. Якщо прийняти лічильно нескінченний тип натуральних чисел як область визначення і тип булевих чисел як область значень, то існує незлічена кількість теоретико-множинних функцій між ними. Ймовірно, ця безліч функцій свідомо ширше безлічі функцій, визначених в мовах програмування, так як існує лише рахункова безліч програм (де програма являє собою кінцевий ланцюжок із символів кінцевого набору).
Денотаціонна семантика займається пошуком більш відповідних моделей, яких називають областями, в тому числі, для моделювання таких понять мов програмування як функціональний тип. У денотаціонной семантиці вважається, що доцільно не обмежуватися лише обчислюваною функцією, а використовувати будь-які безперервні по Скотту функції на частково впорядкованих множинах, якими можливо змоделювати також й обчислення, що не закінчуються. Засоби теорії областей, які використовуються в денотаціонной семантиці, досить виразні, наприклад, безперервної по Скотту функцією моделюється «parallel or», визначний далеко не у всіх мовах програмування.
Дивитись також
Посилання
- Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program (англ.). Institute for Advanced Study. 2013. — розділ 1.2