Typový systém

Z Multimediaexpo.cz

Nemáte oprávnění „upravit tuto stránku“. Důvod:

Můžete si prohlédnout a zkopírovat zdrojový kód této stránky:

'''Typový systém''' lze v [[informatika|informatice]] definovat jako „tvárný [[syntax|syntaktický]] rámec pro klasifikování výrazů podle toho, jaký druh hodnoty vypočítávají“.<ref name="pierce2002">{{cite book |last=Pierce |first=Benjamin C. |title=Types and Programming Languages |publisher=MIT Press |year=2002 |id=ISBN 0-262-16209-1 }}</ref> Typový systém porovnává [[Datový typ|datové typy]] a výpočty ve [[výraz (formule)|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 [[programovací jazyk C|jazyka C]] používá datový typ ''float'', který je podle [[IEEE 754]] reprezentován jako [[32bitový|32bitové]] číslo, a používá pro něj speciální [[Strojová instrukce|strojové instrukce]] určené pro výpočty s [[Pohyblivá řádová čárka|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 [[Polymorfismus (programování)|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 [[elektronická paměť|paměti]] nebo [[objekt (programování)|objekty]] jako jsou [[proměnná|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 [[adresa (programování)|adresou v paměti]], [[strojová instrukce|kódem instrukce]], [[znak (počítače)|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ů. Mezi hlavní funkce poskytované typovým systémem patří: ;Bezpečnost: Použití typů dovoluje [[kompilátor|kompilátoru]] detekovat nesmyslný nebo pravděpodobně neplatný kód. Například, můžeme identifikovat výraz <code>3/"Hello World"</code> jako neplatný, protože [[aritmetika|aritmetická]] pravidla nespecifikují, jak dělit [[celé číslo]] [[řetězec|řetězcem]]. Silná typová kontrola nabízí větší bezpečnost, nezaručuje však úplnou bezpečnost (více informací viz. [[Typová kontrola|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 můžou typy sloužit i jako určitá forma [[dokumentace]], neboť mohou ilustrovat záměry programátora. Například časová razítka můžou být reprezentována jako celá čísla&nbsp;– 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í (informatika)|rozhraní]] mezi dvěma subsystémy. To pomáhá lokalizovat definice potřebné pro interopereabilitu subsystémů a zabraňuje nesrovnatelnostem při komunikaci těchto subsystémů. Typová kontrola přispívá k [[Styl zápisu programu|správnosti programu]], ale nemůže ji zaručit, když se vyskytne [[rozhodnutelnost|nerozhodnutelný problém]]. V závislosti na konkrétním typovém systému může vydat program špatný výsledek, i když je správně napsaný 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 [[Programátorská chyba|běhová chyba]]. Pokud chceme dokázat, že je program bez obecnějších vad, použijeme k tomu jiné druhy formálních [[metoda|metod]] známé jako [[analýza programu]]. Formální metody jsou při [[testování softwaru]] široce používanou [[empirický|empirickou]] metodou pro zjištění chyb, které typová kontrola nemůže odhalit. 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 [[objekt (programování)|objekty]], [[modul|moduly]], komunikační kanály, [[závislost|závislosti]] nebo dokonce samy typy se můžou 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ř. [[datový typ|závislé typy]]), umožňují pro jemněji zrnité programové specifikace ověření typovou kontrolou, za cenu toho, že typ nebo jiné vlastnosti budou [[rozhodnutelnost|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á kontrola|typové bezpečnosti]], jak výstižně řekl Mark Manasse: <ref>Pierce, Benjamin C. (2002), p. 208</ref> 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. == Typová kontrola == K ověřování a omezování typů – ''typové kontrole'' - dochází buď při [[kompilace|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 [[ActionScript]] 3, [[Ada]], [[programovací jazyk C|C]], [[C++]], [[C Sharp|C#]], [[D (programovací jazyk)|D]], [[Eiffel (programovací jazyk)|Eiffel]], [[F Sharp|F#]], [[Fortran]], [[Go (programovací jazyk)|Go]], [[Haskell]], [[JADE]], [[Java (programovací jazyk)|Java]], [[ML]], [[Objective-C]], [[OCaml]], [[Pascal]], [[Perl]] (s ohledem na rozlišení skalárů, polí, hashí a subrutin) a [[Scala (programovací jazyk)|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 <code><complex test></code>, který je při běhu vždy vyhodnocen jako <code>true</code>, program obsahuje kód :<code>if <complex test> then 42 else <type error></code> bude zamítnuto jako špatný typ, protože statická analýza nemůže určit jestli nebude vybrán příkaz <code>else</code>.<ref name="pierce2002" /> Konzervativní chování statických kontrol je výhodné, jestliže <code><complex test></code> bude vyhodnocen jako <code>false</code> 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á kontrola|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 [[:en:type punning|type punning]] a Haskell má vlastnosti jako <code>unsafedPerformIO</code>: takové operace můžou 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. ===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 definaované 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|přetížené funkce]], ale můžeme také využít dynamické ovládání, [[:en:Dynamic binding (computer science)|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ů můžou být potenciálně složitější než kontroly staticky typovaných jazyků, jelikož můžou 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í softwaru|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í [[:en:downcasting|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í sjednocení|disjunktní spojení]], [[:en:Variant type|variantní typy]] a [[Polymorfismus (programování)|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[http://msdn.microsoft.com/en-us/library/dd233052(VS.100).aspx 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 dymamická 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. <ref>{{Cite journal |last1=Xi |first1=Hongwei |last2=Scott |first2=Dana |title=Dependent Types in Practical Programming |journal=Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages |year=1998 |pages=214–227 |publisher=ACM Press |url=http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.548&rep=rep1&type=pdf }}</ref> Statická typová kontrola obvykle vyústí v zkompilovaný kód, který se spustí rychleji. Když kompilátor zná přesné datové typy, které jsou použity, může produkovat optimalizovaný zdrojový kód. Také lze pro staticky typované jazyky snadněji najít příkazy v assembleru. 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 (informatika)|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é [[:en:Type inference|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 (programovací jazyk)|Scala]] a v menší míře i [[C Sharp|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 ''[[:en:eval|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í). Dynamické typování se používá v duck typing (kachní typování), to podporuje snadnější opětovné použití kódu. 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 [[Python|Pythonu]]. Pokročilejší run-time konstrukty jako [[metatřída|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 [[operand|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'' Intimity == Number.POSITIVE_INFINITY ''// vrací true'' "Infinity" == Infinity ''// vrací true'' y == "Infinity" ''// vrací true'' [[C (programovací jazyk)|Přetypování]] v [[programovací jazyk C|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=== {{Hlavní článek|Typová kontrola}} 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 Basic|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 můžou 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 [[dereference|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 (zejména metod a tříd), aby pracoval 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. V jazyce s polymorfizmem programátorům obvykle stačí 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é programování|generickým programováním]]''. Typově teoretické základy polymorfizmu úzce souvisí s [[abstrakce|abstrakcí]], [[modul|modularitou]] a (v některých případech) s [[podtyp|podtypy]]. ===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 [[:en:Structural type system|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 [[:en:Structural type system|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 [[:en:duck test|kachní test]], autor [[James Whitconb Riley]]). Tento termín vytvořil [[:en:Alex Martelli|Alex Martelli]] v roce 2000 zprávou<ref>{{cite web |title=Re: polymorphism (was Re: Type checking in python?) |author=Martelli, Alex |id=8lmvn6017l@news1.newsguy.com |date=2000/07/26 |url=http://groups.google.com/group/comp.lang.python/msg/e230ca916be58835?hl=en& }}</ref> 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í [[:en:type theory|teorie typů]] a jsou k dispozici pouze jako součást prototypových výzkumných systémů. ==Závislé typy== [[Závislé 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 (programovací jazyk)|ML]] tzv. [[závislý ML|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 [[rozhodnutelnost|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ř. '<code>str = str + "a"</code>') 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 [[:en:Singularity (operating system)|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. [[:en:Clean (programming language)|Čistý]] jazyk (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 nemůžou 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ý typ|záznamovými typy]] reprezentujícími [[modul|moduly]] a [[abstraktní datový typ|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 [[:en:John C. Mitchell|John C. Mitchell]] a [[:en:Gordon Plotkin|Gordon Plotkin]] založili formální teorii pod heslem: "Abstraktní [datové] typy mají existenční typ"<ref>Mitchell, John C.; Plotkin, Gordon D.; [http://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf ''Abstract Types Have Existential Type''], ACM Transactions on Programming Languages and Systems, Vol. 10, No. 3, July 1988, pp. 470–502</ref>. Tato teorie je druhý stupeň typového [[Lambda kalkul|lambda kalkulu]] podobný [[:en:System F|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í ''[[:en:type inference|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 <code>3,14</code> může znamenat typ floating-point, zatímco <code>[1, 2, 3]</code> může znamenat seznam celých čísel, což je typicky [[Pole (datová struktura)|pole]]. Typové odvozování je obecně možné jen když se jedná o [[rozhodnutelnost|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í [[System F#System Fω|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í: * [[Datový typ|Primitivní typ]]y – nejjednodušší druh typu, např. [[celé číslo]] a [[Pohyblivá řádová čárka|desetinné číslo]] ** [[Boolean]] ** [[Integrální typ]]y – typy celých čísel, např. celá a přirozená ** typy s plovoucí desetinnou čárkou – typy čísel v plovoucí desetinné čárce * [[Datový typ|Referenční typ]]y * [[Datový typ|Variantní typ]]y ** [[Nulární typy]] * [[Datový typ|Kompozitní typ]]y – typy složené ze základních typů, např. pole nebo záznamy ** [[Abstraktní datový typ|Abstraktní datové typy]] * [[Datový typ|Algebraické typy]] * [[Datový typ|Podtypy]] * [[Datový typ|Odvozené typy]] * Objektové typy, např. datové proměnné * Částečné typy * [[Datový typ|Rekurzivní typ]]y * [[Datový typ|Funkční typ]]y, 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 <code>x := ''e''</code>, 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 <code>x</code> 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í typový systém|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 [[polymorfizmus|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í a že typové chyby jsou jen malá část chyb v programu. <ref>{{cite web |url=http://research.microsoft.com/en-us/um/people/emeijer/Papers/RDL04Meijer.pdf |title=Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages |last1=Meijer |first1=Erik |last2=Drayton |first2=Peter |publisher=Microsoft Corporation }}</ref><ref>{{cite web |url=http://docs.google.com/View?id=dcsvntt2_25wpjvbbhk |title=Strong Typing vs. Strong Testing |last=Eckel |first=Bruce |publisher=Google Docs }}</ref> Likewise, there is often no need to manually declare all types in statically typed languages with type inference; thus, the need for the programmer to explicitly specify types of variables is automatically lowered for such languages; and some dynamic languages have run-time optimisers<ref>{{cite web |url=http://www.mozilla.com/en-US/press/mozilla-2006-11-07.html |title=Adobe and Mozilla Foundation to Open Source Flash Player Scripting Engine }}</ref><ref>{{cite web |url=http://psyco.sourceforge.net/introduction.html |title=Psyco, a Python specializing compiler }}</ref> Rovněž zde často není potřeba manuálně deklarovat všechny typy jako ve staticky typovaných jazycích s typovým odvozováním. Tím se pro programátora automaticky snižuje pro takovéto jazyky nutnost výslovně specifikovat typy proměnných a některé dynamicky typované jazyky dokonce mají runtime optimalizaci, která dokáže generovat kód blížící se v rychlosti překladačům statických jazyků, často s pomocí částečného typového usuzování. == Literatura == * Smith, Chris, [http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/ ''What To Know Before Debating Type Systems''] * Tratt, Laurence, [http://tratt.net/laurie/research/publications/html/tratt__dynamically_typed_languages/ ''Dynamically Typed Languages''], Advances in Computers, Vol. 77, pp. 149–184, July 2009 == Související články == * [[Polymorfismus (programování)|Přetěžování operátorů]] * [[Polymorfismus (programování)|Polymorfizmus v objektově orientovaném programování]] * [[Programovací jazyk]] == Reference == <references /> {{Článek z Wikipedie}} {{DEFAULTSORT:Typový Systém}} [[Kategorie:Datové typy]]

Návrat na stránku „Typový systém“.