Funktionell typ

Funktionell typ ( piltyp , exponentiell ) inom datavetenskap  - typen av en variabel eller parameter , vars värde eller som kan vara en funktion ; eller typen av argument eller returvärde för en högre ordningsfunktion som accepterar eller returnerar en funktion.

Funktionstypen beror på parametertyperna och funktionens resultattyp . Det är med andra ord en typ av högsta slag , eller, mer exakt, en otillämpad typkonstruktor " ". I teoretiska modeller och språk som stöder currying , som den enkelt skrivna lambdakalkylen , beror funktionstypen på exakt två typer: domän och värdedomän . I det här fallet skrivs funktionstypen, enligt den matematiska traditionen, vanligtvis som (i praktiska programmeringsspråk- ), eller som , vilket antyder att det finns exakt mängdteoretiska funktioner som mappar till . När det gäller Curry-Howard-korrespondensen, är bebyggelsen av en funktionell typ likvärdig med bevisbarheten av en logisk implikation . A -> B

En funktionstyp kan ses som ett specialfall av en beroende produkt av typer . Bland andra egenskaper bär en sådan representation idén om en polymorf funktion .

Programmeringsspråk

Följande tabell sammanfattar syntaxen som används i olika programmeringsspråk för funktionstyper, såväl som motsvarande typsignaturexempel för funktionssammansättningsfunktionen .

Programmeringsspråk Notation Typ Signatur Exempel
Med stöd för förstklassiga funktioner ,
parametrisk polymorfism 		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);
gå 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++ med block ρ (^)(α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
Inga förstklassiga funktioner ,
parametrisk polymorfism 		Xi ρ (*)(α1,α2,...,αn) int (*compose(int (*f)(int), int (*g)(int)))(int);

Observera att i C# -exemplet är funktionen composeav typen " Func< Func<A,B>, Func<B,C>, Func<A,C> >".

Denotationssemantik

Funktionstypen i programmeringsspråk motsvarar inte utrymmet för alla set-teoretiska funktioner. Om vi ​​tar den oräkneligt oändliga typen av naturliga tal som definitionsdomän och typen av booleska tal som domänen av värden, så finns det ett oräkneligt antal ( är kontinuumets  makt ) mängdteoretiska funktioner mellan dem. Uppenbarligen är denna uppsättning funktioner förvisso bredare än uppsättningen funktioner som definieras i programmeringsspråk, eftersom det bara finns en räknebar uppsättning program (där programmet är en ändlig sträng av tecken från en ändlig uppsättning).

Denotationssemantik letar efter mer lämpliga modeller (kallade regioner ), inklusive för modellering av programmeringsspråkskoncept som funktionstyp. Inom denotationssemantik tror man att det är lämpligt att inte begränsas endast till beräkningsbara funktioner , utan att använda alla Scott-kontinuerliga funktioner på partiellt ordnade uppsättningar , som också kan modellera oslutliga beräkningar (och de som uppstår i alla Turing- komplett språk). Medlen för teorin om områden som används i denotationssemantik är ganska uttrycksfulla, till exempel modelleras Scott-kontinuerlig funktion av " parallel or" , som inte definieras i alla programmeringsspråk.

Se även

Länkar

 Datatyper
Otolkbart
Numerisk
Text
Referens
Sammansatt
abstrakt
Övrig
Relaterade ämnen