Typový systém

Typový systém lze v informatice definovat jako „tvárný syntaktický rámec pro klasifikování výrazů podle toho, jaký druh hodnoty vypočítávají“.^[1] Typový systém porovnává datové typy a výpočty ve výrazech a tím umožňuje zajistit, že nedojde k typovým chybám. Různé operace očekávají různé datové typy a typový systém zajišťuje, aby nebyly použity hodnoty, pro které nemá operace smysl.

Kompilátor může k uložení hodnoty použít staticky definovaný datový typ a pak na ni aplikovat příslušný typ výpočtu. Například kompilátor jazyka C používá datový typ float, který je podle IEEE 754 reprezentován jako 32bitové číslo, a používá pro něj speciální strojové instrukce určené pro výpočty s pohyblivou řádovou čárkou.

Úroveň typových omezení a způsob jejich posuzování mají vliv na typování daného programovacího jazyka. Programovací jazyk může v případě typového polymorfizmu přiřadit každému typu další operace s různými konkrétními algoritmy. Teorie typů řeší typové systémy, i když konkrétní typové systémy vycházejí z praktických otázek jako je architektura počítače, implementace překladače a konstrukce programovacího jazyka.

Základy

Přiřazování datových typů (tj. typování) dává význam sekvencím bitů. Typy se obvykle asociují s hodnotami v paměti nebo objekty jako jsou proměnné. Jelikož je každá hodnota v počítači pouze sekvence bitů, hardware proto nedokáže na tomto základě sám rozlišovat mezi adresou v paměti, kódem instrukce, znakem, celým číslem, číslem s plovoucí řádovou čárkou atd. Jak má sekvence bitů chápat, určuje programátor v programu prostřednictvím datových typů.

V dnešních jazycích programátor pracuje s abstraktnějšími typy než je bit a konkrétní implementace pomocí (ne nutně sekvence) bitů ho zpravidla nezajímá. Tu určuje tvůrce kompilátoru. Pro programátora je podstatné, že z bitové reprezentace lze jednoznačně rekonstruovat původní hodnotu. Samozřejmě konkrétní implementace se projevuje, např. v rozsahu čísel a znaků, nepřenositelnosti programů apod.

Mezi hlavní funkce poskytované typovým systémem patří:

Bezpečnost

Použití typů dovoluje kompilátoru detekovat nesmyslný nebo pravděpodobně neplatný kód. Například, můžeme identifikovat výraz 3/„Hello World“ jako neplatný, protože aritmetická pravidla nespecifikují, jak dělit celé číslo řetězcem. Silná typová kontrola nabízí větší bezpečnost, nezaručuje však úplnou bezpečnost (více informací viz typová bezpečnost).

Optimalizace

Statická typová kontrola může poskytovat důležité kompilační informace. Například, když typ vyžaduje, že hodnota musí být násobkem 4 bajtů, může kompilátor použít efektivnější strojovou instrukci.

Dokumentace

Ve více expresivních typových systémech mohou typy sloužit i jako určitá forma dokumentace, neboť mohou ilustrovat záměry programátora. Například časová razítka mohou být reprezentována jako celá čísla – ale když programátor deklaruje funkci, která vrací hodnotu typu časové razítko (timestamp), místo celého čísla (integer), pak tato část informuje o významu funkce.

Abstrakce (nebo modularita)

Typy dovolují programátorům přemýšlet o programech na vyšší úrovni, než jsou bity nebo bajty a nemusí se obtěžovat s nízkoúrovňovou implementací. Například umožňuje programátorovi dívat se na řetězce jako na soubor znaků a ne jako na pouhé pole bajtů nebo umožňuje vyjádřit rozhraní mezi dvěma subsystémy. To pomáhá lokalizovat definice potřebné pro interoperabilitu subsystémů a zabraňuje nesrovnatelnostem při komunikaci těchto subsystémů.

Program obvykle sdružuje jednotlivé hodnoty s jedním konkrétním typem (i když typ může mít víc než jeden podtyp). Jiné entity, jako jsou objekty, moduly, komunikační kanály, závislosti nebo dokonce samy typy se mohou spojit s typem. Některé implementace se označují následujícími označeními (i když se jedná o technicky odlišné pojmy):

• datový typ – typ hodnoty
• třída – typ objektu
• kind – typ typu

Typový systém, který je stanovený pro každý programovací jazyk, hlídá chování napsaných programů a zakazuje chování mimo tato pravidla. Účinný systém obvykle poskytuje jemnější ovládání než je typový systém.

Formálně teorie typů studuje typové systémy. Komplikovanější systémy (např. závislé typy), umožňují pro jemněji zrnité programové specifikace ověření typovou kontrolou, za cenu toho, že typ nebo jiné vlastnosti budou nerozhodnutelné a kontrola typu je závislá na uživateli dodaných důkazech. Je náročné najít dostatečně expresivní typový systém, který splňuje bezpečným způsobem všechny programové praktiky v typové bezpečnosti, jak výstižně řekl Mark Manasse:^[2]

Tento zásadní problém řešíme pomocí teorie typů, abychom se ujistili, že programy mají smysl. Zásadním problémem této teorie je, že programy nemusí mít význam, který je jim připisován. Z toho vyplývá, že se snažíme hledat bohatší typové systémy.

Typy a správnost

Typová kontrola přispívá k správnosti programu (správnosti programu), ale nemůže ji zaručit, protože kontroluje "pouze" typy. V závislosti na konkrétním typovém systému může vydat program špatný výsledek, i když je správně napsaný (asi myšleno typově správně) a kompilátor nehlásí žádné chyby. Například dělení nulou u většiny programovacích jazyků nespadá do typové kontroly, ale je to běhová chyba. Pokud chceme dokázat, že je program bez obecnějších vad, použijeme k tomu jiné druhy formálních metod známé jako analýza programu. Formální metody jsou při vývoji a testování softwaru široce používanou empirickou metodou pro zjištění chyb, které typová kontrola nemůže odhalit.

Některé úlohy typového odvozování jsou i nerozhodnutelný problém.

Typová kontrola

K ověřování a omezování typů – typové kontrole - dochází buď při kompilaci (statická kontrola) nebo za běhu (dynamická kontrola). Pokud specifikace jazyka vyžaduje silnou typovou kontrolu (to zn. více či méně umožňuje pouze automatické typové konverze, které neztrácí informace), můžeme říct, že je proces silně typovaný, pokud ne, pak je slabě typovaný. Tyto pojmy však nejsou používány v striktním slova smyslu.

Statická typová kontrola

Programovací jazyk používá statickou typovou kontrolu, když se typová kontrola provádí při kompilaci na rozdíl od běhu. Mezi staticky typované jazyky patří ActionScript 3, Ada, C, C++, C#, D, Eiffel, F#, Fortran, Go, Haskell, JADE, Java, ML, Objective-C, OCaml, Pascal, Perl (s ohledem na rozlišení skalárů, polí, hashí a subrutin) a Scala. Statická typová kontrola je omezená forma ověření správnosti programu (viz typová bezpečnost), protože umožňuje zachytit mnoho chyb typů už v rané fázi vývoje. Statická typová kontrola vyhodnotí informace o typech, které budou stanoveny při kompilaci a navíc je schopná ověřit, že podmínky budou platit pro všechna spuštění programu a tím se eliminuje potřeba provádět typovou kontrolu při každém spuštění. Tím, že vynecháme typovou kontrolu při běhu, může být běh programu efektivnější (tj. rychlejší nebo se sníží nároky na paměť) a umožní to další optimalizace.

Jelikož se určují informace o typu už při kompilaci, nemají statické kontroly typu informace o typech, které jsou k dispozici jen při běhu programu, proto musí být kontrola opatrná. Musí odmítnout programy, které se správně chovají až při běhu, protože správné typy nelze určit staticky. Například máme výraz <complex test>, který je při běhu vždy vyhodnocen jako true, program obsahuje kód

if <complex test> then 42 else <type error>

bude zamítnuto jako špatný typ, protože statická analýza nemůže určit jestli nebude vybrán příkaz else.^[1] Konzervativní chování statických kontrol je výhodné^[kdo?], jestliže <complex test> bude vyhodnocen jako false jen zřídka: Statická typová kontrola dokáže detekovat chybu typu v málo používaných větvích programu. Bez statické kontroly se ani u kódu, který je na 100% pokryt testy nemusí povést takovou chybu objevit. Testy mohou mít problémy s rozpoznáním tohoto druhu chyb, protože musíme brát v úvahu kombinace všech míst, kde jsou hodnoty vytvořeny a kde jsou používány.

Nejpoužívanější staticky typované jazyky nejsou formálně typově bezpečné. Mají „mezery“ ve specifikaci programovacího jazyka, které umožňují programátorům psát kód, který obchází statickou kontrolu typů, a tak může nastat další škála problémů. Například většina C jazyků obsahuje type punning a Haskell má vlastnosti jako unsafedPerformIO: takové operace mohou být nebezpečné za běhu tím, že mohou způsobit nežádoucí chování způsobené nesprávným zadáním hodnot.

Pro statickou typovou kontrolu není rozhodující, zda a jak často programátor musí do zdrojového kódu typy psát. Podstatné je, že se typy dají určit během kompilace. Pokud je píše, kompilátor má jednodušší práci a vystačí si s typovou kontrolou, jinak musí využít typové odvozování (jinde řčeno typové usuzování).

Dynamická typová kontrola

O programovacím jazyce řekneme, že je dynamicky typovaný, když je většina typové kontroly prováděna za běhu, místo při kompilaci. Při dynamické typové kontrole mají typy hodnoty, ale ne proměnné a to znamená, že proměnná může ukazovat na hodnotu jakéhokoli typu. Jazyky s dynamickou typovou kontrolou jsou například APL, Erlang, Groovy, JavaScript, Lisp, Lua, Matlab/GNU Octave, Perl (pro uživatelsky definované typy, ne však pro vestavěné typy), PHP, Prolog, Python, Ruby, Smalltalk, Tcl a Clojure.

Implementace dynamicky typovaných jazyků obyčejně spojuje run-time objekty s „tagy“, které obsahují informace o jejich typu. Tyto run-time klasifikace se používají k implementaci typových kontrol a expedují přetížené funkce, ale můžeme také využít dynamické ovládání, pozdní vazbu a podobné styly, které by byly ve staticky typovaném jazyce přinejmenším těžkopádné, protože vyžadují použití variantních typů nebo podobných vlastností.

Obecněji, jak je vysvětleno níže, může dynamická typová kontrola vylepšit podporu dynamických vlastností programovacího jazyka jako jsou generování typů a funkce založené na run-time datech. (Přesto dynamicky typované jazyky nemusí podporovat některé nebo dokonce žádné tyto funkce a některé dynamické programovací jazyky jsou dokonce staticky typované). Na druhou stranu dynamické typování poskytuje a priori záruk: dynamicky typovaný jazyk přijímá a pokouší se spustit i programy, které by byly při statické kontrole posouzeny jako neplatné a to buď kvůli chybě v programu nebo kvůli tomu, že statická typová kontrola je příliš konzervativní.

Dynamická typová kontrola může vést na runtime chyby, to znamená že hodnota může mít za běhu nečekaný typ a je na ní aplikována neplatná operace. Takové chyby se mohou vyskytnout až daleko za místem, kde je programovací chyba, neboli místa, kde dostala data nesprávný datový typ. Chyby tohoto typu se většinou špatně objevují.

Runtime kontroly dynamických jazykových systémů mohou být potenciálně složitější než kontroly staticky typovaných jazyků, jelikož mohou použít dynamické informace i veškeré informace ze zdrojového kódu. Nicméně runtime kontrola uplatňuje podmínky jen při konkrétním spuštění a kontroly se opakují při každém spuštění programu.

Při vývoji v dynamicky typovaných jazycích se často používají nejrůznější programovací praktiky, jako například testování. Testování je klíčové při profesionálním vývoji softwaru a je zejména důležité právě v dynamicky typovaných jazycích. V praxi se testování provádí kvůli zajištění správného fungování programu, přičemž lze odhalit mnohem širší rozsah chyb než statickou typovou kontrolou, ale naopak nelze souhrnně najít chyby, které detekuje statická typová kontrola.

Kombinace dynamické a statické typové kontroly

Přítomnost statické typové kontroly v programovacím jazyce nemusí nutně znamenat absenci všech dynamicky typovaných mechanizmů. Například Java a některé další zdánlivě staticky typované jazyky podporují downcasting a jiné typové operace, které jsou závislé na běhové typové kontrole formou dynamického přetypování. Obecněji řečeno, většina programovacích jazyků podporuje mechanizmy pro přiřazení přes různé 'druhy' dat, jako jsou disjunktní spojení, variantní typy a polymorfní objekty: I když se nejedná o interakci s typovými komentáři nebo typovou kontrolou, jsou tyto mechanizmy podobné implementaci dynamické typové kontroly. Viz programovací jazyk, kde je další diskuze o interakci mezi statickou a dynamickou typovou kontrolou.

Některé jazyky, jako například Clojure, jsou ve výchozím nastavení dynamicky typované, ale toto chování lze přepsat pomocí explicitních typových hintů tak, že výsledek je typován staticky. Jedním z důvodů pro použití těchto hintů je využití statického typování v částech kódu, které jsou citlivé na výkon.

Verze .NET frameworku 4.0 podporuje variantu dynamického typování pomocí jmenného prostoru System.Dynamic, pomocí kterého statický objekt typu 'dynamic' je zástupný symbol pro .NET runtime, který se zeptá na dynamické vlastnosti kvůli referenci na objekt.

Statická a dynamická typová kontrola v praxi

Volba mezi statickou a dynamickou typovou kontrolou vyžaduje kompromisy.

Statická typová kontrola najde chyby typu spolehlivě v době kompilace, to by mělo zvýšit spolehlivost dodaného programu. Nicméně se programátoři nemohou shodnout jak často dochází k chybám typu a také na podílu chyb, které jsou kódované a které by měly spadat pod vhodnou reprezentaci určenou typy v kódu. Stoupenci statické typové kontroly jsou přesvědčeni, že programy jsou spolehlivější, když mají dobře zkontrolované typy, zatímco příznivci dynamické typové kontroly směřují k distribuovanému kódu, který se ukázal jako spolehlivý a k malým chybovým databázím. Výhoda statické typové kontroly je, že se pravděpodobně zvýší stabilita typového systému. Zastánci závisle typovaných jazyků jako je Dependent ML a Epigram navrhli, že téměř všechny chyby lze považovat za typové chyby, jestliže typy používané v programu jsou řádně deklarovány programátorem nebo je správně odvodil kompilátor.^[3]

Statická typová kontrola obvykle vyústí ve zkompilovaný kód, který běží rychleji, protože neobsahuje analýzu a kontrolu typů. Když kompilátor zná přesné datové typy, které jsou použity, může produkovat optimalizovaný přeložený kód. Také lze pro staticky typované jazyky snadněji najít příkazy v assembleru (.. v instrukční sadě). Některé dynamicky typované jazyky jako Common Lisp umožňují z tohoto důvodu pro optimalizaci volitelný typ deklarace. Tím se stává statická typová kontrola všudypřítomnou. Viz optimalizace.

Oproti tomu dynamická typová kontrola může umožnit kompilátorům rychlejší běh a interpretům dynamičtěji načítat nový kód, protože v dynamicky typovaných jazycích mohou mít změny zdrojového kódu za následek menší kontrolu a stačí přehodnotit méně kódu. To také může redukovat cyklus editace – kompilace – testování – ladění.

Staticky typované jazyky, které nemají dostatečné typové usuzování (jako je Java nebo C) vyžadují, aby programátoři deklarovali typy, které zamýšlejí použít v metodách nebo funkcích. To může sloužit jako rozšiřující dokumentace k programu, kde kompilátor nedovolí programátorovi ignorovat nebo dovolí posun k synchronizaci. Může však existovat jazyk, který je staticky typovaný bez předchozích deklarací typů (například Haskell, Scala a v menší míře i C#) a to znamená, že explicitní deklarace typu není nutnou podmínkou pro statické typování ve všech jazycích.

Dynamická typová kontrola podporuje některé konstrukce, které by statická typová kontrola zamítla jako nepřijatelné. Například eval funkce, ty spustí jakákoli data jako kód. Kromě toho dynamickému typování lépe vyhovuje přechodný kód a prototypování, takže umožňuje zástupnou datovou strukturu (falešný objekt) transparentně použít na místě plně rozvinutě datové struktury (obvykle pro účely experimentování a testování).

V případě dynamického typování se často používá duck typing (kachní typování).

Dynamická typová kontrola typicky dělá metaprogramování více efektivní a jednodušší pro použití. Například C++ šablony jsou typicky těžkopádnější na typování než ekvivalent v Ruby nebo Pythonu. Pokročilejší run-time konstrukty jako metatřídy a introspekce je často těžké použít v staticky typovaných jazycích. V některých jazycích mohou být tyto funkce také použity například pro generování nových typů a chování za běhu, založených na run-time datech. Tyto moderní konstrukce jsou často poskytovány dynamickými programovacími jazyky, mnoho z nich je dynamicky typovaných, i když dynamické typování nemusí mít souvislost s dynamickými programovacími jazyky.

Silné a slabé typování

Typový systém říká, že rysem silného typování je specifikace jednoho nebo více omezení, jak mohou být smíšeny operace zahrnující hodnoty různých typů. Počítačový jazyk, jenž implementuje silné typování, bude předcházet úspěšnému provedení operací s argumenty špatného typu.

Slabé typování znamená, že jazyk implicitně převádí (nebo přidělí) typy při použití. Vezměme následující příklad:

var x := 5; // (1) (x je celé číslo)
var y := "37"; // (2) (y je řetězec)
x + y; // (3) (?)

V slabě typovaných jazycích je výsledek nejasný. Některé jazyky jako je Visual Basic, by při spuštění kódu produkovaly výsledek 42: systém by převedl řetězec „37“ na číslo 37, což má smysl téměř násilné operace. Jiné jazyky jako JavaScript by produkovaly výsledek „537“: systém převede číslo 5 na řetězec „5“ a sloučí oba. Ve VisualBasicu i JavaScriptu je výsledek určen pravidlem, které bere v úvahu oba operandy. V JavaScriptu nezáleží na pořadí operandů (x + y by bylo „375“). Když použijeme operátor „+“ na String a Number(JavaScriptový typ) výsledek je String, jestliže hodnota y je String, který nejde převést na Number (např. „Hello World“), pak je výsledek diskutabilní. V některých jazycích jako AppleScript je typ výsledku vždy určen podle typu operandu nejvíce vlevo.

Stejným způsobem, v důsledku dynamické JavaScriptové typové konverze:

var y = 2 / 0                  // y se nyní rovná konstantě nekonečno
y == Number.POSITIVE_INFINITY        // vrací true
Infinity == Number.POSITIVE_INFINITY // vrací true
"Infinity" == Infinity               // vrací true
y == "Infinity"                      // vrací true

Přetypování v C špatně ilustruje problém, který může nastat, když chybí silné typování. Když programátor přetypovává hodnotu z jednoho typu do jiného v C, nemusí vždy při kompilaci kompilátor povolit tento kód, ale za běhu ho povolí jako přijatelný. To umožňuje rychlejší a kompaktnější kód, ale může to ztížit ladění.

Bezpečně a nebezpečně typované systémy

Třetí způsob, jak roztřídit typový systém programovacího jazyka používá bezpečnost typových operací a konverzí. Počítačový odborníci považují jazyk za „typově bezpečný“, pokud neumožňuje operace nebo konverze, které vedou k chybným podmínkám.

Někteří pozorovatelé používají termín paměťově bezpečný jazyk (nebo jen bezpečný jazyk) pro popis jazyků, u kterých nemohou nastat nedefinované operace. Například paměťově bezpečný jazyk kontroluje hranice polí nebo staticky zjišťuje (tj. při kompilaci před spuštěním) přístup pole mimo hranice pole, což může způsobovat komplikace a možná i běhové chyby.

var x := 5;     // (1)
var y := "37";  // (2)
var z := x + y; // (3)

V jazycích podobných Visual Basicu proměnná v příkladu nabývá hodnoty 42. I když to programátor chtít může nebo nemusí, jazyk definuje výsledek konkrétně a program nehavaruje nebo nepřiřadí špatně definovanou hodnotu do proměnné. Z tohoto pohledu jsou jazyky typově bezpečné, nicméně v některých jazycích, pokud by byla hodnota y řetězec, který nejde převést na číslo (např. „Hello World“), by byl výsledek nedefinovaný. Takové jazyky jsou typově bezpečné (nebudou havarovat), ale mohou snadno produkovat nežádoucí výsledky. V jiných jazycích, jako JavaScript, může být číselný operand převeden na řetězec a provede se zřetězení. V tomto případě není výsledek nedefinovaný a dá se předvídat.

Nyní se podívejme na stejný příklad v C:

int x = 5;
char y[] = "37";
char* z = x + y;

V tomto příkladu budeme ukazovat na adresu v paměti pět znaků za y, což se rovná tři znaky po ukončovacím znaku textu, na který ukazuje y. Obsah tohoto umístění je prázdný a může ležet mimo adresovanou paměť. Pouhý výpočet tohoto ukazatele může vyvolat nedefinované chování (včetně pádu programu), dle standardů C a v typických systémových dereferencích by mohlo způsobit pád programu. Máme dobře typovaný, ale ne paměťově bezpečný program, toto je podmínka, ke které nemůže dojít v typově bezpečném jazyce.

V některých jazycích, jako JavaScript se používají speciální číselné hodnoty a konstanty, které povolují typově bezpečné matematické operace bez vyústění do běhových chyb. Například, když dělíme typ Number typem String nebo typ Number nulou.

var x = 32;
var aString = new String("A");
x = x / aString;                // x je nyní rovno konstantě NaN, to znamená Not a Numer (není číslo)
is NaN(x);                      // vrátí true
typeof(x);                      // vrátí „number“
var y = 2 / 0;                  // y je nyní rovno konstantě nekonečno
y == Number.POSITIVE_INFINITY;  // vrátí true
typeof(y);                      // vrátí „number“

Polymorfizmus a typy

Termín „polymorfizmus“ odkazuje na schopnost kódu (v OOP zejména metod a tříd) pracovat s hodnotami různých typů nebo schopnost různých instancí stejné datové struktury obsahovat prvky různých typů. Typové systémy umožňují polymorfizmus proto, aby zlepšily znovu použitelnost kódu nebo kód zkrátily. V jazyce s polymorfizmem programátorům obvykle stačí^[kdo?] implementovat datovou strukturu jako seznam nebo asociativní pole, spíše než sólo pro každý prvek, který chtějí použít. Z tohoto důvodu počítačoví odborníci někdy nazývají některé formy polymorfizmu generickým programováním, což by se možná asi správně mělo nechat pouze pro případy, kdy se z jednoho kódu generuje a překládá několik kódů pro různé typy, ať už implicitně nebo explicitně. Typově teoretické základy polymorfizmu úzce souvisí s abstrakcí, modularitou a (v některých případech) s podtypy.

Ve funkcionálních jazycích a kombinovaných jazycích s funkcionálními rysy se občas potulují typové proměnné, podle kterých ... se polymorfizmus snadno pozná.

Duck typing

Při „Duck typing“ volaná metoda m nespoléhá na prohlašovaný typ objektu, ale pouze na to, že objekt jakéhokoli typu musí dodat implementaci volané metody, je-li za běhu volána.

Duck typing se liší od strukturovaného typování v tom případě, že část (modul celé struktury) potřebné pro daný lokální výpočet, je přítomná za běhu. Duck typový systém je splněn při analýze typové identity. Na druhou stranu, strukturovaný typový systém vyžaduje analýzu celé modulové konstrukce při kompilaci k určení typové identity nebo typové závislosti.

Duck typing se liší od strukturovaného typování v řadě aspektů. Nejvýznamnější z nich jsou, že pro duck typing je informace o typu určena za běhu (na rozdíl od kompilace) a název typu není důležitý k určení typové identity nebo typové závislosti. Pro daný bod při provádění programu jsou nutné pouze částečné informace o struktuře.

Duck typing používá předpoklad, že (odkaz na hodnotu) „jestliže chodí jako kachna a kváká jako kachna, pak je to kachna“ (toto je kachní test, autor James Whitconb Riley). Tento termín vytvořil Alex Martelli v roce 2000 zprávou^[4] comp.lang.python diskuzní skupiny (viz Python)

Specializované typové systémy

Mnoho typových systémů bylo vytvořeno speciálně pro použití v určitých prostředích, s některými typy dat nebo mimo skupinu statických programových analýz. Často jsou založeny na myšlenkách z formální teorie typů a jsou k dispozici pouze jako součást prototypových výzkumných systémů.

Závislostní typy

Závislostní typy jsou založeny na myšlence využití skalárů nebo hodnot přesněji popisujících nějakou jinou hodnotu. Například „matice (3×3)“ může být matice typu 3×3. Můžeme potom definovat pravidla, například následující pravidlo pro násobení matic:

matrix_multiply: matice(k,m) × matice(m,n) → matice(k,n)

kde k, m, n jsou libovolná kladná celá čísla. Varianta ML tzv. závislého ML byla vytvořena na základě tohoto typového systému. Protože typová kontrola převodů závislých typů je nerozhodnutelná, ne všechny systémy používají tuto typovou kontrolu bez nějakého druhu omezení. Závislé ML limituje druh rovnosti, to může rozhodnout Presburgerova aritmetika. Další jazyky, např. Epigram dělá hodnotu všech výrazů v jazyce rozhodnutelnou, takže typová kontrola může rozhodnout. Také je možné vytvořit Turing kompatibilní jazyk, za cenu nerozhodnutelnosti typové kontroly, jako je to u Cayenne.

Lineární typy

Lineární typy jsou založené na teorii lineární logiky a úzce souvisejí s jedinečností typů. Typy jsou přiřazeny k hodnotám, které mají tu vlastnost, že je na ně vždy jen jeden odkaz. Toto je cenné pro popisování velkých neměnných hodnot, jako texty, soubory a podobné. Protože jakákoli činnost, která současně ničí lineární objekt a vytváří podobný (např. 'str = str + "a"') lze optimalizovat „pod kapotou“ do místní mutace. Normálně to není možné, protože takové mutace mohou mít nežádoucí účinky na částech programu držících jiné reference na objekt, tím porušují referenční transparentnost. Jsou také použity v prototypu operačního systému Singularity pro meziprocesorovou komunikaci, která statisticky zajišťuje, že procesy nemohou sdílet objekty se sdílenou pamětí, aby se dodržely běhové podmínky. Čistý (takzvaně Pure) jazyky (např. Haskell) používá tento typový systém s cílem získání rychlosti při zachování bezpečnosti.

Křížené typy

Křížené typy jsou typy popisující hodnoty, které patří do dvou různých typů s překrývajícími se sadami hodnot. Například ve většině implementací C má typ char se znaménkem rozsah -128 až 127 a char bez znaménka 0 až 255, takže křížený typ těchto dvou typů by měl rozsah 0 až 127. To znamená, že křížený typ může bezpečně přejít do funkce, která čeká char se znaménkem nebo bez znaménka, protože je kompatibilní s oběma typy.

Křížené typy jsou užitečné pro popis přetížených funkcí typu: Například, když „int → int“, je typ funkce dostávající integerový argument a vracející integer, „float → float“, to je funkce dostávající floatový argument a vracející floatový argument, pak můžeme použít křížení těchto dvou typů k popisu funkcí, do kterých vstupuje jeden nebo druhý datový typ. Takovéto funkce by měly být bezpečně přijaty v jiných funkcích očekávajících „int → int“, ale nemohou použít funkcionalitu „float → float“.

V hierarchii podtříd kříženec typu a předek typu (jeho rodič) je nejvíce odvozený typ. Průsečík příbuzných typů je prázdný.

Jazyk Forsythe obsahuje obecnou implementaci křížených typů. Omezená forma je upřesnění typů.

Sjednocené typy

Sjednocené typy jsou typy popisující hodnoty, kde hodnota patří do obou dvou typů. Například v C je char se znaménkem -128 až 127 a bez znaménka 0 až 255, pak sjednocení těchto dvou typů je -127 až 255. Každá funkce používající tento sjednocený typ by měla podporovat integer v jeho celém rozsahu. Obecně řečeno, na sjednocený typ platí pouze operace, které platí na oba typy před sjednocením. Koncept „sjednocení“ v C je podobný jako sjednocené typy, ale není typově bezpečný, protože povoluje operace platné i jen pro jeden z typů. Sjednocené typy jsou důležité v programové analýze, kde jsou používány pro reprezentaci symbolických hodnot, jejichž přesná povaha (např. hodnota nebo typ) není známá.

V hierarchii podtříd spojení typu a předka typu (jeho rodiče) jsou předky typu. Spojení sourozenců typů je podtyp jejich společného předka (tedy všechny povolené operace na jejich společném předku jsou povoleny na sjednocení typů, ale mohou mít i další platné společné operace).

Existenční typy

Existenční typy jsou často používány ve spojení se záznamovými typy reprezentujícími moduly a abstraktní datové typy, vzhledem k jejich schopnosti oddělit implementaci od rozhraní. Například typ „T = ∃X { a: X; f: (X → int); }“ popisuje modul rozhraní, které má datový člen typu X a vrací celé číslo. To by mohlo být realizováno různými způsoby, například:

• intT = { a: int; f: (int → int); }
• floatT = { a: float; f: (float → int); }

Oba tyto typy jsou podtypy obecnějšího typu T a odpovídají konkrétní implementaci typů, takže hodnota jednoho z těchto typů je typu T. Dostaneme hodnotu „t“ typu „T“ o níž víme, že je dobře typovaná bez ohledu na to, co je abstraktní typ X. To dodává flexibilitu pro výběr typů vhodných pro konkrétní implementaci. Jestliže klienti používají pouze hodnoty typu rozhraní, pak jsou existenční typy izolovány z výběru.

Obecně lze říci, že je možné, aby typová kontrola odvodila kterému existencionálnímu typu datový modul patří. Ve výše uvedeném příkladu int T = { a: int; f:(int → int);}, může mít také typ ∃X { a: X; f: (int → int); }. Nejjednodušším řešením je opatřit každý model jeho předpokládaným typem, např.:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

Ačkoli abstraktní datové typy a moduly, byly implementovány v programovacích jazycích již před delší dobou, nebylo to dříve než v roce 1988, kdy John C. Mitchell a Gordon Plotkin založili formální teorii pod heslem: „Abstraktní [datové] typy mají existenční typ“.^[5] Tato teorie je druhý stupeň typového lambda kalkulu podobný Systému F, ale existenčním místo univerzálním kvantifikátorem.

Explicitní nebo implicitní deklarace a odvozování

Mnoho statických typových systémů, jako C, Java vyžaduje deklarování typů: programátor musí výslovně přiřadit každé proměnné určitý typ. Jiné jazyky, jako Haskell provádějí typové odvozování: kompilátor vyvozuje závěry o typech proměnných založené na tom, jak programátor tyto proměnné využívá. Například máme funkci f(x,y), která sčítá x a y. Překladač může odvodit, že x a y musí být číslo a před sčítáním je také definuje jako čísla. Proto každé volání funkce f jinde v programu, který specifikuje nečíselný typ (např. řetězec nebo seznam) jako argument, by signalizoval chyby.

Numerické a řetězcové konstanty a výrazy v kódu často znamenají typ v určitém kontextu. Například výraz 3,14 může znamenat typ floating-point, zatímco [1, 2, 3] může znamenat seznam celých čísel, což je typicky pole.

Typové odvozování je obecně možné jen když se jedná o rozhodnutelný dotaz z teorie typů. Navíc, i když je odvozování pro danou typovou teorii obecně nerozhodnutelné, je to často přijatelné pro většinu reálných programů. Typový systém Haskellu, verze od Hindley-Milnera, je omezení Systému Fω na takzvané polymorfické typy prvního stupně, v kterých je typové odvozování rozhodnutelné. Většina Haskellových kompilátorů povoluje libovolnou hodnost polymorfizmu jako rozšíření, ale to způsobí typové odvozování, polymorfické programy vyšších stupňů jsou zamítnuty, dokud nedostanou explicitní typové anotace.

Druhy typů

Typ typů je druh. Druhy se výslovně jeví v plně typovém programování jako typový konstruktor v jazyku Haskell.

Typy se dělí do několika širokých kategorií:

• Primitivní typy – nejjednodušší druh typu, např. celé číslo a desetinné číslo
  • Boolean
  • Integrální typy – typy celých čísel, např. celá a přirozená
  • typy s plovoucí desetinnou čárkou – typy čísel v plovoucí desetinné čárce
• Referenční typy
• Variantní typy
  • Nulární typy
• Kompozitní typy – typy složené ze základních typů, např. pole nebo záznamy
  • Abstraktní datové typy
• Algebraické typy
• Podtypy
• Odvozené typy
• Objektové typy, např. datové proměnné
• Částečné typy
• Rekurzivní typy
• Funkční typy, např. binární funkce
• typy s univerzálním kvantifikátorem, např. parametrizované typy
• typy s existenčním kvantifikátorem, např. moduly
• Zpřesněné typy – typy, které jsou podmnožinami jiných typů
• Závislé typy – typy, které jsou závislé na podmínkách (hodnotách)
• Vlastnické typy – typy, které popisují nebo omezují struktury objektově orientovaných systémů.

Kompatibilita: rovnocennost a podtypy

Typová kontrola pro staticky typovaný jazyk musí ověřit, že typ jakéhokoli výrazu je v souladu s očekávaným typem v kontextu, ve kterém se tento výraz zobrazí. Například příkaz přiřazení ve tvaru x := e, musí odvodit, že typ výrazu e bude v souladu s deklarací nebo musí typ odvodit od proměnné x. Tento pojem konzistence tzv. kompatibility, je specifický pro každý programovací jazyk.

Pokud má e a x stejný typ a pro tento typ je povoleno přiřazení, pak se jedná o správný výraz. V nejjednodušším typovém systému se tedy otázka, zda jsou dva typy kompatibilní, redukuje na to, jestli jsou stejné (nebo ekvivalentní). Různé jazyky mohou mít nicméně odlišná kritéria, pokud dva typové výrazy slouží k označení stejného typu. Tyto různé nominální teorie typů' se značně liší. Jsou dva extrémní případy strukturálních typových systémů. První, ve kterém jsou každé dva typy ekvivalentní, popisuje hodnoty se stejnou strukturou a druhý, v němž žádné dva syntakticky vzácné druhy výrazů neoznačují stejný typ (tj. aby mohly být typy stejné, musí mít stejný „název“).

V jazycích s podtypy jsou vztahy kompatibility složitější. Zejména pokud A je podtyp B, potom hodnota typu A může být použita tam, kde se očekává hodnota typu B a to i v případě, že to nejde obráceně. Stejně jako ekvivalence jsou postupové vztahy definovány odlišně pro každý jazyk. Přítomnost parametrického nebo ad hoc polymorfizmu může mít také vliv na typovou kompatibilitu.

Programovací styl

Někteří programátoři dávají přednost staticky typovaným jazykům, jiní zase dynamicky typovaným jazykům. Staticky typované jazyky upozorňují programátory na typové chyby při kompilaci a mohou podávat větší výkon za běhu. Zastánci dynamicky typovaných jazyků tvrdí, že mají lepší podporu rychlého prototypování, že typové chyby jsou jen malá část chyb v programu.^[6][7] Rovněž se u dynamicky typovaných jazyků nemusí manuálně deklarovat typy, což je opět pro programátora pohodlné.

Některé moderní staticky typované jazyky obsahují typové odvozování, a tak se tato výhoda dynamických jazyků stírá. A naopak, některé dynamicky typované jazyky mají tak výrazné runtime optimalizace, že dokáží generovat kód blížící se v rychlosti překladačům statických jazyků, často s pomocí částečného typového usuzování.^[8][9]

Odkazy

Reference

V tomto článku byl použit překlad textu z článku Type system na anglické Wikipedii.

Literatura

• Smith, Chris, What To Know Before Debating Type Systems
• Tratt, Laurence, Dynamically Typed Languages, Advances in Computers, Vol. 77, pp. 149–184, July 2009

Související články

• Přetěžování operátorů
• Polymorfizmus v objektově orientovaném programování
• Programovací jazyk

Zdroj