Skriv slutning

Skriv inferens ( eng. type inference ) - i programmering , compilerens evne til logisk at udlede typen af værdien af selve udtrykket . Typeinferensmekanismen blev først introduceret i ML -sproget , hvor compileren altid udleder den mest generelle polymorfe type for ethvert udtryk. Dette reducerer ikke kun størrelsen af kildekoden og øger dens kortfattethed, men øger ofte kodegenbrug [1] .

Typeinferens er karakteristisk for funktionelle programmeringssprog , selvom den gennem tiden er delvist implementeret i objektorienterede sprog ( C# , D , Visual Basic.NET , Nim , C++11 , Vala , Java [a] ), hvor det er begrænset til muligheden for at udelade typen af en identifikator i en definition med initialisering (se syntaktisk sukker ). For eksempel:

var s = "Hej verden!" ; // Variablens type s (fra streng) er afledt fra initializeren

Algoritmer

Hindley-Milner algoritme

Hindley-Milner-algoritmen er en udtrykstype-inferensmekanisme implementeret i programmeringssprog baseret på Hindley-Milner-typesystemet , såsom ML (det første sprog i denne familie), Standard ML , OCaml , Haskell , F# , Fortress og Boo . Nemerle - sproget bruger denne algoritme med en række nødvendige modifikationer [2] .

Typeslutningsmekanismen er baseret på evnen til automatisk at udlede, helt eller delvist, typen af et udtryk opnået ved at evaluere et udtryk. Da denne proces udføres systematisk under programoversættelse, kan compileren ofte udlede typen af en variabel eller funktion uden eksplicit at specificere typerne af disse objekter. I mange tilfælde kan eksplicitte typeerklæringer udelades - dette kan gøres for ret simple objekter eller for sprog med simpel syntaks. For eksempel har Haskell-sproget en ret kraftig typeinferensmekanisme, så det er ikke nødvendigt at specificere funktionerne i dette programmeringssprog. Programmereren kan specificere typen af en funktion eksplicit for at begrænse dens brug til specifikke datatyper eller for mere struktureret kildekodeformatering.

For at opnå information til den korrekte udledning af typen af et udtryk i mangel af en eksplicit erklæring af typen af dette udtryk, indsamler oversætteren enten sådanne oplysninger fra de eksplicitte erklæringer af typerne af underudtryk (variabler, funktioner) inkluderet i det undersøgte udtryk, eller bruger implicit information om typerne af atomværdier. En sådan algoritme hjælper ikke altid med at bestemme typen af et udtryk, især i tilfælde af brug af højere-ordens funktioner og parametrisk polymorfi af en ret kompleks karakter. I komplekse sager, hvor der er behov for at undgå uklarheder, anbefales det derfor eksplicit at specificere typen af udtryk.

Selve typningsmodellen er baseret på udtrykstype-inferensalgoritmen, som har som kilde den udtrykstypeafledningsmekanisme, der anvendes i den typebestemte λ-calculus , som blev foreslået i 1958 af H. Curry og R. Face. Yderligere udvidede Roger Hindley i 1969 selve algoritmen og beviste, at den stammer fra den mest generelle type udtryk. I 1978 beviste Robin Milner , uafhængigt af R. Hindley, egenskaberne ved en tilsvarende algoritme. Og endelig, i 1985 , viste Louis Damas endelig, at Milners algoritme er komplet og kan bruges til polymorfe typer. I denne henseende kaldes Hindley-Milner-algoritmen nogle gange også Damas-Milner-algoritmen .

Typesystemet er defineret i Hindley-Milner modellen som følger:

Primitive typer er udtrykstyper. $v$
Parametriske typevariabler α er udtrykstyper.
Hvis og er udtrykstyper, så er typen udtrykstypen. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\højrepil \sigma _{{2}}$
Et symbol er en type udtryk. $\bot$

De udtryk, hvis typer evalueres, er defineret på en ret standard måde:

Konstanter er udtryk.
Variabler er udtryk.
Hvis og er udtryk, så er ( ) et udtryk. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
Hvis er en variabel og er et udtryk, så er et udtryk. $v$ $e$ $\lambda ve$

En type siges at være en forekomst af type, når der er en konvertering , sådan at: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

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

I dette tilfælde antages det normalt, at typekonverteringer er underlagt begrænsninger, som er: $\rho$

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

Selve typeinferensalgoritmen består af to trin - generering af et ligningssystem og den efterfølgende løsning af disse ligninger.

Konstruktion af et ligningssystem

Konstruktionen af et ligningssystem er baseret på følgende regler:

$\Gamma v=\tau$ - hvis bindingen er i . $v:\tau$ $\Gamma$
$\Gamma (ge)=\tau$ — hvis , hvor og . $\tau _{{1}}=\tau _{{2}}\højrepil \tau$ $\tau _{1}=\Gamma g$ $\tau _{2}=\Gamma e$
${\displaystyle \Gamma (\lambda ve)=\tau \rightarrow \tau _{e))$ - i tilfælde af at , hvor det er med den tilføjede binding . $\tau _{e}=\Gamma 'e$ $\gamma '$ $\Gamma$ $v:\tau$

I disse regler er et symbol et sæt associationer mellem variabler og deres typer: $\Gamma$

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

Løsning af et ligningssystem

Løsningen af det konstruerede ligningssystem er baseret på foreningsalgoritmen . Dette er en ret simpel algoritme. Der er en funktion , der tager en ligning af typer som input og returnerer en substitution, der gør venstre og højre side af ligningen ens ("forener" dem). Substitution er simpelthen en projektion af variable typer på selve typerne. Sådanne substitutioner kan beregnes på forskellige måder, som afhænger af den specifikke implementering af Hindley-Milner-algoritmen. $u$

Se også

Noter

Kommentarer

↑ understøttelse tilføjet i Java SE 10

Kilder

↑ Andrew W. Appel. En kritik af Standard ML. — Princeton University, revideret version af CS-TR-364-92, 1992.
↑ Michal Moskal. Skriv slutning med udsættelse . - 2005.