Typový závěr

Typová inference ( angl. type inference ) - v programování schopnost kompilátoru logicky odvodit typ hodnoty samotného výrazu . Mechanismus odvození typu byl poprvé představen v jazyce ML , kde kompilátor vždy odvodí nejobecnější polymorfní typ pro jakýkoli výraz. To nejen snižuje velikost zdrojového kódu a zvyšuje jeho stručnost, ale často zvyšuje opětovné použití kódu [1] .

Typová inference je charakteristická pro funkcionální programovací jazyky , i když postupem času byla částečně implementována v objektově orientovaných jazycích ( C# , D , Visual Basic .NET , Nim , C++11 , Vala , Java [a] ), kde je omezena na možnost vynechat typ identifikátoru v definici s inicializací (viz syntaktický cukr ). Například:

var s = "Ahoj světe!" ; // Typ proměnné s (z řetězce) je odvozen od inicializátoru

Algoritmy

Hindley-Milnerův algoritmus

Algoritmus Hindley-Milner je mechanismus odvození typu výrazu implementovaný v programovacích jazycích založených na systému typu Hindley-Milner , jako je ML (první jazyk této rodiny), Standard ML , OCaml , Haskell , F# , Fortress a Boo . Jazyk Nemerle používá tento algoritmus s řadou nezbytných úprav [2] .

Mechanismus odvození typu je založen na schopnosti automaticky odvodit, zcela nebo částečně, typ výrazu získaného vyhodnocením nějakého výrazu. Protože se tento proces systematicky provádí během překladu programu, kompilátor může často odvodit typ proměnné nebo funkce, aniž by explicitně specifikoval typy těchto objektů. V mnoha případech lze explicitní deklarace typu vynechat - to lze provést pro poměrně jednoduché objekty nebo pro jazyky s jednoduchou syntaxí. Například jazyk Haskell má poměrně výkonný mechanismus odvození typu, takže není nutné specifikovat typy funkcí v tomto programovacím jazyce. Programátor může specifikovat typ funkce explicitně, aby omezil její použití na konkrétní datové typy nebo pro strukturovanější formátování zdrojového kódu.

Aby překladatel získal informace pro správné vyvození typu výrazu v případě, že neexistuje explicitní deklarace typu tohoto výrazu, shromažďuje tyto informace buď z explicitních deklarací typů podvýrazů (proměnných, funkcí) obsažených. ve studovaném výrazu, nebo využívá implicitní informace o typech atomárních hodnot. Takovýto algoritmus ne vždy pomůže určit typ výrazu, zejména v případech použití funkcí vyšších řádů a parametrického polymorfismu poměrně složité povahy. Proto se ve složitých případech, kdy je potřeba vyhnout se nejasnostem, doporučuje výslovně specifikovat typ výrazů.

Samotný typizační model je založen na inferenčním algoritmu typu výrazu, jehož zdrojem je mechanismus odvození typu výrazu použitý v typovaném λ-kalkulu , který v roce 1958 navrhli H. Curry a R. Face. Dále Roger Hindley v roce 1969 rozšířil samotný algoritmus a dokázal, že odvozuje nejobecnější typ výrazu. V roce 1978 Robin Milner , nezávisle na R. Hindley, dokázal vlastnosti ekvivalentního algoritmu. A konečně v roce 1985 Louis Damas konečně ukázal , že Milnerův algoritmus je kompletní a může být použit pro polymorfní typy. V tomto ohledu je Hindley-Milnerův algoritmus někdy také nazýván Damas-Milnerův algoritmus .

Typový systém je definován v Hindley-Milnerově modelu takto:

Primitivní typy jsou typy výrazů. $proti$
Parametrické proměnné typu α jsou typy výrazů.
Jestliže a jsou typy výrazu, pak typ je typ výrazu. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\rightarrow \sigma _{{2}}$
Symbol je druh výrazů. $\bot$

Výrazy, jejichž typy se vyhodnocují, jsou definovány poměrně standardním způsobem:

Konstanty jsou výrazy.
Proměnné jsou výrazy.
Jestliže a jsou výrazy, pak ( ) je výraz. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
Jestliže je proměnná a je výraz, pak je výraz. $proti$ $E$ $\lambda ve$

O type se říká, že je instancí typu , když dojde k nějaké konverzi , která: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

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

V tomto případě se obvykle předpokládá, že typové konverze podléhají omezením, kterými jsou: $\rho$

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

Vlastní algoritmus typové inference se skládá ze dvou kroků - generování soustavy rovnic a následného řešení těchto rovnic.

Konstrukce soustavy rovnic

Konstrukce soustavy rovnic je založena na následujících pravidlech:

$\Gamma v=\tau$ - pokud je vazba v . $v:\tau$ $\Gamma$
$\Gamma (ge)=\tau$ — pokud , kde a . $\tau _{{1}}=\tau _{{2}}\rightarrow \tau$ $\tau _{1}=\Gamma g$ $\tau _{2}=\Gamma e$
${\displaystyle \Gamma (\lambda ve)=\tau \rightarrow \tau _{e))$ - v případě , kde je s přidanou vazbou . $\tau _{e}=\Gamma 'e$ $\gamma'$ $\Gamma$ $v:\tau$

V těchto pravidlech je symbolem soubor asociací mezi proměnnými a jejich typy: $\Gamma$

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

Řešení soustavy rovnic

Řešení sestrojeného systému rovnic je založeno na sjednocovacím algoritmu . Toto je poměrně jednoduchý algoritmus. Existuje nějaká funkce , která bere rovnici typů jako vstup a vrací substituci, která dělá levou a pravou stranu rovnice stejnou ("sjednocuje" je). Substituce je jednoduše projekce typů proměnných na typy samotné. Takové substituce lze vypočítat různými způsoby, které závisí na konkrétní implementaci Hindley-Milnerova algoritmu. $u$

Viz také

Poznámky

Komentáře

↑ podpora přidána do Java SE 10

Zdroje

↑ Andrew W. Appel. Kritika standardního ML. — Princetonská univerzita, revidovaná verze CS-TR-364-92, 1992.
↑ Michal Moskal. Typ Inference s odkladem . — 2005.

Odkazy

Implementace Hindley - Milnerova algoritmu v Perlu
Archivovaná e-mailová zpráva Rogera Hindleyho vysvětluje historii odvození typu
Polymorfní typová inference od Michaela Schwartzbacha poskytuje přehled polymorfní typové inference.
Hlavní typová schémata pro funkční programy. Překódovaná kopie listu Damas a Milner, která popisovala důkazy o správnosti a úplnosti.
Výukový program a kompletní implementace ve Standard ML Výukový program obsahuje část logické historie typových systémů a také podrobný popis implementovaného algoritmu. Některé typografické chyby v původním papíru Damas Milner jsou opraveny.
Základní Typechecking paper od Lucy Cardelli, popisuje algoritmus, zahrnuje implementaci v Modula-2
Implementace odvození typu Hindley-Milner v Scala , Andrew Forrest (získáno 30. července 2009)
Implementace Hindley-Milner v Perlu 5, Nikita Borisov (nedostupný odkaz) . Datum přístupu: 12. března 2009. Archivováno z originálu 18. února 2007. (neurčitý)
Co je Hindley-Milner? (a proč je to cool?) Vysvětluje Hindley-Milner, příklady ve Scale
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Hindley-Milnerův model psaní a příklad jeho implementace v Haskell