Típusk?vetkeztetés

A típusk?vetkeztetés a kifejezés típusának automatikus felismerésére vonatkozik egy formális nyelven. Ide tartoznak a programozási nyelvek és a matematikai típusú rendszerek, de a számítástechnika és a nyelvészet egyes ágaiba a természetes nyelvek is beletartoznak.

M?szaki magyarázat

A legáltalánosabb nézetben szerepl? típusok társíthatók olyan kiválasztott felhasználásokhoz, amelyek javasolják és korlátozzák az adott típusú objektumok lehetséges m?veleteit. A nyelvben számos f?név határozza meg ezt a használatot. Például a póráz szónak más célja van, mint a sor szónak. Ha valamit asztal táblának hívunk, annak jelentése eltér a t?zifának nevezhet? asztaltól, annak ellenére, hogy nagyjából azonos lehet. Noha anyagi tulajdonságaik miatt ezek a dolgok bizonyos célokra hasznosak, mégis sajátos nevekkel rendelkeznek. Ez kül?n?sen igaz az absztrakt területeken, nevezetesen a matematikában és az informatikában, ahol az anyag végül csak bitek vagy formulák.

A felesleges, de gazdaságilag lehetséges felhasználások kizárása érdekében a típus fogalmát számos változatban definiálják és alkalmazzák. A matematikában Russell paradoxon hozta létre a típuselmélet korai verzióit. A programozási nyelvekben egyik tipikus példa a "típushiba", például a számítógép olyan ?sszeszámolásra utasít, amely nem szám. Bár megvalósítható, az eredmények már nem lesznek értelmezhet?ek, és súlyos k?vetkezményekkel járhatnak az egész folyamatra nézve.

A típusokban a kifejezések a típusokhoz viszonyulnak. Például a $4$ , $2+2$ , és $2\cdot 2$ és a $2\cdot 2$ független kifejezések, és $\mathrm {nat}$ típusú természetes számok. Hagyományosan a kifejezést kett?spont k?veti, és annak típusa, mint pl $2:\mathrm {nat}$ . Ez azt jelenti, hogy a $2$ -es érték típusa $\mathrm {nat}$ . Ezt az ?rlapot új nevek deklarálására is használják, pl $n:\mathrm {nat}$ , hasonlóan ahhoz, hogy egy "Decker nyomozó" szavakkal új karaktert mutassanak be a jelenetben.

Ellentétben azokkal a t?rténetekkel, amelyekben a szimbólumok lassan bontakoznak ki, a hivatalos nyelvi objektumokat általában kezdett?l fogva típusuk szerint kell meghatározni. Ezenkívül, ha a feltételek nem egyértelm?ek, a típus megadására lehet szükség a cél megadásához. Például a $2$ -es kifejezés lehet $\mathrm {nat}$ típus, de racionális vagy valós számként, vagy akár egyszer? sz?vegként is olvasható.

Ennek k?vetkezményeként a programok vagy eljárások túlterhel?dnek a típusokkal, amennyiben azokat a kontextusból kell származtatni. Ezt úgy lehet elérni, hogy ?sszegy?jtjük a nem típusú kifejezések használatát (beleértve a meghatározatlan neveket is). Például, ha $n+2$ meghatározatlan nevet használ a kifejezésben, arra k?vetkeztethet, hogy n legalább egy szám. A típus kifejezésb?l és ?sszefüggéséb?l t?rtén? levezetésének folyamata a típus k?vetkeztetése.

általánosságban elmondható, hogy nem csak az objektumoknak, hanem az eljárásoknak is vannak típusaik, amelyek használatukkal k?nnyen bevezethet?k. A Star Trek t?rténetéhez egy ilyen ismeretlen eseményt "lehet k?zvetíteni", de hivatalosan soha nem indították el, csak hogy a t?rténet folytatódhasson. Mindazonáltal a típusára (szállítására) azonban a t?rténtekb?l lehet k?vetkeztetni. Ezenkívül objektumok és tevékenységek felépíthet?k a részeikb?l. Ebben az esetben a típusk?vetkeztetés nemcsak bonyolultabbá válik, hanem hasznosabbá is válik, mert lehet?vé teszi, hogy teljes leírást gy?jts?n az ?sszeszerelési jelenetben mindenr?l, ugyanakkor képes legyen észlelni az ?sszeütk?zéseket vagy a nem szándékos felhasználást.

Típusellen?rzés vs típusk?vetkeztetés

A gépelésnél az E kifejezést szembe állítják a T-vel, és T-t hivatalosan E: T-nek írják. A gépelés általában csak bizonyos ?sszefüggésekben értelmes, itt ezt kihagyjuk.

Ebben a k?rnyezetben a k?vetkez? kérdések kül?n?sen érdekesek:

E : T? Ebben az esetben E-kifejezést és T-t is megadunk. Most E valóban T? Ez a forgatók?nyv típusellen?rzés néven ismert.
E : _? Itt csak a kifejezés ismert. Ha van mód az E típusának levezetésére, akkor elvégeztük a típusk?vetkeztetést.
_ : T? Fordítva. Csak egy típust adva, van-e kifejezés rá, vagy a típusnak nincsenek értékei? Van-e példa T-re?

Az egyszer?, tipizált lambda számításokhoz mindhárom probléma meghatározható. Amikor kifejez?bb típusok megengedettek, a helyzet kevésbé kényelmes.

A típusok olyan jellemz?k, amelyek jelen vannak néhány er?sen statikusan tipizált nyelvben. Ez kifejezetten gyakran jellemz? a funkcionális programozási nyelvekre általában. Egyes nyelvek k?zé típusú k?vetkeztetést tartalmaznia C ++ 11, C # (3.0 verziótól kezd?d?en), Chapel, Clean, Crystal, D, F#,^[1] FreeBASIC, Go, Haskell, Java (verziótól kezd?d?en 10),Julia,^[2] Kotlin, ML, Nim, OCaml, Opa, RPython, Rust, Scala,^[3] Swift, TypeScript,^[4] Vala, Dart,^[5] és Visual Basic (kezdve a 9.0 verziótól). T?bbségük a típusk?vetkeztetés egyszer? formáját alkalmazza; a Hindley-Milner típusú rendszer teljesebb típusú k?vetkeztetésre képes. A típusok kik?vetkeztetésének képessége sok programozási feladatot megk?nnyít, így a programozó szabadon hagyhatja a típusjegyzeteket, mik?zben engedélyezi a típusellen?rzést.

Bizonyos programozási nyelvekben minden értéknek van egy adattípusa, amelyet kifejezetten deklaráltak a fordítás idején, ami korlátozza azokat az értékeket, amelyeket egy adott kifejezés futás k?zben kaphat. Ami leginkább ellentmondásossá teszi a fordítási id? és a futási id? k?zti kül?nbséget, az a just-in-time fordítás. Azonban, t?rténelmileg, ha az érték típusa csak futás k?zben ismert, akkor ezeket a nyelveket dinamikusan gépelik. Eltér? nyelvekben a kifejezés típusa csak fordításkor ismert; az ilyen nyelvek tipizálása statikusan t?rténik. A legt?bb statikusan tipizált nyelvben a függvények és a helyi változók bemeneti és kimeneti típusait általában típusjegyzetekkel adják meg. Például a C-ben :

int add_one(int x) {
    int result; /* egész eredmény deklarálása */

    result = x + 1;
    return result;
}

Ennek a függvénydefinícinak a signature-je az int add_one(int x) kijelenti, hogy az add_one egy olyan függvény, amely egy argumentumot kér be, egész számot és visszatér egész számmal. int result; kijelenti, hogy a helyi változó result egész szám. A hipotetikus nyelvben, amely támogatja a típusk?vetkeztetést, helyette ilyen kódot írhat:

add_one(x) {
    var result;  /* inferred-type variable result */
    var result2; /* inferred-type variable result #2 */

    result = x + 1;
    result2 = x + 1.0;  /* ez a sor nem fog m?k?dni (a javasolt nyelven) */
    return result;
}

Ez megegyezik a Dart nyelven írt kóddal, de további korlátozások vonatkoznak rá, az alábbiakban leírtak szerint. A fordítás során az ?sszes változó típusára k?vetkeztetni lehet. A fenti példában a fordító arra a k?vetkeztetésre jutott, hogy aresult-nak és azx-nek egész típusúnak kell lennie, mivel az 1. konstans típusú egész szám, tehát az add_one egy int -> int függvény. Az result2 változót t?rvényszer?en nem használják, így nem lesz típusa.

Az utolsó példát író fiktív nyelvben a fordító azt feltételezte, hogy hacsak másképp nem jelezzük, a + két egész számot elfogad és egy egész számot ad vissza. (Például az OCaml.így m?k?dik.) Ebb?l a k?vetkeztetéstípusból arra k?vetkeztethetünk, hogy az x + 1típusa egész szám, ami azt jelenti, hogy a result egész szám, tehát az add_onevisszatérési értéke egész szám. , Mivel a +megk?veteli, hogy a két paraméter azonos típusú legyen, x-nek egész számnak kell lennie, ezért az add_oneegész számot fogad el paraméterként.

A k?vetkez? sorokban azonban az result2 kiszámítása 1.0 tizedes lebeg?pontos m?velet hozzáadásával t?rténik, ami konfliktusokhoz vezet az x egész és lebeg?pontos kifejezésekben való használatával. Ebben az esetben a helyes típusú k?vetkeztetési algoritmus 1958 óta ismert és 1982 óta javított. áttekintette a korábbi k?vetkeztetéseket, és a kezdetekt?l fogva a leggyakoribb típust használta: ebben az esetben lebeg?pontos típusról van szó. Ennek azonban kedvez?tlen k?vetkezményei lehetnek, például a lebeg?pontos számok használata olyan pontossági problémákat okozhat, amelyek kezdett?l fogva nem egész számok.

Azonban általában elfajzott típus-k?vetkeztetési algoritmust alkalmaznak, amely esetben nem térhet vissza, hanem hibaüzenetet generál. Ez a viselkedés el?ny?sebb lehet, mert a típus k?vetkeztetése nem mindig lehet algoritmikusan semleges, amint azt az el?z? lebeg?pontos pontossági probléma mutatja.

A k?ztes általánosság algoritmusa implicit módon lebeg?pontos változóvá nyilvánítja a result2 -t, és az ?sszeadás implicit módon átalakítja x értékét lebeg?ponttá. Ez az eset akkor lehet megfelel?, ha soha nem adnak lebeg?pontos argumentumot a hívó kontextusok. Egy ilyen szituáció megmutatja a kül?nbséget típusú k?vetkeztetés, amely nem jár típuskonverzióval, és implicit típuskonverzióvalt, amely az adatokat egy másik adattípusra konvertálásra kényszeríti. általában nincs megk?tés.

Végül a komplex típusú k?vetkeztetési algoritmusok jelent?s hátránya, hogy az ebb?l ered? k?vetkeztetéstípus felbontása az emberek számára nem nyilvánvaló (nem lehetséges a visszalépés miatt), ami káros lehet, mert a kód f?leg ember számára érthet?.

A just-in-time nemrégiben megjelent lehet?sége olyan vegyes módszereket tesz lehet?vé, amikor a fordításkor ismertek a kül?nb?z? hívók?rnyezetek által biztosított paramétertípusok, és ugyanannak a függvénynek nagyszámú lefordított változata generálható. Ezután minden lefordított verzió optimalizálható kül?nb?z? típusú típusokhoz. Például a JIT-fordítás lehet?vé teszi az add_one: legalább két lefordított változatának megadását:

Olyan verzió, amely elfogad egy egész számot és implicit típusú konverziót használ.

Olyan verzió, amely lebeg?pontos számot fogad be bevitelként, és lebeg?pontos utasításokat használ végig.

Technikai leírás

A típusk?vetkeztetés az a képesség, hogy a kifejezés típusát részben vagy egészben a fordítás idején levezethetjük. A fordító általában képes egyértelm? k?vetkeztetéstípus megadása nélkül kik?vetkeztetni a változó típusát vagy a függvény típusaláírását. Sok esetben, ha a típusú k?vetkeztetési rendszer elég robusztus, vagy a program vagy a nyelv elég egyszer?, a típusjegyzeteket teljesen el lehet hagyni.

A kifejezés típusának meghatározásához szükséges információk megszerzése érdekében a fordító ?sszegy?jti ezeket az információkat, és leegyszer?síti az alkifejezéséhez hozzáadott típusjegyzeteket, vagy hallgatólagosan megérti a kül?nb?z? atomértékek típusait (például igaz : logikai; 42 : egész szám; 3.14159 : valódi; stb.). Annak felismerésével, hogy a kifejezések implicit módon beírható atomértékekre redukálódhatnak, a k?vetkeztetett nyelv fordítója teljesen megírhatja a programot anélkül, hogy tipusjegyzetekre lenne szüksége.

A magasabb szint? programozás és a polimorfizmus bonyolult formáiban a fordító nem mindig k?vetkeztethet ennyire, és a finomításhoz id?nként tipikus kommentárokra van szükség. Például a polimorf rekurzióval kapcsolatos típusú k?vetkeztetéseket nem lehet cáfolni. Ezenkívül azzal, hogy a fordítót arra kényszeríti, hogy a k?vetkeztetett típusnál specifikusabb (gyorsabb / kisebb) típust használjon, explicit típusú kommentárokkal használhatja a kód optimalizálását.^[6]

A típusú k?vetkeztetés egyes módszerei a kényszer-elégedettségen^{[halott link]}^[7] vagy az elégedettség modulo-elméleteken^{[halott link]} alapulnak.^[8]

Példaként, a Haskell funkció map v egy listának minden eleme egy funkcióra vonatkozik, és lehet meghatározni:

map f [] = []
map f (first:rest) = f first : map f rest

A típusk?vetkeztetés a map funkció a k?vetkez?képpen jár el. A map két argumentum funkciója, ezért típusa a → b → c alakú. Haskellben a [] és (first:rest) mindig egyeznek a minták a listákkal, tehát a második argumentumnak mindig listatípusnak kell lennie: b = [d] d típus esetében. Els? argomentum az f alkalmazzuk a first az argumentumra, ami mindenképpen d típusúnak kell lennie, amely megegyezik a lista argumentum típusával, tehát f :: d → e ( :: jelentése "a típusa") bizonyos e típusoknál. A visszatérési értéke map f, végezetük, felsorolja azt, amit f produkál, tehát [e]. Ha megfelel?en ?sszerakjuk a részeket, map :: (d → e) → [d] → [e]. A típusváltozókban nincs semmi kül?n?s, ezért megjegyezhetjük ?ket

map :: (a → b) → [a] → [b]

Kiderült, hogy ez is a leggyakoribb típus, mert nincsenek további korlátozások. Mivel a mapk?vetkeztetett típusa paraméter polimorf, az f paramétereinek és eredményeinek típusa nem k?vetkeztetett, hanem típusváltozóként fenntartott, így a leképezés kül?nféle típusú függvényekre és listákra alkalmazható, mindaddig, amíg a tényleges típus minden alkalommal megmérk?zik.

Hindley – Milner típusú k?vetkeztetési algoritmus

Az eredetileg a típusú k?vetkeztetések végrehajtására használt algoritmust ma informálisan Hindley-Milner algoritmusnak nevezik, bár az algoritmust Damasknak, illetve Milnernek kell tulajdonítani.^[9]

Ennek az algoritmusnak az eredete Haskell Curry és Robert Feys által 1958-ban kitalált egyszer? típusú lambda számítási érvelési algoritmus. 1969-ben J. Roger Hindley kiterjesztette ezt a munkát, és bebizonyította, hogy algoritmusuk mindig a leggyakoribb típust vezeti le. 1978-ban Robin Milner,^[10] Hindley munkájától függetlenül, egy ekvivalens algoritmust, a W algoritmust biztosított. Luis Damas^[11] végül bebizonyította, hogy Milner algoritmusa 1982-ben elkészült, és kiterjesztette polimorf referenciákkal rendelkez? rendszerek támogatására.

A legáltalánosabb típus használatának mellékhatásai

A tervezés szerint a típusk?vetkeztetés, kül?n?sen korrekt (visszalépési) típusú k?vetkeztetés a leggyakoribb típusok használatát foglalja magában, de ennek k?vetkezményei lehetnek, mert az általánosabb típusok nem mindig algoritmus semlegesek. A tipikus helyzet:

a lebeg?pontos egész szám általános típusának tekinthet?, míg a lebeg?pontos pontossági kérdéseket fog bevezetni
a variáns / dinamikus típusok más típusok általános típusának tekinthet?k, amelyek bevetési szabályokat és ?sszehasonlítást vezetnek be, amelyek eltér?ek lehetnek, például az ilyen típusok a ?+” operátort használják mind numerikus kiegészítésekhez, mind karakterláncok ?sszef?zéséhez, de a m?veletet milyen inkább dinamikusan, mint statikusan határozzák meg