Típuskövetkeztetés

Típuskövetkeztetés ( eng. type inference ) - a programozásban a fordító azon képessége , hogy logikusan következtessen magának a kifejezés értékének típusára . A típuskövetkeztetési mechanizmust először az ML nyelvben vezették be , ahol a fordító mindig a kifejezés legáltalánosabb polimorf típusára következtet. Ez nemcsak a forráskód méretét csökkenti és tömörségét növeli, hanem gyakran növeli a kód újrafelhasználását [1] .

A típuskövetkeztetés a funkcionális programozási nyelvekre jellemző , bár az idők során részben az objektum-orientált nyelvekben is implementálták ( C# , D , Visual Basic .NET , Nim , C++11 , Vala , Java [a] ), ahol ez arra korlátozódik, hogy az inicializálással egy definícióban elhagyható az azonosító típusa (lásd szintaktikai cukor ). Például:

var s = "Szia, világ!" ; // Az s változó típusa (karakterláncból) az inicializálóból származik

Algoritmusok

Hindley-Milner algoritmus

A Hindley-Milner algoritmus egy kifejezéstípusú következtetési mechanizmus, amelyet a Hindley-Milner típusú rendszeren alapuló programozási nyelvekben valósítottak meg , mint például az ML (a család első nyelve), a Standard ML , OCaml , Haskell , F# , Fortress és Boo . A Nemerle nyelv ezt az algoritmust használja számos szükséges módosítással [2] .

A típuskövetkeztetési mechanizmus azon a képességen alapul, hogy egy kifejezés kiértékelésével kapott kifejezés típusára részben vagy egészben automatikusan következtethetünk. Mivel ezt a folyamatot szisztematikusan hajtják végre a programfordítás során, a fordító gyakran tud következtetni egy változó vagy függvény típusára anélkül, hogy kifejezetten meghatározná az objektumok típusát. Sok esetben az explicit típusdeklaráció elhagyható - ez megtehető meglehetősen egyszerű objektumok vagy egyszerű szintaxisú nyelvek esetén. Például a Haskell nyelvnek elég erős típuskövetkeztetési mechanizmusa van, így ebben a programozási nyelvben nem szükséges megadni a függvénytípusokat. A programozó kifejezetten megadhatja egy függvény típusát annak érdekében, hogy bizonyos adattípusokra korlátozza a használatát, vagy strukturáltabb forráskód formázáshoz.

Annak érdekében, hogy információt szerezzen a kifejezés típusának pontos megállapításához a kifejezés típusának explicit deklarációjának hiányában, a fordító vagy a benne foglalt részkifejezések típusainak (változók, függvények) explicit deklarációiból gyűjti össze ezeket az információkat. a vizsgált kifejezésben, vagy implicit információkat használ az atomi értékek típusairól. Egy ilyen algoritmus nem mindig segít meghatározni egy kifejezés típusát, különösen magasabb rendű függvények és meglehetősen összetett természetű parametrikus polimorfizmus esetén . Ezért összetett esetekben, amikor szükség van a kétértelműségek elkerülésére, ajánlatos kifejezetten megadni a kifejezések típusát.

Maga a tipizálási modell a kifejezéstípus-következtetési algoritmuson alapul, amelynek forrása a típusos λ-számításban használt kifejezéstípus-levezetési mechanizmus, amelyet 1958 -ban javasoltak H. Curry és R. Face. Továbbá Roger Hindley 1969 - ben kiterjesztette magát az algoritmust, és bebizonyította, hogy ez a kifejezés legáltalánosabb típusát eredményezi. 1978- ban Robin Milner R. Hindleytől függetlenül bebizonyította egy ekvivalens algoritmus tulajdonságait. És végül 1985 -ben Louis Damas végre megmutatta, hogy Milner algoritmusa kész, és használható polimorf típusokhoz. Ebben a tekintetben a Hindley-Milner algoritmust néha Damas-Milner algoritmusnak is nevezik .

A típusrendszert a Hindley-Milner-modell a következőképpen határozza meg:

A primitív típusok kifejezéstípusok. $v$
Az α paraméteres típusú változók kifejezéstípusok.
Ha és kifejezéstípusok, akkor a típus a kifejezés típusa. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\jobbra \sigma _{{2}}$
A szimbólum a kifejezések egy fajtája. $\bot$

Azok a kifejezések, amelyek típusai kiértékelve vannak, meglehetősen szabványos módon vannak meghatározva:

A konstansok kifejezések.
A változók kifejezések.
Ha és kifejezések, akkor ( ) egy kifejezés. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
Ha egy változó és egy kifejezés, akkor egy kifejezés. $v$ $e$ $\lambda ve$

Egy típust a típus példányának nevezünk, ha van valamilyen konverzió , például: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

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

Ebben az esetben általában azt feltételezik, hogy a típuskonverziókra korlátozások vonatkoznak, amelyek a következők: $\rho$

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

Maga a típuskövetkeztetési algoritmus két lépésből áll - egy egyenletrendszer létrehozásából, majd ezen egyenletek későbbi megoldásából.

Egyenletrendszer felépítése

Az egyenletrendszer felépítése a következő szabályokon alapul:

$\Gamma v=\tau$ - ha a kötés ben van . $v:\tau$ $\Gamma$
$\Gamma (ge)=\tau$ — ha , hol és . $\tau _{{1}}=\tau _{{2}}\jobbra \tau$ $\tau _{1}=\Gamma g$ $\tau _{2}=\Gamma e$
${\displaystyle \Gamma (\lambda ve)=\tau \rightarrow \tau _{e))$ - abban az esetben , ha , hol van a hozzáadott kötéssel . $\tau _{e}=\Gamma 'e$ $\gamma$ $\Gamma$ $v:\tau$

Ezekben a szabályokban a szimbólum a változók és típusaik közötti asszociációk halmaza: $\Gamma$

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

Egyenletrendszer megoldása

A megszerkesztett egyenletrendszer megoldása az egyesítő algoritmuson alapul . Ez egy meglehetősen egyszerű algoritmus. Van néhány függvény , amely egy típusegyenletet vesz be bemenetként, és olyan helyettesítést ad vissza, amely az egyenlet bal és jobb oldalát azonossá teszi ("egyesíti" őket). A helyettesítés egyszerűen a változótípusok magukra a típusokra vetítése. Az ilyen helyettesítéseket különféle módon lehet kiszámítani, amelyek a Hindley-Milner algoritmus konkrét megvalósításától függenek. $u$

Lásd még

Jegyzetek

Megjegyzések

↑ támogatás hozzáadva a Java SE 10 -hez

Források

↑ Andrew W. Appel. A Standard ML kritikája. — Princetoni Egyetem, a CS-TR-364-92 átdolgozott változata, 1992.
↑ Michal Moskal. Típus Következtetés halasztással . – 2005.

Linkek

A Hindley-Milner algoritmus megvalósítása Perlben
Roger Hindley archivált e-mail üzenete elmagyarázza a típuskövetkeztetés történetét
Michael Schwartzbach Polymorphic Type Inference , áttekintést ad a polimorf típusú következtetésről.
Funkcionális programok fő típussémái. A Damas és Milner-papír újraszedett példánya, amely leírta a hitelesség és a teljesség bizonyítékait.
Oktatóanyag és teljes megvalósítás a Standard ML-ben Az oktatóanyag tartalmazza a típusrendszerek logikai történetét, valamint az algoritmus részletes leírását a megvalósítás állapotában. Az eredeti Damas Milner-papír néhány tipográfiai hibáját kijavítottuk.
Alapvető típusellenőrző papír, Luca Cardelli, leírja az algoritmust, tartalmazza a Modula-2 megvalósítását
Hindley-Milner típusú következtetés megvalósítása a Scalában , Andrew Forrest (letöltve: 2009. július 30.)
A Hindley-Milner megvalósítása Perl 5-ben, Nikita Boriszov (nem elérhető link) . Hozzáférés dátuma: 2009. március 12. Az eredetiből archiválva : 2007. február 18. (határozatlan)
Mi az a Hindley-Milner? (és miért jó?) Magyarázza Hindley-Milner, példák a Scalában
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Hindley-Milner gépelési modell és példa a megvalósítására a Haskellben