Функційний тип (стрілочний тип, експоненціал) у інформатиці — тип змінної або параметра, значенням якої або якого може бути функція; або тип аргументу чи повертаного значення функції вищого порядку, приймаючий або повертаючий функцію.
Функційний тип залежить від типів параметрів та типу повертаного значення функції. Іншими словами, це тип вищого роду. У теоретичних моделях і мовах з підтримкою каррування, наприклад в [en], функційний тип залежить від двох типів: області визначення та області значень . У цьому випадку функційний тип, слідуючи математичної традиції, зазвичай записують як , або як , маючи на увазі, що існує рівно теоретико-множинних функцій, відображаючих на .
Функційний тип можна розглядати як окремий випадок залежного творення типів. Серед інших властивостей, таке уявлення несе в собі ідею поліморфної функції.
Мови програмування
У наступну таблицю зведено синтаксис, який використовується в різних мовах програмування для функційних типів, а також відповідні приклади сигнатури типу для функції композиції функцій.
Мови програмування | Нотація | Приклад сигнатури типу | |
---|---|---|---|
З підтримкою функцій першого класу, [ru] | 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 | |
Без першокласних функцій, [ru] | 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> >
».
Денотаціонна семантика
Функційний тип в мовах програмування не відповідає простору всіх теоретико-множинних функцій. Якщо прийняти зліченний тип натуральних чисел як область визначення і тип булевих чисел як область значень, то існує незлічена кількість теоретико-множинних функцій між ними. Очевидно, ця множина функцій ширше множини функцій, визначених в мовах програмування, так як існує лише зліченна множина програм (де програма являє собою кінцевий ланцюжок із символів кінцевого набору).
Денотаціонна семантика займається пошуком більш відповідних моделей, яких називають областями, в тому числі, для моделювання таких понять мов програмування як функційний тип. У денотаціонной семантиці вважається, що доцільно не обмежуватися лише обчислюваною функцією, а використовувати будь-які [en] на частково впорядкованих множинах, якими можливо змоделювати також й обчислення, що не закінчуються. Засоби теорії областей, які використовуються в денотаціонной семантиці, досить виразні, наприклад, безперервної по Скотту функцією моделюється «parallel or
», визначний далеко не у всіх мовах програмування.
Див. також
Посилання
- Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program (англ.). Institute for Advanced Study. 2013. — розділ 1.2
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Funkcijnij tip strilochnij tip eksponencial u informatici tip zminnoyi abo parametra znachennyam yakoyi abo yakogo mozhe buti funkciya abo tip argumentu chi povertanogo znachennya funkciyi vishogo poryadku prijmayuchij abo povertayuchij funkciyu Funkcijnij tip zalezhit vid tipiv parametriv ta tipu povertanogo znachennya funkciyi Inshimi slovami ce tip vishogo rodu U teoretichnih modelyah i movah z pidtrimkoyu karruvannya napriklad v en funkcijnij tip zalezhit vid dvoh tipiv oblasti viznachennya A displaystyle A ta oblasti znachen B displaystyle B U comu vipadku funkcijnij tip sliduyuchi matematichnoyi tradiciyi zazvichaj zapisuyut yak A B displaystyle A to B abo yak B A displaystyle B A mayuchi na uvazi sho isnuye rivno B A displaystyle B A teoretiko mnozhinnih funkcij vidobrazhayuchih A displaystyle A na B displaystyle B Funkcijnij tip mozhna rozglyadati yak okremij vipadok zalezhnogo tvorennya tipiv Sered inshih vlastivostej take uyavlennya nese v sobi ideyu polimorfnoyi funkciyi Movi programuvannyaU nastupnu tablicyu zvedeno sintaksis yakij vikoristovuyetsya v riznih movah programuvannya dlya funkcijnih tipiv a takozh vidpovidni prikladi signaturi tipu dlya funkciyi kompoziciyi funkcij Movi programuvannya Notaciya Priklad signaturi tipu Z pidtrimkoyu funkcij pershogo klasu ru C 11 std function lt i r i i a i sub 1 sub i a i sub 2 sub i a sub n sub i gt function lt function lt int int gt function lt int int gt function lt int int gt gt compose C Func lt i a i sub 1 sub i a i sub 2 sub i a sub n sub i i r i gt Func lt A C gt compose Func lt A B gt f Func lt B C gt g Go func i a i sub 1 sub i a i sub 2 sub i a sub n sub i i r i var compose func func int int func int int func int int Haskell i a i gt i r i compose a gt b gt b gt c gt a gt c Objective C i r i i a i sub 1 sub i a i sub 2 sub i a sub n sub i int compose int f int int g int int OCaml i a i gt i r i compose a gt b gt b gt c gt a gt c Scala i a i sub 1 sub i a i sub 2 sub i a sub n sub i gt i r i def compose A B C f B gt C g A gt B A gt C Standard ML i a i gt i r i compose a gt b gt b gt c gt a gt c Bez pershoklasnih funkcij ru C i r i i a i sub 1 sub i a i sub 2 sub i a sub n sub i int compose int f int int g int int Slid zvernuti uvagu sho v prikladi na C funkciya compose maye tip Func lt Func lt A B gt Func lt B C gt Func lt A C gt gt Denotacionna semantikaFunkcijnij tip v movah programuvannya ne vidpovidaye prostoru vsih teoretiko mnozhinnih funkcij Yaksho prijnyati zlichennij tip naturalnih chisel yak oblast viznachennya i tip bulevih chisel yak oblast znachen to isnuye nezlichena kilkist teoretiko mnozhinnih funkcij mizh nimi Ochevidno cya mnozhina funkcij shirshe mnozhini funkcij viznachenih v movah programuvannya tak yak isnuye lishe zlichenna mnozhina program de programa yavlyaye soboyu kincevij lancyuzhok iz simvoliv kincevogo naboru Denotacionna semantika zajmayetsya poshukom bilsh vidpovidnih modelej yakih nazivayut oblastyami v tomu chisli dlya modelyuvannya takih ponyat mov programuvannya yak funkcijnij tip U denotacionnoj semantici vvazhayetsya sho docilno ne obmezhuvatisya lishe obchislyuvanoyu funkciyeyu a vikoristovuvati bud yaki en na chastkovo vporyadkovanih mnozhinah yakimi mozhlivo zmodelyuvati takozh j obchislennya sho ne zakinchuyutsya Zasobi teoriyi oblastej yaki vikoristovuyutsya v denotacionnoj semantici dosit virazni napriklad bezperervnoyi po Skottu funkciyeyu modelyuyetsya parallel or viznachnij daleko ne u vsih movah programuvannya Div takozhFunkciya pershogo klasuPosilannyaHomotopy Type Theory Univalent Foundations of Mathematics The Univalent Foundations Program angl Institute for Advanced Study 2013 rozdil 1 2