Typový systém je sada pravidel v programovacích jazycích , která přiřazují vlastnosti, nazývané typy , různým konstrukcím tvořícím program , jako jsou proměnné , výrazy , funkce nebo moduly . Hlavní úlohou typového systému je snížit počet chyb v programech [1] definováním rozhraní mezi různými částmi programu a následnou kontrolou konzistence interakce těchto částí. Tato kontrola může probíhat staticky ( v době kompilace ) nebo dynamicky ( za běhu) a také být kombinací obou.
Podle Pierce je typový systém rozhodnoutelnou syntaktickou metodou dokazování nepřítomnosti určitého chování programu klasifikací konstrukcí podle druhů vypočítaných hodnot [2] .
Příklad jednoduchého typového systému lze vidět v jazyce C . Části programu C jsou zapsány jako definice funkcí . Funkce se navzájem volají. Rozhraní funkce určuje název funkce a seznam hodnot, které jsou předány do jejího těla. Volající funkce postuluje název funkce, kterou chce volat, a názvy proměnných, které obsahují hodnoty, které chce předat. Během provádění programu jsou hodnoty umístěny do dočasného úložiště a poté je provádění předáno do těla volané funkce. Volaný funkční kód přistupuje k hodnotám a používá je. Pokud jsou instrukce v těle funkce psány s předpokladem, že jim má být ke zpracování předána celočíselná hodnota, ale volající kód předal číslo s plovoucí desetinnou čárkou, pak volaná funkce vyhodnotí špatný výsledek. Kompilátor jazyka C kontroluje typy definované pro každou proměnnou předávanou proti typům definovaným pro každou proměnnou v rozhraní volané funkce. Pokud se typy neshodují, kompilátor vygeneruje chybu při kompilaci.
Technicky vzato, typový systém přiřadí typ každé vypočítané hodnotě a poté sledováním posloupnosti těchto výpočtů se pokusí zkontrolovat nebo prokázat, že neexistují žádné chyby shody typu . Specifický typový systém může určit, co chybu způsobuje, ale obvykle je cílem zabránit operacím, které přebírají určité vlastnosti svých parametrů, v přijímání parametrů, pro které tyto operace nedávají smysl – předcházet logickým chybám . Kromě toho také zabraňuje chybám adresy paměti .
Typové systémy jsou obvykle definovány jako součást programovacích jazyků a zabudovány do jejich interpretů a kompilátorů. Typový systém jazyka však lze rozšířit o speciální nástroje , které provádějí dodatečné kontroly na základě původní syntaxe psaní v jazyce.
Kompilátor může také použít typ statické hodnoty k optimalizaci úložiště a k výběru algoritmické implementace operací s touto hodnotou. Například v mnoha kompilátorech jazyka C je typ float reprezentován 32 bity podle specifikace IEEE pro operace s plovoucí desetinnou čárkou s jednoduchou přesností . Na základě toho bude pro hodnoty tohoto typu (sčítání, násobení a další operace) použita speciální sada instrukcí mikroprocesoru .
Počet omezení uvalených na typy a způsob jejich výpočtu určují typizaci jazyka. Navíc v případě typového polymorfismu může jazyk také specifikovat pro každý typ operace různých specifických algoritmů. Studium typových systémů je teorií typů , i když v praxi je konkrétní typový systém programovacího jazyka založen na vlastnostech počítačové architektury, implementaci kompilátoru a obecné představě jazyka.
Formálním odůvodněním pro typové systémy je teorie typů . Programovací jazyk zahrnuje typový systém pro provádění kontroly typu v době kompilace nebo za běhu , vyžaduje explicitní deklarace typu nebo je sám odvozuje . Mark Manasse formuloval problém následovně [3] :
Hlavním problémem, který teorie typů řeší, je zajistit, aby programy dávaly smysl. Hlavním problémem teorie typů je, že smysluplné programy se nemusí chovat tak, jak bylo zamýšleno. Důsledkem tohoto napětí je hledání výkonnějších typových systémů.
Původní text (anglicky)[ zobrazitskrýt] Základním problémem, který teorie typů řeší, je zajistit, aby programy měly smysl. Základem teorie typů je to, že smysluplným programům nemusí být připisovány problémové významy. Z tohoto napětí vyplývá hledání systémů bohatších typů. — Mark Massey [3]Operace přiřazení typu, nazývaná psaní, dává význam řetězcům bitů , jako je hodnota v paměti počítače , nebo objektům , jako je proměnná . Počítač nemá žádný způsob, jak rozlišit například adresu v paměti od instrukce kódu nebo znak od celého čísla nebo čísla s plovoucí desetinnou čárkou , protože bitové řetězce představující tyto různé významy nemají žádné zjevné vlastnosti, které by umožňovaly domněnky o jejich významu. Přiřazení bitů typu řetězcům poskytuje tuto srozumitelnost, čímž se z programovatelného hardwaru stane znakový systém sestávající z tohoto hardwaru a softwaru.
Proces kontroly typu a omezení – kontrola typu nebo kontrola typu – lze provádět buď v době kompilace statické typování) nebo za běhu (dynamické psaní). Jsou možná i přechodná řešení (srov . sekvenční psaní ).
Pokud specifikace jazyka vyžaduje, aby byla pravidla pro psaní striktně implementována (to znamená, že do té či oné míry povolují pouze ty automatické převody typů, které neztrácejí informace), nazývá se takový jazyk silně typovaný ; ), jinak slabě typovaný . Tyto termíny jsou podmíněné a nepoužívají se ve formálních odůvodněních.
Jazyk se nazývá typovaný, pokud specifikace každé operace definuje datové typy, na které lze tuto operaci aplikovat, z čehož vyplývá její nepoužitelnost na jiné typy [4] . Například data, která představuje „ tento citovaný text “ , jsou typu „ строка“. Ve většině programovacích jazyků nedává dělení čísla řetězcem smysl a většina moderních jazyků odmítne program, který se pokouší provést takovou operaci. V některých jazycích bude během kompilace ( statické typování ) detekována nesmyslná operace a kompilátorem odmítnuta. V jiných bude detekován za běhu ( dynamické psaní ) a vyvolá výjimku .
Speciálním případem typovaných jazyků jsou jazyky s jedním typem ( angl. single-type language ), tedy jazyky s jedním typem. Obvykle se jedná o skriptovací nebo značkovací jazyky , jako je REXX a SGML , jejichž jediným datovým typem je znakový řetězec, který se používá k reprezentaci znakových i číselných dat.
Netypové jazyky na rozdíl od typových umožňují provádět libovolnou operaci s libovolnými daty, která jsou v nich reprezentována řetězci bitů libovolné délky [4] . Většina jazyků assembleru je netypizovaná . Příklady netypizovaných jazyků na vysoké úrovni jsou BCPL , BLISS , Forth , Refal .
V praxi lze jen málo jazyků považovat za typované z hlediska teorie typů (povolení nebo odmítnutí všech operací), většina moderních jazyků nabízí pouze určitý stupeň typizace [4] . Mnoho průmyslových jazyků poskytuje možnost obejít nebo prolomit typový systém, čímž vymění bezpečnost typu za jemnější kontrolu nad prováděním programu ( psací hříčka ).
Termín „polymorfismus“ označuje schopnost kódu běžet na hodnotách mnoha různých typů nebo schopnost různých instancí stejné datové struktury obsahovat prvky různých typů. Některé typy systémů umožňují polymorfismus potenciálně zlepšit opětovné použití kódu : v jazycích s polymorfismem potřebují programátoři pouze jednou implementovat datové struktury, jako je seznam nebo asociativní pole , a nemusí vyvíjet jednu implementaci pro každý typ prvku, který plánují. skladovat.struktury. Z tohoto důvodu někteří počítačoví vědci někdy označují použití určitých forem polymorfismu jako „ generické programování “. Opodstatnění pro polymorfismus z hlediska teorie typů jsou prakticky stejná jako pro abstrakci , modularitu a v některých případech podtypování dat .
Byla vyvinuta řada systémů speciálního typu pro použití za určitých podmínek s určitými daty a také pro statickou analýzu programů. Z velké části vycházejí z myšlenek formální teorie typů a používají se pouze jako součást výzkumných systémů.
Existenciální typy, tj. typy definované existenčním kvantifikátorem (existenčním kvantifikátorem) , jsou mechanismem zapouzdření na úrovni typu : jde o složený typ, který ve svém složení skrývá implementaci nějakého typu.
Pojem existenciálního typu se často používá ve spojení s pojmem typ záznamu k reprezentaci modulů a abstraktních datových typů kvůli jejich účelu oddělit implementaci od rozhraní. Typ například T = ∃X { a: X; f: (X → int); }popisuje rozhraní modulu (rodiny modulů se stejnou signaturou), které má datovou hodnotu typu Xa funkci, která přebírá parametr přesně stejného typu Xa vrací celé číslo. Implementace může být různá:
Oba typy jsou podtypy obecnějšího existenčního typu Ta odpovídají konkrétně implementovaným typům, takže jakákoli hodnota, která patří k některému z nich, patří také do typu T. Pokud t je hodnota typu T, pak t.f(t.a)projde kontrolou typu bez ohledu na to, ke kterému abstraktnímu typu patří X. To poskytuje flexibilitu při výběru typů, které jsou vhodné pro konkrétní implementaci, protože externí uživatelé přistupují pouze k hodnotám typu rozhraní (existenciálního) a jsou od těchto variací izolováni.
Obecně platí, že kontrola typové konzistence nemůže určit, ke kterému existenčnímu typu daný modul patří. Ve výše uvedeném příkladu intT { a: int; f: (int → int); }může mít také typ ∃X { a: X; f: (int → int); }. Nejjednodušším řešením je explicitně specifikovat pro každý modul předpokládaný typ v něm, například:
Přestože abstraktní datové typy a moduly byly v programovacích jazycích používány již dlouhou dobu, formální model existenciálních typů byl sestaven až v roce 1988 [5] . Teorie je druhořadý typovaný lambda počet podobný systému F , ale s existenční kvantifikací namísto univerzální kvantifikace .
Existenční typy jsou explicitně dostupné jako experimentální rozšíření jazyka Haskell , kde se jedná o speciální syntaxi, která vám umožňuje používat typovou proměnnou v algebraické definici typu , aniž byste ji přesunuli do podpisu typového konstruktoru , tj. bez zvýšení její arity [ 6] . Jazyk Java poskytuje omezenou formu existenciálních typů prostřednictvím zástupného znaku . V jazycích, které implementují klasický let-polymorfismus ve stylu ML , lze existenciální typy simulovat pomocí takzvaných „ typově indexovaných hodnot “ [7] .
Mnoho systémů se statickým typem, jako jsou systémy v C a Java, vyžaduje deklaraci typu : programátor musí explicitně přiřadit konkrétní typ každé proměnné. Jiné, jako je Hindley-Milnerův typový systém používaný v ML a Haskell , dělají typovou inferenci : kompilátor odvozuje typy proměnných na základě toho, jak programátor tyto proměnné používá.
Například pro funkci f(x,y), která provádí sčítání xa y, to může kompilátor odvodit xa ymusí to být čísla - protože operace sčítání je definována pouze pro čísla. Volání funkce někde v programu fpro parametry jiné než číselné (například pro řetězec nebo seznam) tedy signalizuje chybu.
Číselné a řetězcové konstanty a výrazy obvykle často vyjadřují typ v určitém kontextu. Výraz 3.14může například znamenat reálné číslo , zatímco to [1,2,3]může být seznam celých čísel – obvykle pole .
Obecně řečeno, typová inference je možná, pokud je v teorii typů zásadně rozhodnutelná . Navíc, i když je inference pro danou teorii typů nerozhodnutelná, inference je často možná pro mnoho skutečných programů. Systém typu Haskell , který je variací systému typu Hindley-Milner , je omezením systému Fω System na takzvané prvořadé polymorfní typy, na kterých je možné usuzovat. Mnoho kompilátorů Haskell poskytuje polymorfismus libovolného pořadí jako rozšíření, ale díky tomu je odvození typu nerozhodnutelné, takže je vyžadována explicitní deklarace typu. Nicméně kontrola typové konzistence zůstává rozhoditelná a pro programy s prvotřídním polymorfismem jsou typy stále odvoditelné.
Některé jazyky, jako například C# , mají jednotný typový systém [8] . To znamená, že všechny typy jazyka, až po ty primitivní , se dědí z jednoho kořenového objektu (v případě C# z třídy Object). Java má několik primitivních typů, které nejsou objekty. Spolu s nimi Java také poskytuje typy obalových objektů, takže vývojář může použít primitivní nebo objektové typy, jak uzná za vhodné.
Mechanismus kontroly konzistence typu ve staticky typovaném jazyce kontroluje, zda jakýkoli výraz odpovídá typu očekávanému v kontextu, ve kterém se vyskytuje. Například v příkazu přiřazení typu se typ odvozený pro výraz musí shodovat s typem deklarovaným nebo odvozeným pro proměnnou . Zápis shody, nazývaný kompatibilita , je specifický pro každý jazyk. x := eex
Pokud ea xjsou stejného typu a přiřazení je pro tento typ povoleno, pak je výraz legální. Proto je v nejjednodušších typových systémech otázka kompatibility dvou typů zjednodušena na otázku jejich rovnosti ( ekvivalence ). Různé jazyky však mají různá kritéria pro určení typové kompatibility dvou výrazů. Tyto teorie ekvivalence se pohybují mezi dvěma extrémy: systémy strukturního typu , ve kterých jsou dva typy ekvivalentní, pokud popisují stejnou vnitřní strukturu hodnoty; a systémy nominativních typů , ve kterých syntakticky odlišné typy nejsou nikdy ekvivalentní ( to znamená, že dva typy jsou si rovny, pouze pokud jsou jejich identifikátory stejné) .
V jazycích s podtypy jsou pravidla kompatibility složitější. Pokud je například podtypem , pak lze hodnotu typu použít v kontextu, který očekává hodnotu typu , i když opak není pravdivý. Stejně jako u ekvivalence se vztahy podtypů v různých jazycích liší a je možných mnoho variací pravidel. Přítomnost parametrického nebo situačního polymorfismu v jazyce může také ovlivnit kompatibilitu typů. ABAB
Někteří programátoři preferují systémy statického typu, jiní zase dynamické . Staticky typované jazyky signalizují chyby typové konzistence v době kompilace , mohou generovat efektivněji spustitelný kód a pro takové jazyky je možné relevantnější dokončení v IDE . Zastánci dynamického psaní argumentují, že jsou vhodnější pro rychlé prototypování a že chyby shody typu jsou pouze malým zlomkem potenciálních chyb v programech [9] [10] . Na druhou stranu u staticky typovaných jazyků se explicitní deklarace typu obvykle nevyžaduje, pokud jazyk podporuje odvození typu a některé dynamicky typované jazyky provádějí optimalizace za běhu [11] [12] , často pomocí částečného typu. závěr [13] .
| Typy dat | |
|---|---|
| Neinterpretovatelné | |
| Numerický | |
| Text | |
| Odkaz | |
| Kompozitní | |
| abstraktní | |
| jiný | |
| související témata | |