A típusrendszer a programozási nyelvek szabályainak halmaza, amelyek tulajdonságokat, úgynevezett típusokat rendelnek a programot alkotó különféle konstrukciókhoz , például változókhoz , kifejezésekhez , függvényekhez vagy modulokhoz . A típusrendszer fő szerepe a programokban előforduló hibák számának csökkentése [1] azáltal, hogy interfészeket definiál a program különböző részei között, majd ellenőrzi ezen részek interakciójának konzisztenciáját. Ez az ellenőrzés történhet statikusan ( fordítási időben vagy dinamikusan ( futási időben ), vagy mindkettő kombinációjával.
Pierce szerint a típusrendszer egy eldönthető szintaktikai módszer bizonyos programviselkedések hiányának bizonyítására azáltal, hogy a konstrukciókat a számított értékek fajtája szerint osztályozza [2] .
Egy egyszerű típusú rendszerre láthatunk példát a C nyelvben . A C program részei függvénydefiníciókként vannak megírva . A függvények hívják egymást. Egy függvény interfésze meghatározza a függvény nevét és a törzsébe továbbított értékek listáját. A hívó függvény felteszi a meghívni kívánt függvény nevét és azon változók nevét, amelyek az átadni kívánt értékeket tartalmazzák. A program végrehajtása során az értékek átmeneti tárolóba kerülnek, majd a végrehajtás átkerül a hívott függvény törzsébe. A hívott függvénykód eléri és használja az értékeket. Ha egy függvény törzsében az utasításokat azzal a feltételezéssel írjuk, hogy egy egész értéket kell átadni nekik feldolgozásra, de a hívó kód lebegőpontos számot adott át, akkor a meghívott függvény rossz eredményt fog kiértékelni. A C fordító ellenőrzi az egyes átadott változókhoz definiált típusokat a hívott függvény interfészén az egyes változókhoz definiált típusokhoz képest. Ha a típusok nem egyeznek, a fordító fordítási idejű hibát generál.
Technikailag a típusrendszer minden számított értékhez típust rendel , majd a számítások sorrendjének nyomon követésével megpróbálja ellenőrizni vagy bizonyítani, hogy nincsenek típusillesztési hibák . Az adott típusú rendszer meg tudja határozni, hogy mi okozza a hibát, de általában az a cél, hogy megakadályozzák, hogy a paramétereik bizonyos tulajdonságait feltételező műveletek olyan paramétereket kapjanak, amelyeknél ezeknek a műveleteknek nincs értelme – ezzel megelőzve a logikai hibákat . Ezenkívül megakadályozza a memóriacím-hibákat .
A típusrendszereket általában a programozási nyelvek részeként határozzák meg, és beépítik azok értelmezőibe és fordítóiba. A nyelv típusrendszere azonban bővíthető speciális eszközökkel , amelyek további ellenőrzéseket végeznek a nyelv eredeti gépelési szintaxisa alapján.
A fordító statikus értéktípust is használhat a tárolás optimalizálására, és az adott értékre vonatkozó műveletek algoritmikus megvalósításának kiválasztására. Például sok C-fordítóban egy típust float 32 bit képvisel az IEEE egypontos lebegőpontos műveletekre vonatkozó specifikációja szerint . Ennek alapján az ilyen típusú értékekhez (összeadás, szorzás és egyéb műveletek) egy speciális mikroprocesszor utasításkészlet kerül felhasználásra.
A típusokra vonatkozó korlátozások száma és számítási módja határozza meg a nyelv tipizálását. Ezen túlmenően a típuspolimorfizmus esetén a nyelv minden típushoz megadhatja a változó specifikus algoritmusok működését is. A típusrendszerek tanulmányozása a típusok elmélete , bár a gyakorlatban egy programozási nyelv adott típusrendszere a számítógép architektúrájának jellemzőire, a fordítóprogram megvalósítására és a nyelv általános képére épül.
A típusrendszerek formális igazolása a típuselmélet . A programozási nyelv tartalmaz egy típusrendszert a fordítási időben vagy futási időben történő típusellenőrzés végrehajtására , amely kifejezett típusdeklarációkat igényel, vagy önmagában következtet rájuk. Mark Manasse a következőképpen fogalmazta meg a problémát [3] :
A típuselmélet által megoldott fő probléma a programok értelmességének biztosítása. A típuselmélettel kapcsolatos fő probléma az, hogy az értelmes programok esetleg nem úgy viselkednek, ahogyan azt szándékozták. Ennek a feszültségnek a következménye az erősebb típusú rendszerek keresése.
Eredeti szöveg (angol)[ showelrejt] A típuselmélet alapvető problémája annak biztosítása, hogy a programoknak legyen jelentése. A típuselmélet alapja az, hogy az értelmes programoknak nem lehet problémás jelentéseket tulajdonítani. A gazdagabb típusú rendszerekre való törekvés ebből a feszültségből adódik. – Mark Massey [3]A típus-hozzárendelési művelet, amelyet gépelésnek neveznek, jelentést ad bitkarakterláncoknak , például egy értéknek a számítógép memóriájában , vagy objektumoknak , például egy változónak . A számítógépnek nincs módja megkülönböztetni például a memóriában lévő címet egy kódutasítástól , vagy egy karaktert egy egész számtól vagy lebegőpontos számtól , mivel az ezeket a különböző jelentéseket képviselő bitsoroknak nincs olyan nyilvánvaló jellemzője, amely lehetővé tenné jelentésükkel kapcsolatos feltevések. A karakterláncokhoz típusbitek hozzárendelése biztosítja ezt az érthetőséget, így a programozható hardvert ebből a hardverből és szoftverből álló karakterrendszerré alakítja .
A típusellenőrzés és kényszerítés folyamata – típusellenőrzés vagy típusellenőrzés – elvégezhető akár fordítási időben statikus gépelés), akár futási időben (dinamikus gépelés). Köztes megoldások is lehetségesek (vö. szekvenciális gépelés ).
Ha a nyelvi specifikáció megköveteli a gépelési szabályok szigorú végrehajtását (vagyis bizonyos fokig csak azokat az automatikus típuskonverziókat engedje meg, amelyek nem veszítenek el információt), akkor egy ilyen nyelvet erősen beírtnak ; ) , egyébként gyengén beírtnak nevezzük . Ezek a kifejezések feltételesek, és nem használják formális indoklásban.
Egy nyelvet típusosnak nevezünk, ha az egyes műveletek specifikációi meghatározzák azokat az adattípusokat, amelyekre ez a művelet alkalmazható, ami azt jelenti, hogy más típusokra nem alkalmazható [4] . Például az " ez idézett szöveg " által képviselt adatok " " típusúak строка. A legtöbb programozási nyelvben nincs értelme egy szám karakterlánccal való elosztásának, és a legtöbb modern nyelv elutasítja az ilyen műveletet végrehajtó programot. Egyes nyelveken a program egy értelmetlen műveletet észlel a fordítás során ( statikus gépelés ), és a fordító elutasítja. Más esetekben a rendszer futás közben észleli ( dinamikus gépelés ), kivételt dobva ezzel .
A tipizált nyelvek speciális esetei az egytípusú nyelvek ( angol. egytípusú nyelv ), vagyis az egytípusú nyelvek. Ezek általában szkript- vagy jelölőnyelvek , mint például a REXX és az SGML , amelyek egyetlen adattípusa a karakterlánc, amely karakteres és numerikus adatok megjelenítésére is szolgál.
A típusolatlan nyelvek, ellentétben a tipizált nyelvekkel, lehetővé teszik, hogy bármilyen műveletet végrehajtsunk bármilyen adaton, amelyet bennük tetszőleges hosszúságú bitláncok képviselnek [4] . A legtöbb assembly nyelv gépeletlen . Példák a magas szintű típus nélküli nyelvekre: BCPL , BLISS , Forth , Refal .
A gyakorlatban kevés nyelv tekinthető tipizáltnak a típuselmélet szempontjából (minden művelet engedélyezése vagy elutasítása), a legtöbb modern nyelv csak bizonyos fokú gépeltséget kínál [4] . Sok ipari nyelv lehetővé teszi a típusrendszer megkerülését vagy megszakítását, a típusbiztonságot a programvégrehajtás finomabb ellenőrzése érdekében ( gépelési szójáték ).
A "polimorfizmus" kifejezés a kód azon képességére utal, hogy számos különböző típusú értéken futhat, vagy arra, hogy ugyanazon adatstruktúra különböző példányai különböző típusú elemeket tartalmazhatnak. Egyes típusrendszerek lehetővé teszik a polimorfizmust, hogy potenciálisan javítsa a kód újrafelhasználását : a polimorfizmussal rendelkező nyelvekben a programozóknak csak egyszer kell megvalósítaniuk az adatstruktúrákat, például egy listát vagy egy asszociatív tömböt , és nem kell egy implementációt kidolgozniuk minden egyes tervezett elemtípushoz. struktúrák tárolására. Emiatt egyes informatikusok néha „ általános programozásnak ” nevezik a polimorfizmus bizonyos formáinak használatát. A polimorfizmus indoklása a típuselmélet szempontjából gyakorlatilag megegyezik az absztrakció , a modularitás és esetenként az adataltípusosítással .
Számos speciális típusú rendszert fejlesztettek ki bizonyos feltételek mellett bizonyos adatokkal való használatra, valamint programok statikus elemzésére . Ezek többnyire a formális típuselmélet gondolatain alapulnak, és csak kutatási rendszerek részeként használatosak.
Az egzisztenciális típusok, azaz az egzisztenciális kvantor (egzisztenciális kvantor) által meghatározott típusok egy típusszintű beágyazási mechanizmus : ez egy összetett típus, amely valamilyen típus megvalósítását rejti összetételében.
Az egzisztenciális típus fogalmát gyakran használják a rekordtípus fogalmával együtt a modulok és az absztrakt adattípusok ábrázolására , mivel céljuk elválasztani a megvalósítást az interfésztől. Például egy típus T = ∃X { a: X; f: (X → int); }leír egy modulinterfészt (azonos aláírású modulcsaládokat), amelynek van egy ilyen típusú adatértéke, Xés egy függvény, amely egy pontosan ugyanolyan típusú paramétert vesz fel, Xés egy egész számot ad vissza. A megvalósítás eltérő lehet:
Mindkét típus az általánosabb egzisztenciális típus altípusa, Tés konkrétan megvalósított típusoknak felel meg, így bármely érték, amely valamelyikhez tartozik, a típushoz is tartozik T. Ha t típus értéke T, akkor t.f(t.a)átmegy a típusellenőrzésen, függetlenül attól, hogy melyik absztrakt típushoz tartozik X. Ez rugalmasságot biztosít az adott megvalósításhoz megfelelő típusok kiválasztásában, mivel a külső felhasználók csak az interfész (egzisztenciális) típusának értékeihez férnek hozzá, és el vannak szigetelve ezektől a változatoktól.
Általában a típuskonzisztencia-ellenőrző nem tudja meghatározni, hogy egy adott modul melyik egzisztenciális típushoz tartozik. A fenti példában a intT { a: int; f: (int → int); }típusa is lehet ∃X { a: X; f: (int → int); }. A legegyszerűbb megoldás, ha minden modulhoz kifejezetten megadjuk a benne szereplő típust, például:
Bár az absztrakt adattípusokat és modulokat már régóta használják a programozási nyelvekben, az egzisztenciális típusok formális modellje csak 1988 -ban készült el [5] . Az elmélet egy másodrendű típusos lambda-számítás , amely hasonló az F rendszerhez , de az univerzális kvantifikáció helyett egzisztenciális kvantifikációt alkalmaz .
Az egzisztenciális típusok kifejezetten a Haskell nyelv kísérleti kiterjesztéseként érhetők el , ahol egy speciális szintaxis, amely lehetővé teszi egy típusváltozó használatát egy algebrai típusdefinícióban anélkül, hogy áthelyezné egy típuskonstruktor aláírásába , azaz nem növelné az aritását . 6] . A Java nyelv az helyettesítő karakteren keresztül az egzisztenciális típusok korlátozott formáját biztosítja . A klasszikus ML - stílusú let-polimorfizmust megvalósító nyelvekben az egzisztenciális típusok szimulálhatók úgynevezett " típusindexelt értékek " [7] segítségével .
Sok statikus típusú rendszer, például a C és a Java, megköveteli a típusdeklarációt : a programozónak kifejezetten hozzá kell rendelnie egy adott típust minden változóhoz. Mások, mint például az ML - ben használt Hindley-Milner típusú rendszer és a Haskell , típuskövetkeztetést végeznek : a fordító a változók típusára következtet az alapján, hogy a programozó hogyan használja ezeket a változókat.
Például egy és az f(x,y)összeadást végrehajtó függvény esetében a fordító arra következtethet, hogy és számoknak kell lenniük – mivel az összeadási művelet csak számokhoz van definiálva. Ezért egy függvény meghívása valahol a programban a numerikustól eltérő paraméterekhez (például egy karakterlánchoz vagy egy listához) hibát jelez. xyxyf
A numerikus és karakterlánc-konstansok és kifejezések általában egy adott kontextusban fejeznek ki egy típust. Például egy kifejezés 3.14jelenthet valós számot , míg [1,2,3]lehet egész számok listája – általában egy tömb .
Általánosságban elmondható, hogy a típuskövetkeztetés akkor lehetséges, ha a típuselméletben alapvetően eldönthető . Sőt, még ha a következtetés eldönthetetlen is egy adott típusú elmélet esetében, gyakran sok valós program esetében lehetséges a következtetés. A Haskell típusú rendszer , amely a Hindley-Milner típusú rendszer egy változata, az Fω rendszer korlátozása az úgynevezett elsőrangú polimorf típusokra, amelyekre a következtetés eldönthető. Sok Haskell fordító tetszőleges rangú polimorfizmust ad kiterjesztésként, de ez eldönthetetlenné teszi a típuskövetkeztetést, ezért explicit típusdeklaráció szükséges. A típuskonzisztencia-ellenőrzés azonban továbbra is eldönthető, és az elsőrangú polimorfizmussal rendelkező programok esetében a típusok továbbra is származtathatók.
Egyes nyelvek, mint például a C# , egységes típusrendszerrel rendelkeznek [8] . Ez azt jelenti, hogy a nyelv minden típusa, a primitívekig , egyetlen gyökérobjektumtól öröklődik (C# esetén az osztályból Object). A Java -nak számos primitív típusa van, amelyek nem objektumok. Ezek mellett a Java wrapper objektumtípusokat is biztosít, így a fejlesztő saját belátása szerint használhatja a primitív vagy objektumtípusokat.
A típuskonzisztencia-ellenőrző mechanizmus egy statikusan beírt nyelvben ellenőrzi, hogy bármely kifejezés megfelel-e a kontextus által elvárt típusnak, amelyben előfordul. Például egy típus- hozzárendelési utasításban a kifejezéshez kikövetkeztetett típusnak meg kell egyeznie a változóhoz deklarált vagy kikövetkeztetett típussal . A megfelelőségi jelölés, az úgynevezett kompatibilitás , minden nyelvre jellemző. x := eex
Ha a eés xazonos típusúak, és ehhez a típushoz engedélyezett a hozzárendelés, akkor a kifejezés legális. Ezért a legegyszerűbb típusú rendszerekben a két típus kompatibilitásának kérdése leegyszerűsödik egyenlőségük ( ekvivalenciájuk ) kérdésére. A különböző nyelvek azonban eltérő kritériumokkal rendelkeznek a két kifejezés típuskompatibilitásának meghatározására. Ezek az ekvivalenciaelméletek két véglet között változnak: strukturális típusú rendszerek , amelyekben két típus ekvivalens, ha egy érték ugyanazt a belső szerkezetét írják le; és nominatív típusú rendszerek , amelyekben a szintaktikailag különböző típusok soha nem ekvivalensek ( vagyis két típus csak akkor egyenlő, ha az azonosítóik azonosak) .
altípusú nyelveken a kompatibilitási szabályok bonyolultabbak. Például, ha egy altípusa , akkor a típus értéke használható olyan környezetben, amely típus értéket vár , még akkor is, ha ennek ellenkezője nem igaz. Az ekvivalenciához hasonlóan az altípus-kapcsolatok nyelvenként változnak, és a szabályoknak számos változata lehetséges. A paraméteres vagy szituációs polimorfizmus jelenléte egy nyelvben szintén befolyásolhatja a típuskompatibilitást. ABAB
Egyes programozók a statikus típusú rendszereket részesítik előnyben, mások a dinamikus rendszereket . A statikusan beírt nyelvek jeltípus-konzisztencia-hibák fordítási időben , hatékonyabban futtatható kódot generálhatnak, és az ilyen nyelvek esetében megvalósítható a relevánsabb befejezés az IDE- ben . A dinamikus gépelés hívei azzal érvelnek, hogy ezek alkalmasabbak a gyors prototípuskészítésre , és hogy a típusillesztési hibák csak töredékét képezik a programok lehetséges hibáinak [9] [10] . Másrészt a statikusan beírt nyelvekben általában nincs szükség explicit típusdeklarációra, ha a nyelv támogatja a típuskövetkeztetést , és egyes dinamikusan tipizált nyelvek futásidejű optimalizálást hajtanak végre [11] [12] , gyakran részleges típus használatával. következtetés [13] .
| Adattípusok | |
|---|---|
| Értelmezhetetlen | |
| Numerikus | |
| Szöveg | |
| Referencia | |
| Összetett | |
| absztrakt | |
| Egyéb | |
| Kapcsolódó témák | |