Funktionstyp
Inom datavetenskap och matematisk logik är en funktionstyp (eller piltyp eller exponentiell ) typen av en variabel eller parameter som en funktion har eller kan tilldelas, eller ett argument eller resultattyp för en högre ordningsfunktion som tar eller returnerar en funktion.
En funktionstyp beror på typen av parametrar och funktionens resultattyp (den, eller rättare sagt den otillämpade typkonstruktören · → · , är en typ av högre typ ). I teoretiska inställningar och programmeringsspråk där funktioner definieras i curryform , som den enkelt skrivna lambdakalkylen , beror en funktionstyp på exakt två typer, domänen A och intervallet B. Här betecknas ofta en funktionstyp A → B , enligt matematisk konvention, eller B A , baserat på det existerande exakt B A (exponentiellt många) mängdteoretiska funktioner avbildningar A till B i kategorin mängder . Klassen av sådana kartor eller funktioner kallas exponentialobjektet . Curryningen att funktionstypen ansluter till produkttypen ; detta utforskas i detalj i artikeln om curry.
Funktionstypen kan anses vara ett specialfall av den beroende produkttypen , som bland andra egenskaper omfattar idén om en polymorf funktion .
Programmeringsspråk
Syntaxen som används för funktionstyper i flera programmeringsspråk kan sammanfattas, inklusive ett exempel på typsignatur för den högre ordningens funktionskompositionsfunktionen :
| Språk | Notation | Exempel typ signatur | |
|---|---|---|---|
|
Med förstklassiga funktioner , parametrisk polymorfism |
C# |
Func< α 1 , α 2 ,..., α n , ρ >
|
Func < A , C > compose ( Func < B , C > f , Func < A , B > g );
|
| Haskell |
α -> ρ
|
komponera :: ( b -> c ) -> ( a -> b ) -> a -> c
|
|
| OCaml |
α -> ρ
|
komponera : ( ' b -> ' c ) -> ( ' a -> ' b ) -> ' a -> ' c
|
|
| Scala |
( ai , a2 , ..., an ) = > ρ
|
def compose [ A , B , C ]( f : B => C , g : A => B ): A => C
|
|
| Standard ML |
α -> ρ
|
komponera : ( 'b -> 'c ) -> ( 'a -> 'b ) -> 'a -> 'c
|
|
| Snabb |
α -> ρ
|
func compose < A , B , C >( f : ( B ) -> C , g : ( A ) -> B ) -> ( A ) -> C
|
|
| Rost |
fn( α 1 , α 2 ,..., α n ) -> ρ
|
fn komponera < A , B , C > ( f : fn ( A ) -> B , g : fn ( B ) -> C ) -> fn ( A ) -> C
|
|
|
Med förstklassiga funktioner , utan parametrisk polymorfism |
Gå |
func ( 1 , α 2 ,..., α n ) ρ
|
var compose func ( func ( int ) int , func ( int ) int ) func ( int ) int
|
| C++ , Objective-C , med block |
ρ (^)( α 1 , α 2 ,..., α n )
|
int ( ^ compose ( int ( ^ f )( int ), int ( ^ g )( int )))( int );
|
|
|
Utan förstklassiga funktioner , parametrisk polymorfism |
C |
ρ (*)( α 1 , α 2 ,..., α n )
|
int ( * compose ( int ( * f )( int ), int ( * g )( int )))( int );
|
| C++11 | Inte unikt.
|
funktion < funktion < int ( int ) > ( funktion < int ( int ) > , funktion < int ( int ) > ) > komponera ;
|
|
När man tittar på exempeltypsignaturen för till exempel C#, är typen av funktionen compose faktiskt Func<Func<A,B>,Func<B,C>,Func<A,C>> .
På grund av typradering i C++11s std::funktion är det vanligare att använda mallar för funktionsparametrar av högre ordning och typinferens ( auto ) för stängningar .
Denotationssemantik
Funktionstypen i programmeringsspråk motsvarar inte utrymmet för alla mängdteoretiska funktioner. Givet den räkningsbart oändliga typen av naturliga tal som domän och booleanerna som intervall, så finns det ett oräkneligt oändligt antal (2 ℵ 0 = c ) av mängdteoretiska funktioner mellan dem. Uppenbarligen är detta utrymme av funktioner större än antalet funktioner som kan definieras i vilket programmeringsspråk som helst, eftersom det bara finns otaliga många program (ett program är en ändlig sekvens av ett ändligt antal symboler) och en av de mängdteoretiska funktionerna löser effektivt stoppproblemet .
Denotationssemantik sysslar med att hitta mer lämpliga modeller (kallade domäner ) för att modellera programmeringsspråkskoncept som funktionstyper. Det visar sig att det inte räcker att begränsa uttrycket till uppsättningen av beräkningsbara funktioner heller om programmeringsspråket tillåter skrivning av icke-avslutande beräkningar (vilket är fallet om programmeringsspråket är Turing komplett ). Uttrycket måste begränsas till de så kallade kontinuerliga funktionerna (motsvarande kontinuitet i Scott-topologin , inte kontinuitet i verklig analytisk mening). Även då innehåller uppsättningen av kontinuerlig funktion parallell-eller- funktionen, som inte kan definieras korrekt i alla programmeringsspråk.
Se även
- Kartesisk sluten kategori
- Curry
- Exponentiellt objekt , kategoriteoretisk motsvarighet
- Förstklassig funktion
- Funktionsutrymme , mängdteoretisk motsvarighet
- Pierce, Benjamin C. (2002). Typer och programmeringsspråk . MIT Press. s. 99 –100. ISBN 9780262162098 .
- Mitchell, John C. Grunder för programmeringsspråk . MIT Press.
- funktionstyp vid n Lab
- Homotopy Type Theory: Univalent Foundations of Mathematics , The Univalent Foundations Program, Institute for Advanced Study . Se avsnitt 1.2 .