Na nejširší úrovni je typová teorie oborem matematiky a logiky, který nejprve vytvoří hierarchii typů, poté přiřadí každému matematickému (a případně i jinému) subjektu určitý typ. Objekty daného typu jsou sestaveny z objektů předchozího typu. Typy v tomto smyslu souvisí s metafyzickým pojmem typu. Bertrand Russell vynalezl typovou teorii v reakci na svůj objev, že naivní teorie množin byla postižena Russellovým paradoxem. Typová teorie se výrazně objevuje ve Whiteheadově a Russellově Principia Mathematica.
Vlastnost dokonalého čtverce může být významně predikována jak kardinálům, tak poměrům kardinálů; ale vlastnost lichá (nebo sudá) není pro poměry definována. Nejsme tak schopni odpovědět na otázku, zda 2/3 je lichá nebo sudá. (Nagel 1951).
V teorii programovacího jazyka, což je odvětví informatiky, poskytuje typová teorie formální základ pro návrh, analýzu a studium typových systémů. Mnoho počítačových vědců skutečně používá termín typová teorie k odkazu na formální studium typových systémů pro programovací jazyky, i když někteří jej omezují na studium abstraktnějších formalismů, jako je typový λ-kalkul.
Následující systém je Mendelsonův (1997, 289-293) ST. Doména kvantifikace je rozdělena do vzestupné hierarchie typů, přičemž všem jednotlivcům je přiřazen určitý typ. Kvantifikované proměnné se pohybují pouze přes jeden typ; proto je základní logikou logika prvního řádu. ST je „jednoduché“ (vzhledem k typové teorii Principia Mathematica) především proto, že všichni členové domény a kodomainu jakéhokoli vztahu musí být stejného typu.
Existuje nejnižší typ, jehož jednotlivci nemají členy a jsou členy druhého nejnižšího typu. Jednotlivci nejnižšího typu odpovídají urelementům určitých množinových teorií. Každý typ má další vyšší typ, analogický s představou nástupce v Peanově aritmetice. Zatímco ST mlčí o tom, zda existuje maximální typ, neurčitý počet typů nepředstavuje žádný problém. Tato fakta, připomínající Peanovy axiomy, činí pohodlné a konvenční přiřadit každému typu přirozené číslo, počínaje 0 pro nejnižší typ. Ale typová teorie nevyžaduje předchozí definici naturalů.
Symboly typické pro ST jsou primované proměnné a infix ∈. V kterémkoli daném vzorci mají všechny nenaprogramované proměnné stejný typ, zatímco primované proměnné (x’) se pohybují v rozmezí nejbližšího vyššího typu. Atomové vzorce ST mají dvě formy, x=y (identita) a y∈x ’. Symbol infix ∈ naznačuje zamýšlenou interpretaci, množinové členství.
Všechny proměnné, které se objevují v definici identity a v axiomech Extensionalita a Comprehension, se pohybují nad jednotlivci jednoho ze dvou po sobě jdoucích typů. Vlevo (vpravo) od ‚∈‘ se mohou objevit pouze nezaměřené (primované) proměnné, které se pohybují nad typem „lower“ („vyšší“). Formulace prvního řádu ST vylučuje kvantifikaci nad typy. Proto každá dvojice po sobě jdoucích typů vyžaduje svůj vlastní axiom Extensionality a Comprehension, což je možné, pokud níže uvedené Extensionality a Comprehension jsou brány jako schémata axiomů „pohybujících se nad“ typy.
ST odhaluje, jak může být typová teorie velmi podobná axiomatické teorii množin. Navíc propracovanější ontologie ST, zakotvená v tom, co se dnes nazývá „iterativní pojetí množin“, vytváří axiom (schémata), které jsou mnohem jednodušší než u konvenčních teorií množin, jako je ZFC, s jednoduššími ontologiemi. Teorie množin, jejichž výchozím bodem je typová teorie, ale jejichž axiomy, ontologie a terminologie se od výše uvedeného liší, zahrnují New Foundations a Scott-Potterovu teorii množin.
Tato část je pahýl. Můžete pomoci tím, že do ní přidáte.
Praktický dopad typové teorie
Nejviditelnější aplikace typové teorie je v konstrukci algoritmů typové kontroly ve fázi sémantické analýzy kompilátorů pro programovací jazyky.
Teorie typů se také hojně používá v teoriích sémantiky přirozeného jazyka. Nejběžnější konstrukce bere základní typy a pro jednotlivce a pravdivostní hodnoty a definuje množinu typů rekurzivně takto:
Komplexní typ je typ funkcí od entit typu k entitám typu . Tedy máme typy, jako jsou ty, které jsou interpretovány jako prvky množiny funkcí od entit k hodnotám pravdy, tj. charakteristické funkce množin jestli entit. Výraz typu je funkce od množin entit k hodnotám pravdy, tj. množina množin (charakteristická funkce a). Tento druhý typ je standardně považován za typ kvantifikátorů přirozeného jazyka, jako každý chlapec nebo nikdo (Montague 1973, Barwise a Cooper 1981).
Tato část je pahýl. Můžete pomoci tím, že do ní přidáte.
Spojení s konstruktivní logikou
Tato část je pahýl. Můžete pomoci tím, že do ní přidáte.
Tato část je pahýl. Můžete pomoci tím, že do ní přidáte.
Definice typového systému se liší, ale následující díky Benjaminu C. Piercovi zhruba odpovídá současnému konsensu v komunitě teorie programovacího jazyka:
[Typový systém je] únosná syntaktická metoda pro prokázání absence určitých programových chování klasifikací frází podle druhů hodnot, které vypočítávají. (Pierce 2002).
Jinými slovy, typový systém dělí hodnoty programu na množiny nazývané typy – tomu se říká přiřazení typu – a na základě typů, které jsou takto přiřazeny, činí určité chování programu nezákonným. Typový systém může například klasifikovat hodnotu „hello“ jako řetězec a hodnotu 5 jako číslo a zakázat programátorovi přidat „hello“ k 5 na základě tohoto přiřazení typu. V tomto typovém systému může program
by bylo nelegální. Tudíž jakýkoliv program povolený typovým systémem by prokazatelně nebyl zatížen chybným chováním při přidávání řetězců a čísel.
Návrh a implementace typových systémů je téma téměř stejně široké jako samotné téma programovacích jazyků. Zastánci typové teorie totiž běžně prohlašují, že návrh typových systémů je samotnou podstatou návrhu programovacího jazyka: „Navrhněte typový systém správně a jazyk se navrhne sám.“