Skriv slutledning

Typ inferens ( eng. typ inference ) - i programmering , kompilatorns förmåga att logiskt härleda typen av värdet för själva uttrycket . Typinferensmekanismen introducerades först i ML-språket , där kompilatorn alltid härleder den mest allmänna polymorfa typen för alla uttryck. Detta minskar inte bara storleken på källkoden och ökar dess koncisitet, utan ökar ofta kodåteranvändningen [1] .

Typinferens är karakteristisk för funktionella programmeringsspråk , även om den med tiden delvis har implementerats i objektorienterade språk ( C# , D , Visual Basic .NET , Nim , C++11 , Vala , Java [a] ), där den är begränsad till möjligheten att utelämna typen av en identifierare i en definition med initialisering (se syntaktisk socker ). Till exempel:

var s = "Hej världen!" ; // Typen av variabeln s (från sträng) härleds från initialiseraren

Algoritmer

Hindley-Milner algoritm

Hindley-Milner-algoritmen är en inferensmekanism för uttryckstyp implementerad i programmeringsspråk baserade på Hindley-Milner-systemet , såsom ML (det första språket i denna familj), Standard ML , OCaml , Haskell , F# , Fortress och Boo . Nemerle - språket använder denna algoritm med ett antal nödvändiga modifieringar [2] .

Typinferensmekanismen är baserad på förmågan att automatiskt härleda, helt eller delvis, typen av ett uttryck som erhålls genom att utvärdera något uttryck. Eftersom denna process systematiskt utförs under programöversättning kan kompilatorn ofta sluta sig till typen av en variabel eller funktion utan att explicit specificera typerna av dessa objekt. I många fall kan explicita typdeklarationer utelämnas - detta kan göras för ganska enkla objekt eller för språk med enkel syntax. Till exempel har Haskell-språket en ganska kraftfull typinferensmekanism, så det är inte nödvändigt att specificera typerna av funktioner i detta programmeringsspråk. Programmeraren kan specificera typen av en funktion uttryckligen för att begränsa dess användning till specifika datatyper, eller för mer strukturerad källkodsformatering.

För att erhålla information för korrekt slutledning av typen av ett uttryck i avsaknad av en explicit deklaration av typen av detta uttryck, samlar översättaren antingen in sådan information från de explicita deklarationerna av de typer av underuttryck (variabler, funktioner) som ingår i det studerade uttrycket, eller använder implicit information om typerna av atomvärden. En sådan algoritm hjälper inte alltid till att bestämma typen av ett uttryck, särskilt i fall av användning av högre ordningsfunktioner och parametrisk polymorfism av en ganska komplex natur. Därför, i komplexa fall, när det finns ett behov av att undvika oklarheter, rekommenderas det att uttryckligen specificera typen av uttryck.

Själva typningsmodellen är baserad på uttryckstypinferensalgoritmen, som har som källa den uttryckstypsderivationsmekanism som används i den typade λ-kalkylen , som föreslogs 1958 av H. Curry och R. Face. Vidare utökade Roger Hindley 1969 själva algoritmen och bevisade att den härleder den mest allmänna typen av uttryck. 1978 bevisade Robin Milner , oberoende av R. Hindley, egenskaperna hos en likvärdig algoritm. Och slutligen, 1985 , visade Louis Damas äntligen att Milners algoritm är komplett och kan användas för polymorfa typer. I detta avseende kallas Hindley-Milner-algoritmen ibland även Damas-Milner-algoritmen .

Typsystemet definieras i Hindley-Milner-modellen enligt följande:

Primitiva typer är uttryckstyper. $v$
Parametriska typvariabler α är uttryckstyper.
Om och är uttryckstyper, så är typen uttryckstypen. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\högerpil \sigma _{{2}}$
En symbol är en typ av uttryck. $\bot$

De uttryck vars typer utvärderas definieras på ett ganska standardiserat sätt:

Konstanter är uttryck.
Variabler är uttryck.
Om och är uttryck, då är ( ) ett uttryck. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
Om är en variabel och är ett uttryck, då är ett uttryck. $v$ $e$ $\lambda ve$

En typ sägs vara en instans av typ när det finns någon konvertering så att: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

$\sigma _{{1}}=\rho (\sigma _{{2}})$

I det här fallet antas det vanligtvis att typkonverteringar är föremål för restriktioner, som är att: $\rho$

$\rho (\sigma _{{1}}\högerpil \sigma _{{2}})=\rho (\sigma _{{1}})\högerpil \rho (\sigma _{{2}})$
$\rho (v)=v$

Själva typinferensalgoritmen består av två steg - genereringen av ett ekvationssystem och den efterföljande lösningen av dessa ekvationer.

Konstruktion av ett ekvationssystem

Konstruktionen av ett ekvationssystem bygger på följande regler:

$\Gamma v=\tau$ - om bindningen är i . $v:\tau$ $\Gamma$
$\Gamma (ge)=\tau$ — om , var och . $\tau _{{1}}=\tau _{{2}}\högerpil \tau$ $\tau _{1}=\Gamma g$ $\tau _{2}=\Gamma e$
${\displaystyle \Gamma (\lambda ve)=\tau \högerpil \tau _{e))$ - i händelse av att , var den är med tilläggsbindning . $\tau _{e}=\Gamma 'e$ $\gamma '$ $\Gamma$ $v:\tau$

I dessa regler är en symbol en uppsättning associationer mellan variabler och deras typer: $\Gamma$

$\Gamma =v_{{1}}:A_{{1}},v_{{2}}:A_{{2}},\ldots ,v_{{n}}:A_{{n}}$

Lösa ett ekvationssystem

Lösningen av det konstruerade ekvationssystemet är baserad på föreningsalgoritmen . Detta är en ganska enkel algoritm. Det finns någon funktion som tar en ekvation av typer som indata och returnerar en substitution som gör att vänster och höger sida av ekvationen blir lika ("förenar" dem). Substitution är helt enkelt en projektion av variabeltyper på själva typerna. Sådana substitutioner kan beräknas på olika sätt, vilket beror på den specifika implementeringen av Hindley-Milner-algoritmen. $u$

Se även

Anteckningar

Kommentarer

↑ stöd lagt till i Java SE 10

Källor

↑ Andrew W. Appel. En kritik av Standard ML. — Princeton University, reviderad version av CS-TR-364-92, 1992.
↑ Michal Moskal. Skriv inferens med uppskov . — 2005.

Länkar

Implementering av Hindley-Milner-algoritmen i Perl
Arkiverat e-postmeddelande av Roger Hindley, förklarar historien om typinferens
Polymorphic Type Inference av Michael Schwartzbach, ger en översikt över Polymorphic Type Inference.
Huvudsakliga typscheman för funktionsprogram. En omskriven kopia av Damas och Milner-tidningen som beskrev korrektheten och fullständighetsbevisen.
Handledning och fullständig implementering i Standard ML Handledningen innehåller en del av typsystemens logiska historia samt en detaljerad beskrivning av algoritmen som implementerad. Vissa typografiska fel i originalet Damas Milner har rättats.
Basic Typechecking papper av Luca Cardelli, beskriver algoritm, inkluderar implementering i Modula-2
Implementering av slutledning av Hindley-Milner-typ i Scala , av Andrew Forrest (hämtad 30 juli 2009)
Implementering av Hindley-Milner i Perl 5, av Nikita Borisov (inte tillgänglig länk) . Tillträdesdatum: 12 mars 2009. Arkiverad från originalet 18 februari 2007. (obestämd)
Vad är Hindley-Milner? (och varför är det coolt?) Förklarar Hindley-Milner, exempel i Scala
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Hindley-Milner typmodell och ett exempel på dess implementering i Haskell