Typový systém - Type system

V programovacích jazycích , je systém typu je logický systém, který obsahuje soubor pravidel, který přiřazuje vlastnost zvanou typ s různými konstrukcemi s počítačovým programem , jako jsou proměnné , výrazy , funkce či moduly . Tyto typy formalizují a prosazují jinak implicitní kategorie, které programátor používá pro algebraické datové typy , datové struktury nebo jiné komponenty (např. „Řetězec“, „pole float“, „funkce vracející boolean“). Hlavním účelem typového systému je omezit možnosti výskytu chyb v počítačových programech definováním rozhraní mezi různými částmi počítačového programu a následnou kontrolou, zda jsou součásti spojeny konzistentním způsobem. Tato kontrola může probíhat staticky (v době kompilace ), dynamicky (za běhu ) nebo jako kombinace obojího. Typové systémy mají i jiné účely, například vyjádření obchodních pravidel, povolení určitých optimalizací kompilátoru , umožnění vícenásobného odeslání , poskytnutí formy dokumentace atd.

Typový systém spojuje typ s každou vypočítanou hodnotou a zkoumáním toku těchto hodnot se pokouší zajistit nebo dokázat, že nemůže dojít k žádným typovým chybám . Daný daný typový systém určuje, co představuje chybu typu, ale obecně je cílem zabránit tomu, aby se operace očekávající určitý druh hodnoty používaly s hodnotami, pro které tato operace nedává smysl (chyby platnosti). Typové systémy jsou často specifikovány jako součást programovacích jazyků a zabudovány do tlumočníků a překladačů, ačkoli typový systém jazyka lze rozšířit o volitelné nástroje, které provádějí přidané kontroly pomocí původní syntaxe a gramatiky jazyka.

Přehled použití

Příkladem jednoduchého systému typu je to, že v jazyce C . Části programu C jsou definice funkcí . Jedna funkce je vyvolána jinou funkcí. Rozhraní funkce uvádí název funkce a seznam parametrů, které jsou předány do kódu funkce. Kód vyvolávající funkce uvádí název vyvolaného spolu s názvy proměnných, které uchovávají hodnoty, které mu mají být předány. Během provádění jsou hodnoty umístěny do dočasného úložiště, poté provedení přeskočí na kód vyvolané funkce. Kód vyvolané funkce přistupuje k hodnotám a využívá je. Pokud jsou instrukce uvnitř funkce napsány s předpokladem přijetí celočíselné hodnoty, ale volající kód předal hodnotu s plovoucí desetinnou čárkou , pak bude vyvolaná funkce vypočítána špatný výsledek. Kompilátor C kontroluje typy argumentů předaných funkci, když je volána proti typům parametrů deklarovaných v definici funkce. Pokud se typy neshodují, kompilátor vyvolá chybu při kompilaci.

Kompilátor může také použít typ statického o hodnotu pro optimalizaci ukládání, kterou potřebuje a výběr algoritmu pro operace na hodnotě. V mnoha kompilátorech C je například datový typ float reprezentován 32 bity v souladu se specifikací IEEE pro čísla s plovoucí desetinnou čárkou s jednoduchou přesností . Na těchto hodnotách tedy budou používat mikroprocesorové operace specifické s pohyblivou řádovou čárkou (sčítání s plovoucí desetinnou čárkou, násobení atd.).

Hloubka omezení typu a způsob jejich vyhodnocení ovlivňují psaní jazyka. Programovací jazyk může dále přiřadit operaci s různým rozlišením pro každý typ, v případě typu polymorfismus . Teorie typů je studium typových systémů. Konkrétní typy některých programovacích jazyků, jako jsou celá čísla a řetězce, závisí na praktických problémech počítačové architektury, implementace kompilátoru a jazykového designu.

Základy

Formálně teorie typů studuje typové systémy. Programovací jazyk musí mít možnost zadat kontrolu pomocí typového systému, ať už v době kompilace nebo za běhu, ručně opatřenou poznámkou nebo automaticky odvozenou. Jak výstižně vyjádřil Mark Manasse :

Základní problém, který řeší teorie typů, je zajistit, aby programy měly smysl. Základní problém způsobený teorií typů spočívá v tom, že smysluplné programy nemusí mít žádný význam. Z tohoto napětí vyplývá hledání bohatších typů systémů.

Přiřazení datového typu, nazývaného psaní , dává význam posloupnosti bitů , jako je hodnota v paměti nebo některému objektu , jako je proměnná . Hardware počítače pro obecné účely není schopen rozlišovat například mezi adresou paměti a kódem instrukce nebo mezi znakem , celým číslem nebo číslem s plovoucí desetinnou čárkou , protože nedělá žádné vnitřní rozlišení mezi žádnými z možných hodnot, které posloupnost bitů může znamenat . Sdružení sekvence bitů s typem přenáší tento význam na programovatelný hardware a vytváří symbolický systém složený z tohoto hardwaru a nějakého programu.

Program spojuje každou hodnotu s alespoň jedním konkrétním typem, ale může se také stát, že jedna hodnota je spojena s mnoha podtypy . K typu mohou být přidruženy další entity, jako jsou objekty , moduly , komunikační kanály a závislosti . I typ může být přidružen k typu. Implementace typového systému by teoreticky mohla spojovat identifikace nazývané datový typ (typ hodnoty), třída (typ objektu) a druh ( typ typu nebo metatyp). Toto jsou abstrakce, kterými může psaní procházet, v hierarchii úrovní obsažených v systému.

Když programovací jazyk vyvíjí propracovanější typový systém, získává jemněji zrnitou sadu pravidel než základní kontrolu typu, ale to stojí za cenu, když se závěry typu (a další vlastnosti) stanou nerozhodnutelnými a kdy musí být věnována větší pozornost programátor k anotaci kódu nebo k zvážení operací a fungování souvisejících s počítačem. Je náročné najít dostatečně expresivní typový systém, který by bezpečným způsobem vyhovoval všem programovacím postupům .

Čím více omezení typu, která jsou uložená kompilátor, tím více silně napsaný programovací jazyk. Silně napsané jazyky často vyžadují, aby programátor provedl explicitní převody v kontextech, kde by implicitní převod nepoškodil. Systém typu Pascal byl popsán jako „příliš silný“, protože například velikost pole nebo řetězce je součástí jeho typu, což ztěžuje některé programovací úlohy. Haskell je také silně typovaný, ale jeho typy jsou automaticky odvozeny, takže explicitní převody jsou často zbytečné.

Kompilátor programovacího jazyka může také implementovat závislý typ nebo efektový systém , který umožňuje ještě více specifikací programu ověřit pomocí kontroly typu. Kromě jednoduchých párů typu hodnota je virtuální „oblast“ kódu spojena s komponentou „efekt“, která popisuje, co se s čím provádí , a umožňuje například „vyhodit“ chybovou zprávu. Symbolický systém tedy může být systémem typu a efektu , který mu dává větší kontrolu bezpečnosti než samotnou kontrolu typu.

Ať už je to typový systém automatizovaný kompilátorem nebo určený programátorem, činí chování programu nezákonným, pokud je mimo pravidla typového systému. Mezi výhody poskytované systémy typu specifikovaného programátorem patří:

Abstrakce (nebo modularita )-Typy umožňují programátorům přemýšlet na vyšší úrovni než bit nebo byte, neobtěžují se implementací na nízké úrovni. Například programátoři mohou začít považovat řetězec za sadu hodnot znaků místo za pouhé pole bajtů. A co víc , typy umožňují programátorům přemýšlet a vyjadřovat rozhraní mezi dvěma subsystémy jakékoli velikosti. To umožňuje více úrovní lokalizace, takže definice požadované pro interoperabilitu subsystémů zůstávají konzistentní, když tyto dva subsystémy komunikují.
Dokumentace - V expresivnějších typových systémech mohou typy sloužit jako forma dokumentace objasňující záměr programátora. Pokud například programátor deklaruje funkci jako návrat typu časového razítka, dokumentuje to funkci, když lze typ časového razítka explicitně deklarovat hlouběji v kódu jako celočíselný typ.

Mezi výhody poskytované systémy typu specifikovaného kompilátorem patří:

Optimalizace -Statická kontrola typu může poskytnout užitečné informace při kompilaci. Pokud například typ vyžaduje, aby se hodnota musela v paměti zarovnat na násobek čtyř bajtů, kompilátor může být schopen používat efektivnější strojové instrukce.
Bezpečnost - Typový systém umožňuje kompilátoru detekovat nesmyslný nebo neplatný kód. Můžeme například identifikovat výraz 3 / "Hello, World"jako neplatný, když pravidla neurčují, jak rozdělit celé číslo na řetězec . Silné psaní nabízí větší bezpečnost, ale nemůže zaručit úplnou bezpečnost typu .

Typové chyby

Chyba typu je nezamýšlená podmínka, která se může projevit ve více fázích vývoje programu. V typovém systému je tedy zapotřebí zařízení pro detekci chyby. V některých jazycích, jako je Haskell, u nichž je odvozování typů automatizováno, může být jeho kompilátoru k dispozici lint, který pomáhá při detekci chyb.

Bezpečnost typu přispívá ke správnosti programu , ale může zaručit správnost pouze za cenu toho, že se samotná kontrola typu stane nerozhodnutelným problémem . V typovém systému s automatizovanou kontrolou typu se může ukázat, že program běží nesprávně, ale nevytváří žádné chyby kompilátoru. Dělení nulou je nebezpečná a nesprávná operace, ale kontrola typu spuštěná v době kompilace ve většině jazyků pouze nehledá dělení nulou a poté je ponechána jako chyba runtime . K prokázání absence těchto vad se běžně používají jiné druhy formálních metod , souhrnně známé jako programové analýzy . Alternativně dostatečně expresivní typový systém, například v závisle napsaných jazycích, může těmto druhům chyb zabránit (například vyjádřit typ nenulových čísel ). Kromě testování softwaru je empirická metoda pro hledání chyb, které kontrola typu nelze detekovat.

Kontrola typu

Proces ověřování a vynucování omezení typů-kontrola typu- může nastat v době kompilace (statická kontrola) nebo za běhu . Pokud jazyková specifikace vyžaduje svá pravidla pro psaní silně (tj. Víceméně povoluje pouze ty automatické převody typů , které neztrácejí informace), lze tento proces označit jako silně typovaný , pokud ne, jako slabě typovaný . Termíny se obvykle nepoužívají v přísném smyslu.

Statická kontrola typu

Statická kontrola typu je proces ověření typové bezpečnosti programu na základě analýzy textu programu ( zdrojový kód ). Pokud program projde kontrolou statického typu, pak je zaručeno, že program splní určitou sadu vlastností bezpečnosti typu pro všechny možné vstupy.

Statickou kontrolu typu lze považovat za omezenou formu ověřování programu (viz bezpečnost typu ) a v jazyce bezpečném pro typ lze považovat také za optimalizaci. Pokud kompilátor dokáže, že je program dobře napsaný, nemusí vydávat dynamické bezpečnostní kontroly, takže výsledný kompilovaný binární soubor poběží rychleji a bude menší.

Statická kontrola typu pro Turingovo-úplné jazyky je ze své podstaty konzervativní. To znamená, že pokud je typový systém jak zvukový (to znamená, že odmítá všechny nesprávné programy), tak rozhodnutelný (což znamená, že je možné napsat algoritmus, který určuje, zda je program dobře napsaný), pak musí být neúplný (tj. jsou správné programy, které jsou také odmítnuty, přestože nenarazí na chyby za běhu). Zvažte například program obsahující kód:

if <complex test> then <do something> else <signal that there is a type error>

I když se výraz za běhu <complex test>vždy vyhodnotí na true, většina kontrolerů typu odmítne program jako špatně zadaný, protože je pro statický analyzátor obtížné (ne-li nemožné) určit, že elsevětev nebude převzata. V důsledku toho bude kontrola statického typu rychle detekovat chyby typu v zřídka používaných cestách kódu. Bez kontroly statického typu nemusí být takové chyby typu schopny najít ani testy pokrytí kódem se 100% pokrytím. Testy nemusí detekovat takové chyby typu, protože je třeba vzít v úvahu kombinaci všech míst, kde se vytvářejí hodnoty, a všech míst, kde se používá určitá hodnota.

Řadu užitečných a běžných funkcí programovacího jazyka nelze kontrolovat staticky, například downcasting . Mnoho jazyků tedy bude mít kontrolu statického i dynamického typu; kontrola statického typu ověří, co může, a dynamické kontroly ověří zbytek.

Mnoho jazyků se statickou kontrolou typu poskytuje způsob, jak obejít kontrolu typu. Některé jazyky umožňují programátorům volit mezi bezpečností statického a dynamického typu. C# například rozlišuje proměnné se statickým typem a dynamicky typované . Použití prvního z nich se kontroluje staticky, zatímco použití druhého se kontroluje dynamicky. Jiné jazyky umožňují psaní kódu, který není typově bezpečný; například v jazyce C mohou programátoři libovolně přenášet hodnotu mezi libovolné dva typy, které mají stejnou velikost, čímž efektivně rozvracejí koncept typu.

Seznam jazyků s kontrolou statického typu najdete v kategorii pro staticky zadané jazyky .

Dynamická kontrola typu a informace o typu za běhu

Dynamická kontrola typu je proces ověření typové bezpečnosti programu za běhu. Implementace dynamicky kontrolovaných jazyků obecně spojují každý běžecký objekt se značkou typu (tj. Odkazem na typ), která obsahuje informace o jeho typu. Tuto informaci o typu runtime (RTTI) lze také použít k implementaci dynamického odesílání , pozdní vazby , downcastingu , reflexe a podobných funkcí.

Většina jazyků bezpečných pro typ obsahuje nějakou formu dynamické kontroly typů, i když mají také kontrolu statického typu. Důvodem je to, že mnoho užitečných funkcí nebo vlastností je obtížné nebo nemožné ověřit staticky. Předpokládejme například, že program definuje dva typy, A a B, kde B je podtyp A. Pokud se program pokusí převést hodnotu typu A na typ B, který je známý jako downcasting , pak je operace legální pouze pokud je převáděná hodnota ve skutečnosti hodnotou typu B. Je tedy zapotřebí dynamické kontroly, která ověří, zda je operace bezpečná. Tento požadavek je jednou z kritik downcastingu.

Podle definice může dynamická kontrola typu způsobit selhání programu za běhu. V některých programovacích jazycích je možné tyto chyby předvídat a zotavit se z nich. V ostatních případech jsou chyby kontroly typu považovány za smrtelné.

Programovací jazyky, které zahrnují dynamickou kontrolu typu, ale nikoli kontrolu statického typu, se často nazývají „dynamicky psané programovací jazyky“. Seznam těchto jazyků najdete v kategorii pro dynamicky psané programovací jazyky .

Kombinace statické a dynamické kontroly typu

Některé jazyky umožňují statické i dynamické psaní. Například Java a některé další zdánlivě staticky napsané jazyky podporují typy downcastingu na své podtypy , dotazují se na objekt, aby objevily jeho dynamický typ, a další operace typu, které závisí na informacích o typu runtime. Dalším příkladem je C ++ RTTI . Obecněji řečeno, většina programovacích jazyků obsahuje mechanismy pro odesílání přes různé 'druhy' dat, jako jsou disjunktní odbory , runtime polymorfismus a typy variant . I když neinteragují s anotacemi typu nebo kontrolou typu, jsou takové mechanismy věcně podobné implementacím dynamického psaní. Další informace o interakcích mezi statickým a dynamickým typováním najdete v programovacím jazyce .

K objektům v objektově orientovaných jazycích se obvykle přistupuje pomocí odkazu, jehož statický cílový typ (nebo typ manifestu) se rovná buď typu run-time objektu (jeho latentní typ), nebo jeho nadtypu. To je v souladu s Liskovovým substitučním principem , který říká, že všechny operace prováděné na instanci daného typu lze provádět i na instanci podtypu. Tento koncept je také známý jako subsumption nebo subtypový polymorfismus . V některých jazycích mohou podtypy také mít kovariantní nebo protichůdné návratové typy a typy argumentů.

Některé jazyky, například Clojure , Common Lisp nebo Cython, jsou ve výchozím nastavení dynamicky kontrolovány, ale umožňují programům přihlásit se ke kontrole statického typu poskytováním volitelných anotací. Jedním z důvodů použití takových rad by byla optimalizace výkonu kritických částí programu. Toto je formalizováno postupným zadáváním . Programovací prostředí DrRacket , pedagogické prostředí založené na Lispu a předchůdce jazyka Racket, je také měkké.

Naopak od verze 4.0 jazyk C# poskytuje způsob, jak indikovat, že proměnná by neměla být kontrolována staticky. Proměnná, jejíž typ je, dynamicnebude podléhat statické kontrole typu. Místo toho program spoléhá na informace o typu runtime, aby určil, jak lze proměnnou použít.

V Rust je typ nabízí dynamické typování typů. std::any'static

Statická a dynamická kontrola typu v praxi

Volba mezi statickým a dynamickým typováním vyžaduje určité kompromisy .

Statické psaní může v době kompilace spolehlivě najít chyby typu, což zvyšuje spolehlivost dodaného programu. Programátoři však nesouhlasí s tím, jak často dochází k chybám typu, což má za následek další neshody ohledně podílu těch chyb, které jsou kódovány a které by byly zachyceny vhodnou reprezentací navržených typů v kódu. Obhájci statického psaní věří, že programy jsou spolehlivější, pokud byly dobře zkontrolovány, zatímco obhájci dynamického psaní poukazují na distribuovaný kód, který se ukázal spolehlivý, a na databáze malých chyb. Hodnota statického psaní se zvyšuje, jak se zvyšuje síla typového systému. Zastánci závislého psaní , implementovaní v jazycích, jako je Dependent ML a Epigram , navrhli, že téměř všechny chyby lze považovat za typové chyby, pokud jsou typy použité v programu správně deklarovány programátorem nebo správně odvozeny kompilátorem.

Statické psaní má obvykle za následek zkompilovaný kód, který se spouští rychleji. Když kompilátor zná přesné datové typy, které se používají (což je nezbytné pro statické ověření, buď prostřednictvím deklarace, nebo odvození), může vytvořit optimalizovaný strojový kód. Některé dynamicky zadávané jazyky, jako například Common Lisp, umožňují z tohoto důvodu optimalizaci volitelných deklarací typů.

Naproti tomu dynamické psaní může kompilátorům umožnit rychlejší běh a překladačům dynamické načítání nového kódu, protože změny zdrojového kódu v jazycích s dynamickým typem mohou mít za následek menší kontrolu provádění a méně revizí kódu. I to může omezit cyklus edit-compile-test-debug.

Staticky zadané jazyky, které postrádají odvozování typů (například C a Java před verzí 10 ), vyžadují, aby programátoři deklarovali typy, které musí metoda nebo funkce používat. To může sloužit jako přidaná programová dokumentace, která je aktivní a dynamická, namísto statické. To umožňuje kompilátoru zabránit jeho driftování mimo synchronizaci a jeho ignorování programátory. Jazyk však lze staticky psát bez nutnosti deklarace typu (příklady zahrnují Haskell , Scala , OCaml , F# a v menší míře C# a C ++ ), takže explicitní deklarace typu není nezbytným požadavkem pro statické psaní ve všech jazycích.

Dynamické psaní umožňuje konstrukty, které by některé (jednoduché) statické kontroly typu odmítly jako nezákonné. Možné jsou například eval funkce, které spouští libovolná data jako kód. Eval funkce je možné statické psaní, ale vyžaduje pokročilé využití algebraických datových typů . Dynamické psaní dále lépe vyhovuje přechodnému kódu a prototypování, například umožňuje transparentní použití zástupné datové struktury ( falešný objekt ) namísto úplné datové struktury (obvykle pro účely experimentování a testování).

Dynamické psaní obvykle umožňuje psaní kachen (což umožňuje snadnější opětovné použití kódu ). Mnoho jazyků se statickým psaním také nabízí psaní kachen nebo jiné mechanismy, jako je generické programování, které také umožňují snadnější opětovné použití kódu.

Dynamické psaní obvykle usnadňuje používání metaprogramování . Například šablony C ++ jsou obvykle těžší na psaní než ekvivalentní kód Ruby nebo Python, protože C ++ má silnější pravidla týkající se definic typů (pro funkce i proměnné). To nutí vývojáře napsat více standardního kódu pro šablonu, než by vývojář Pythonu potřeboval. Pokročilejší běhové konstrukce, jako jsou metaklasy a introspekce, se ve staticky napsaných jazycích často hůře používají. V některých jazycích mohou být tyto funkce také použity např. Ke generování nových typů a chování za běhu na základě údajů za běhu. Takové pokročilé konstrukce často poskytují dynamické programovací jazyky ; mnoho z nich je napsáno dynamicky, přestože dynamické psaní nemusí souviset s dynamickými programovacími jazyky .

Silné a slabé systémy

Jazyky jsou často hovorově označovány jako silně nebo slabě napsané . Ve skutečnosti neexistuje žádná všeobecně přijímaná definice toho, co tyto pojmy znamenají. Obecně existují přesnější termíny, které představují rozdíly mezi typovými systémy, které vedou lidi k tomu, aby je nazývali „silní“ nebo „slabí“.

Typ bezpečnost a bezpečnost paměti

Třetím způsobem kategorizace typového systému programovacího jazyka je bezpečnost zadaných operací a převodů. Počítačoví vědci používají termín typově bezpečný jazyk k popisu jazyků, které neumožňují operace nebo převody, které porušují pravidla typového systému.

Počítačoví vědci používají termín jazyk bezpečný pro paměť (nebo jen bezpečný jazyk ) k popisu jazyků, které neumožňují programům přistupovat k paměti, která nebyla přiřazena k jejich použití. Například jazyk bezpečný pro paměť zkontroluje hranice pole , nebo také staticky zaručí (tj. V době kompilace před spuštěním), že přístupy polí mimo hranice pole způsobí chyby při kompilaci a možná i za běhu.

Zvažte následující program jazyka, který je bezpečný pro typ i pro paměť:

var x := 5;   
var y := "37"; 
var z := x + y;

V tomto případě zbude mít proměnná hodnotu 42. Ačkoli to nemusí být to, co programátor očekával, je to dobře definovaný výsledek. Pokud by yšlo o jiný řetězec, který nelze převést na číslo (např. „Hello World“), byl by výsledek také dobře definován. Všimněte si, že program může být bezpečný pro typ nebo pro paměť a přesto může selhat při neplatné operaci. To je pro jazyky, kde typový systém není dostatečně pokročilý, aby přesně specifikoval platnost operací na všech možných operandech. Pokud ale program narazí na operaci, která není typově bezpečná, je ukončení programu často jedinou možností.

Nyní zvažte podobný příklad v C:

int x = 5;
char y[] = "37";
char* z = x + y;
printf("%c\n", *z);

V tomto případě bude odkazovat na adresu paměti o pět znaků dále , což odpovídá třem znakům za koncovým nulovým znakem řetězce, na který ukazuje . Toto je paměť, ke které se neočekává přístup programu. Může obsahovat nesmyslná data a rozhodně neobsahuje nic užitečného. Jak ukazuje tento příklad, C není jazyk bezpečný pro paměť ani pro typ. zyy

Obecně platí, že bezpečnost typu a bezpečnost paměti jdou ruku v ruce. Například jazyk, který podporuje aritmetické převody ukazatelů a převody čísel na ukazatele (jako C), není bezpečný ani pro typ, protože umožňuje přístup k libovolné paměti, jako by to byla platná paměť jakéhokoli typu.

Další informace najdete v tématu bezpečnost paměti .

Variabilní úrovně kontroly typu

Některé jazyky umožňují použití různých úrovní kontroly v různých oblastech kódu. Mezi příklady patří:

use strictSměrnice v jazyce JavaScript a Perl platí silnější kontrolu.
declare(strict_types=1)V PHP na základě soubor umožňuje budou přijímány pouze proměnná přesný typ prohlášení typu, nebo TypeErrorbude hozen.
Option Strict OnV VB.NET umožňuje kompilátor požadovat konverzi mezi objekty.

K dosažení vyšší úrovně přísnosti lze použít také další nástroje, jako jsou lint a IBM Rational Purify .

Systémy volitelného typu

Bylo navrženo, zejména Giladem Brachou , aby volba typového systému byla nezávislá na volbě jazyka; že typový systém by měl být modul, který lze podle potřeby zapojit do jazyka. Věří, že je to výhodné, protože to, co nazývá systémy povinných typů, činí jazyky méně expresivními a kódem křehčími. Je obtížné splnit požadavek, aby typový systém neovlivňoval sémantiku jazyka.

Volitelné psaní souvisí s postupným zadáváním , ale je od něj odlišné . Zatímco obě disciplíny psaní lze použít k provádění statické analýzy kódu ( statické psaní ), systémy volitelného typu nevyžadují bezpečnost typů za běhu ( dynamické psaní ).

Polymorfismus a typy

Termín polymorfismus označuje schopnost kódu (zejména funkcí nebo tříd) působit na hodnoty více typů nebo schopnost různých instancí stejné datové struktury obsahovat prvky různých typů. Typové systémy, které umožňují polymorfismus, to obecně dělají, aby se zlepšil potenciál pro opakované použití kódu: v jazyce s polymorfismem potřebují programátoři implementovat datovou strukturu, jako je seznam nebo asociativní pole, pouze jednou, nikoli jednou pro každý typ prvek, se kterým ho plánují použít. Z tohoto důvodu počítačoví vědci někdy nazývají používání určitých forem polymorfismu generickým programováním . Typově teoretické základy polymorfismu úzce souvisí se základy abstrakce , modularity a (v některých případech) podtypů .

Systémy specializovaného typu

Bylo vytvořeno mnoho typových systémů, které jsou specializované pro použití v určitých prostředích s určitými typy dat nebo pro out-of-band statickou programovou analýzu . Č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ů.

Následující tabulka poskytuje přehled teoretických konceptů typů, které se používají ve specializovaných typových systémech. Názvy $M, N, O se$ pohybují nad výrazy a názvy se pohybují nad typy. Zápis (resp. ) Popisuje typ, který je výsledkem nahrazení všech výskytů typové proměnné $α$ (resp. Termínová proměnná $x$ ) v $τ$ typem $σ$ (resp. Člen $N$ ). ${\ Displaystyle \ sigma, \ tau}$ ${\ Displaystyle \ tau [\ alpha: = \ sigma]}$ ${\ Displaystyle \ tau [x: = N]}$

Pojem typu	Zápis	Význam
Funkce	${\ Displaystyle \ sigma \ to \ tau}$	Pokud $M$ má typ a $N$ má typ $σ$ , pak má aplikace typ $τ$ . ${\ Displaystyle \ sigma \ to \ tau}$ ${\ displaystyle M (N)}$
Produkt	${\ Displaystyle \ sigma \ times \ tau}$	Pokud $M$ má typ , pak je pár takový, že $N$ má typ $σ$ a $O$ má typ $τ$ . ${\ Displaystyle \ sigma \ times \ tau}$ ${\ displaystyle M = (N, O)}$
Součet	${\ Displaystyle \ sigma +\ tau}$	Pokud $M$ má typ , pak buď je první injekce tak, že $N$ má typ $σ$ , popř ${\ Displaystyle \ sigma +\ tau}$ ${\ Displaystyle M = \ iota _ {1} (N)}$ ${\ Displaystyle M = \ iota _ {2} (N)}$ je druhá injekce taková, že $N$ má typ $τ$ .
Průsečík	${\ Displaystyle \ sigma \ cap \ tau}$	Pokud $M$ má typ , pak $M$ má typ $σ$ a $M$ má typ $τ$ . ${\ Displaystyle \ sigma \ cap \ tau}$
svaz	${\ Displaystyle \ sigma \ cup \ tau}$	Pokud $M$ má typ , pak $M$ má typ $σ$ nebo $M$ má typ $τ$ . ${\ Displaystyle \ sigma \ cup \ tau}$
Záznam	${\ Displaystyle \ langle x: \ tau \ rangle}$	Pokud $M$ má typ , pak $M$ má člen $x,$ který má typ $τ$ . ${\ Displaystyle \ langle x: \ tau \ rangle}$
Polymorfní	${\ Displaystyle \ forall \ alpha. \ tau}$	Pokud $M$ má typ , pak $M$ má typ pro jakýkoli typ $σ$ . ${\ Displaystyle \ forall \ alpha. \ tau}$ ${\ Displaystyle \ tau [\ alpha: = \ sigma]}$
Existenční	${\ displaystyle \ existuje \ alpha. \ tau}$	Pokud $M$ má typ , pak $M$ má typ pro nějaký typ $σ$ . ${\ displaystyle \ existuje \ alpha. \ tau}$ ${\ Displaystyle \ tau [\ alpha: = \ sigma]}$
Rekurzivní	${\ Displaystyle \ mu \ alpha. \ tau}$	Pokud $M$ má typ , pak $M$ má typ . ${\ Displaystyle \ mu \ alpha. \ tau}$ ${\ Displaystyle \ tau [\ alpha: = \ mu \ alpha. \ tau]}$
Závislá funkce	${\ Displaystyle (x: \ sigma) \ to \ tau}$	Pokud $M$ má typ a $N$ má typ $σ$ , pak má aplikace typ . ${\ Displaystyle (x: \ sigma) \ to \ tau}$ ${\ displaystyle M (N)}$ ${\ Displaystyle \ tau [x: = N]}$
Závislý produkt	${\ Displaystyle (x: \ sigma) \ times \ tau}$	Pokud $M$ má typ , pak je pár takový, že $N$ má typ $σ$ a $O$ má typ . ${\ Displaystyle (x: \ sigma) \ times \ tau}$ ${\ displaystyle M = (N, O)}$ ${\ Displaystyle \ tau [x: = N]}$
Závislá křižovatka	${\ Displaystyle (x: \ sigma) \ cap \ tau}$	Pokud $M$ má typ , pak $M$ má typ $σ$ a $M$ má typ . ${\ Displaystyle (x: \ sigma) \ cap \ tau}$ ${\ Displaystyle \ tau [x: = M]}$
Familiární křižovatka	${\ Displaystyle \ bigcap _ {x: \ sigma} \ tau}$	Pokud $M$ má typ , pak $M$ má typ pro jakýkoli termín $N$ typu $σ$ . ${\ Displaystyle \ bigcap _ {x: \ sigma} \ tau}$ ${\ Displaystyle \ tau [x: = N]}$
Rodinný svaz	${\ Displaystyle \ bigcup _ {x: \ sigma} \ tau}$	Pokud $M$ má typ , pak $M$ má typ pro nějaký termín $N$ typu $σ$ . ${\ Displaystyle \ bigcup _ {x: \ sigma} \ tau}$ ${\ Displaystyle \ tau [x: = N]}$

Závislé typy

Závislé typy jsou založeny na myšlence použít skaláry nebo hodnoty k přesnějšímu popisu typu nějaké jiné hodnoty. Může to být například typ matice. Potom můžeme definovat pravidla pro psaní, jako je následující pravidlo pro násobení matic: ${\ displaystyle \ mathrm {matrix} (3,3)}$ ${\ displaystyle 3 \ times 3}$

{\ Displaystyle \ mathrm {matrix} _ {\ mathrm {multiply}}: \ mathrm {matrix} (k, m) \ times \ mathrm {matrix} (m, n) \ to \ mathrm {matrix} (k, n )}

kde $k$ , $m$ , $n$ jsou libovolné kladné celočíselné hodnoty. Na základě tohoto typového systému byla vytvořena varianta ML s názvem Dependent ML , ale protože typová kontrola pro konvenční závislé typy je nerozhodnutelná , ne všechny programy, které je používají, lze typově kontrolovat bez nějakých omezení. Závislé ML omezuje druh rovnosti, kterou může rozhodnout, na Presburgerovu aritmetiku .

Jiné jazyky, jako je Epigram, činí hodnotu všech výrazů v jazyce rozhodnutelnou, takže je možné rozhodnout o kontrole typu. Obecně je však důkaz rozhodnutelnosti nerozhodnutelný , takže mnoho programů vyžaduje ručně psané anotace, které mohou být velmi netriviální. Protože to brání procesu vývoje, mnoho jazykových implementací poskytuje snadnou cestu ven v podobě možnosti tuto podmínku deaktivovat. To však stojí za cenu toho, aby se kontrola typu spustila v nekonečné smyčce při podávání programů, které nekontrolují typ, což způsobí selhání kompilace.

Lineární typy

Lineární typy , založené na teorii lineární logiky a úzce související s typy jedinečnosti , jsou typy přiřazené hodnotám, které mají tu vlastnost, že na ně má vždy jeden a jediný odkaz. Ty jsou cenné pro popis velkých neměnných hodnot, jako jsou soubory, řetězce atd., Protože jakoukoli operaci, která současně zničí lineární objekt a vytvoří podobný objekt (například „ str= str + "a"“), lze optimalizovat „pod pokličkou“ na místo mutace. Normálně to není možné, protože takové mutace by mohly způsobit vedlejší účinky na části programu, které obsahují jiné odkazy na objekt, což by narušilo referenční průhlednost . Používají se také v prototypu operačního systému Singularity pro meziprocesovou komunikaci, což staticky zajišťuje, že procesy nemohou sdílet objekty ve sdílené paměti, aby se předešlo sporům. Clean jazyk (a Haskell like jazyka) používá tento typ systému, aby získal hodně rychlosti (ve srovnání s provedením hlubokou kopii), zatímco zbývající bezpečné.

Typy křižovatek

Křižovatkové typy jsou typy popisující hodnoty, které patří k oběma dalším dvěma daným typům s překrývajícími se sadami hodnot. Například ve většině implementací C má podepsaný znak rozsah -128 až 127 a nepodepsaný znak má rozsah 0 až 255, takže typ průniku těchto dvou typů by měl rozsah 0 až 127. Takový typ křižovatky by mohl být bezpečně předán do funkcí očekávajících buď podepsané nebo nepodepsané znaky, protože je kompatibilní s oběma typy.

Typy průniků jsou užitečné pro popis typů přetížených funkcí: například pokud „ → “ je typ funkcí, které berou celočíselný argument a vrací celé číslo, a „ → “ je typ funkcí, které berou argument float a vrací float, pak průnik těchto dvou typů lze použít k popisu funkcí, které dělají jeden nebo druhý, podle toho, jaký typ vstupu jim je dán. Taková funkce by mohla být předána do jiné funkce, která bezpečně očekává funkci „ → “; jednoduše by nevyužilo funkci „ → “. intintfloatfloatintintfloatfloat

V hierarchii podtříd je nejvíce odvozeným typem průsečík typu a typu předka (například jeho nadřazeného). Průsečík sourozeneckých typů je prázdný.

Jazyk Forsythe zahrnuje obecnou implementaci typů křižovatek. Omezenou formou jsou typy upřesnění .

Druhy odborů

Typy unie jsou typy popisující hodnoty, které patří k jednomu ze dvou typů. Například v C má podepsaný znak rozsah -128 až 127 a nepodepsaný znak má rozsah 0 až 255, takže spojení těchto dvou typů by mělo celkový "virtuální" rozsah -128 až 255, který může použít částečně v závislosti na tom, ke kterému členovi odboru je přistupováno. Jakákoli funkce zpracovávající tento typ sjednocení by se musela vypořádat s celými čísly v tomto úplném rozsahu. Obecněji řečeno, jedinou platnou operací na typu sjednocení jsou operace, které jsou platné na obou typech, které jsou sjednoceny . Koncept „unie“ C je podobný typům odborů, ale není bezpečný, protože umožňuje operace, které jsou platné pro oba typy, nikoli pro oba . Typy unie jsou důležité v programové analýze, kde se používají k reprezentaci symbolických hodnot, jejichž přesná povaha (např. Hodnota nebo typ) není známa.

V hierarchii podtřídy je typem předchůdce sjednocení typu a typu předka (například jeho nadřazeného). Spojení typů sourozenců je podtypem jejich společného předka (to znamená, že všechny operace povolené na jejich společném předkovi jsou povoleny na typu sjednocení, ale mohou mít také společné jiné platné operace).

Existenciální typy

Existenciální typy se často používají ve spojení s typy záznamů k reprezentaci modulů a abstraktních datových typů , kvůli jejich schopnosti oddělit implementaci od rozhraní. Například, typ "T = ∃X {a: X; f: (X → int);}" popisuje modul rozhraní, který má datový člen s názvem typu X a funkce nazvané f , které trvá parametr stejný typ X a vrátí celé číslo. To by mohlo být implementováno různými způsoby; například:

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

Tyto typy jsou oba podtypy obecnějšího existenciálního typu T a odpovídají konkrétním typům implementace, takže jakákoli hodnota jednoho z těchto typů je hodnotou typu T. Vzhledem k hodnotě „t“ typu „T“ víme, že „ tf (ta)“je dobře napsaný, bez ohledu na to, co je abstraktní typ X je. To poskytuje flexibilitu při výběru typů vhodných pro konkrétní implementaci, zatímco klienti, kteří používají pouze hodnoty typu rozhraní - existenciálního typu - jsou od těchto voleb izolovaní.

Obecně není možné, aby typyecker vyvodil, ke kterému existenciální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 anotovat každý modul jeho zamýšleným typem, např .:

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

Ačkoli abstraktní datové typy a moduly byly v programovacích jazycích implementovány již nějakou dobu, až v roce 1988 John C. Mitchell a Gordon Plotkin založili formální teorii pod heslem: „Abstraktní [datové] typy mají existenciální typ“. Teorie je lambda kalkul druhého typu, podobný systému F , ale s existenciální namísto univerzální kvantifikace.

Postupné psaní

Postupné psaní je typový systém, ve kterém lze proměnným přiřadit typ buď v době kompilace (což je statické psaní), nebo za běhu (což je dynamické psaní), což vývojářům softwaru umožňuje zvolit si buď paradigma typu podle potřeby, zevnitř jeden jazyk. Postupné psaní zejména používá speciální typ s názvem dynamický k reprezentaci staticky neznámých typů a postupné psaní nahrazuje pojem rovnosti typů novým vztahem zvaným konzistence, který spojuje dynamický typ s každým jiným typem. Vztah konzistence je symetrický, ale není přechodný.

Explicitní nebo implicitní deklarace a odvození

Mnoho systémů se statickým typem, jako jsou systémy C a Java, vyžaduje deklaraci typu : programátor musí explicitně přiřadit každou proměnnou konkrétnímu typu. Ostatní, jako například Haskell, provádějí odvozování typů : překladač vyvozuje závěry o typech proměnných podle toho, jak programátoři tyto proměnné používají. Například vzhledem k funkci, která sčítá a dohromady, kompilátor může odvodit, že a musí být čísla - protože sčítání je definováno pouze pro čísla. Jakékoli volání jinde v programu, které jako argument specifikuje nečíselný typ (například řetězec nebo seznam), by tedy signalizovalo chybu. f(x, y)xyxyf

Numerické a řetězcové konstanty a výrazy v kódu mohou a často znamenají typ v konkrétním kontextu. Například výraz 3.14může znamenat typ s plovoucí desetinnou čárkou , zatímco může znamenat seznam celých čísel-obvykle pole . [1, 2, 3]

Inference typu je obecně možná, pokud je v daném typovém systému vyčíslitelná . Navíc, i když inference nelze pro daný typový systém obecně spočítat, inference je často možná pro velkou podmnožinu programů v reálném světě. Systém Haskellova typu, verze Hindley – Milnera , je omezením systému Fω na takzvané polymorfní typy rank-1, ve kterých je odvození typu vypočitatelné. Většina kompilátorů Haskell umožňuje polymorfismus s libovolným hodnocením jako rozšíření, ale to činí odvození typu nepočitatelné. (Kontrola typu je však rozhodnutelná a programy 1. úrovně stále mají odvození typu; polymorfní programy vyšší úrovně jsou odmítnuty, pokud nejsou uvedeny explicitní anotace typů.)

Problémy s rozhodováním

Typ systém, který přiřazuje typy termínů v prostředích typu s použitím pravidla typu je přirozeně spojena s rozhodovací problémy s kontrolou typu , typability a typ osídlení .

Vzhledem k prostředí typu , termínu a typu rozhodněte, zda lze výrazu přiřadit typ v prostředí typu. ${\ displaystyle \ Gamma}$ ${\ displaystyle e}$ ${\ displaystyle \ tau}$ ${\ displaystyle e}$ ${\ displaystyle \ tau}$
Vzhledem k výrazu rozhodněte, zda existuje typové prostředí a typ takový, že tomuto výrazu lze přiřadit typ v prostředí typu . ${\ displaystyle e}$ ${\ displaystyle \ Gamma}$ ${\ displaystyle \ tau}$ ${\ displaystyle e}$ ${\ displaystyle \ tau}$ ${\ displaystyle \ Gamma}$
Vzhledem k typovému prostředí a typu rozhodněte, zda existuje termín , kterému lze typ v prostředí typu přiřadit . ${\ displaystyle \ Gamma}$ ${\ displaystyle \ tau}$ ${\ displaystyle e}$ ${\ displaystyle \ tau}$

Systém jednotného typu

Některé jazyky jako C# nebo Scala mají systém jednotného typu. To znamená, že všechny typy C# včetně primitivních typů dědí z jednoho kořenového objektu. Každý typ v C# dědí ze třídy Object. Některé jazyky, jako Java a Raku , mají kořenový typ, ale také primitivní typy, které nejsou objekty. Java poskytuje typy objektů wrapper, které existují společně s primitivními typy, takže vývojáři mohou používat buď typy objektů wrapper, nebo jednodušší neobjektové primitivní typy. Raku automaticky převádí primitivní typy na objekty při přístupu k jejich metodám.

Kompatibilita: ekvivalence a podtypování

Kontrola typu pro staticky napsaný jazyk musí ověřit, že typ jakéhokoli výrazu je konzistentní s typem očekávaným kontextem, ve kterém se tento výraz nachází. Například v příkazu o přiřazení formuláře musí být odvozený typ výrazu konzistentní s deklarovaným nebo odvozeným typem proměnné . Tento pojem konzistence, nazývaný kompatibilita , je specifický pro každý programovací jazyk. x := eex

Pokud jsou typ ea typ xshodné a přiřazení je pro tento typ povoleno, jedná se o platný výraz. V systémech nejjednodušších typů se tedy otázka, zda jsou dva typy kompatibilní, redukuje na otázku, zda jsou stejné (nebo ekvivalentní ). Různé jazyky však mají různá kritéria pro to, když jsou výrazy dvou typů chápány tak, že označují stejný typ. Tyto různé rovníkové teorie typů se velmi liší, dvěma extrémními případy jsou systémy strukturálních typů , ve kterých jsou libovolné dva typy, které popisují hodnoty se stejnou strukturou, ekvivalentní, a systémy nominativního typu , ve kterých žádné dva syntakticky odlišné výrazy typu neoznačují stejný typ ( tj . typy musí mít stejný „název“, aby byly stejné).

V jazycích s podtypem je vztah kompatibility složitější. Zejména pokud Bje podtypem A, pak hodnotu typu Blze použít v kontextu, kde Ase očekává typ typu ( kovarianční ), i když obráceně není pravdivý. Stejně jako ekvivalence je vztah podtypu pro každý programovací jazyk definován odlišně, přičemž je možné mnoho variací. Přítomnost parametrického nebo ad hoc polymorfismu v jazyce může mít také důsledky pro kompatibilitu typů.

Viz také

Poznámky

Reference

Další čtení

Cardelli, Luca ; Wegner, Peter (prosinec 1985). „O porozumění typům, abstrakci dat a polymorfismu“ (PDF) . Výpočetní průzkumy ACM . 17 (4): 471–523. CiteSeerX 10.1.1.117.695 . doi : 10,1145/6041,6042 . S2CID 2921816 .
Pierce, Benjamin C. (2002). Typy a programovací jazyky . Stiskněte MIT. ISBN 978-0-262-16209-8.
Cardelli, Luca (2004). „Typové systémy“ (PDF) . V Allen B. Tucker (ed.). CRC Handbook of Computer Science and Engineering (2. vyd.). Stiskněte CRC. ISBN 978-1584883609.
Tratt, Laurence (červenec 2009). „5. Dynamicky psané jazyky“ . Pokroky v počítačích . 77 . Elsevier. s. 149–184. doi : 10,1016/S0065-2458 (09) 01205-4 . ISBN 978-0-12-374812-6.

externí odkazy

Média související s typovými systémy na Wikimedia Commons
Smith, Chris (2011). „Co vědět před debatou o typových systémech“ .

Languages

In other projects