Ugrás a tartalomhoz

Típuskövetkeztetés

A Wikipédiából, a szabad enciklopédiából

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

[szerkesztés]

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 , , és és a független kifejezések, és típusú természetes számok. Hagyományosan a kifejezést kettőspont követi, és annak típusa, mint pl . Ez azt jelenti, hogy a -es érték típusa . Ezt az űrlapot új nevek deklarálására is használják, pl , 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 -es kifejezés lehet 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ármoztatni. 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 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álltal 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

[szerkeszté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:

  1. 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.
  2. 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.
  3. _ : 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

[szerkeszté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

[szerkesztés]

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

[szerkesztés]

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

Típuskövetkeztetés a természetes nyelvekre

[szerkesztés]

A típuskövetkeztetési algoritmusokat használták a természetes nyelvek, valamint a programozási nyelvek elemzésére.[12] [13] [14] A típuskövetkeztetési algoritmusokat néhány nyelvtani indukciós[15] [16] és kényszer alapú nyelvtani rendszerben is használják a természetes nyelvek számára.[17]

Hivatkozások

[szerkesztés]
  1. cartermp: Type Inference - F# (amerikai angol nyelven). docs.microsoft.com . (Hozzáférés: 2020. november 21.)
  2. Inference · The Julia Language. docs.julialang.org . (Hozzáférés: 2020. november 21.)
  3. Type Inference. Scala Documentation . (Hozzáférés: 2020. november 21.)
  4. Documentation - Type Inference (angol nyelven). www.typescriptlang.org . (Hozzáférés: 2020. november 21.)
  5. The Dart type system. dart.dev . (Hozzáférés: 2020. november 21.)
  6. Bryan O'Sullivan. Chapter 25. Profiling and optimization, Real World Haskell. O'Reilly (2008) 
  7. Talpin, Jean-Pierre, and Pierre Jouvelot. "Polymorphic type, region and effect inference." Journal of functional programming 2.3 (1992): 245-271.
  8. Hassan, Mostafa. MaxSMT-Based Type Inference for Python 3, Computer Aided Verification, Lecture Notes in Computer Science, 12–19. o.. DOI: 10.1007/978-3-319-96142-2_2 (2018). ISBN 978-3-319-96141-5 
  9. Damas & Milner (1982), POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM
  10. Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences 17 (3): 348–375, DOI 10.1016/0022-0000(78)90014-4
  11. Damas, Luis & Milner, Robin (1982), "Principal type-schemes for functional programs", POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, pp. 207–212, <http://groups.csail.mit.edu/pag/6.883/readings/p207-damas.pdf>
  12. Center, Artificiał Intelligence. Parsing and type inference for natural and computer languages Archiválva 2012. július 4-i dátummal a Wayback Machine-ben. Diss. Stanford University, 1989.
  13. Emele, Martin C., and Rémi Zajac. "Typed unification grammars Archiválva 2018. február 5-i dátummal a Wayback Machine-ben." Proceedings of the 13th conference on Computational linguistics-Volume 3. Association for Computational Linguistics, 1990.
  14. Pareschi, Remo. "Type-driven natural language analysis." (1988).
  15. Fisher, Kathleen, et al. "Fisher, Kathleen, et al. "From dirt to shovels: fully automatic tool generation from ad hoc data." ACM SIGPLAN Notices. Vol. 43. No. 1. ACM, 2008." ACM SIGPLAN Notices. Vol. 43. No. 1. ACM, 2008.
  16. Lappin (2007). „Machine learning theory and practice as a source of insight into universal grammar”. Journal of Linguistics 43 (2), 393–427. o. DOI:10.1017/s0022226707004628.  
  17. Stuart M. Shieber. Constraint-based Grammar Formalisms: Parsing and Type Inference for Natural and Computer Languages. MIT Press (1992). ISBN 978-0-262-19324-5 

Fordítás

[szerkesztés]

Ez a szócikk részben vagy egészben a Type inference című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

További információk

[szerkesztés]