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 $n a t$ típusú természetes számok. Hagyományosan a kifejezést kettőspont követi, és annak típusa, mint pl $2 : n a t$ . Ez azt jelenti, hogy a $2$ -es érték típusa $n a t$ . Ezt az űrlapot új nevek deklarálására is használják, pl $n : n a t$ , 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 $n a t$ 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 Sablon:Halott link^[7] vagy az elégedettség modulo-elméleteken Sablon: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