V teorii typů je konstruktor typu polymorfně typovaný konstrukt formálního jazyka , který vytváří nové typy ze starých.
Příklady typických konstruktorů typů jsou typy produktů , typy funkcí a seznamy . Primitivní typy jsou reprezentovány konstruktory typu nulové arity . Nové typy lze konstruovat pomocí rekurzivního skládání typových konstruktorů.
Jednoduše zadaný lambda kalkul si lze představit jako jazyk s konstruktorem jediného typu, konstruktorem typu funkce. Currying umožňuje, aby typy produktů v typizovaném počtu lambda byly považovány za inline.
Typový konstruktor je v podstatě operátor typu n-ary ( eng. type operator , operátor nad typy), který bere nula nebo více typů jako vstup a vrací jiný typ. Když se používá currying , operátor typu -ary může být reprezentován po sobě jdoucími aplikacemi operátorů unárního typu. Typové operátory lze tedy považovat za jednoduše typovaný lambda kalkul , mající jediný typ, obvykle označovaný " " (čti " typ "), což je typ všech typů v základním jazyce, který lze v tomto případě nazvat charakteristické typy , které je odliší od typových operátorů v jejich vlastních kalkulových rodech typů . n*
Použití typových operátorů jako ospravedlnění pro jednoduše napsaný počet lambda je však více než pouhá formalizace – umožňuje to typové operátory vyššího řádu (viz Rod (teorie typů)#Příklady , polymorfismus ve vyšších rodech ). Typové operátory se mapují na druhou osu v lambda kostce , výsledkem je jednoduše zadaný lambda kalkul s typovými operátory λ ω . Kombinací typových operátorů s polymorfním lambda kalkulem ( systém F ) vzniká systém Fω .
Typové konstruktory se hojně používají v typovém programování .
V programovacích jazycích rodiny ML je typový konstruktor reprezentován funkcí nad typy — tzn. funkce, která přijímá některé typy jako vstup a vrací jiné typy. Optimalizační kompilátory provádějí tyto funkce staticky, tzn. v době kompilace (viz například MLton ).
Klasické dialekty ML ( Standard ML , OCaml ) používají n-ticovoun notaci pro konstruktory typu -ary . V Haskell jsou možné konstruktory typu Curried . Klasické dialekty ML používají postfixovou syntaxi (například „ “) při vytváření nových typů , zatímco Haskell používá syntaxi prefixů („ “). int listList Int
V moderních implementacích Standard ML jsou primitivní typy jako char, int, word, real, definovány v modulech standardních knihoven ( SML Basis ) jako konstruktory typu null-ary (podrobnosti viz ovládání číslic ML ). Takové klasické agregační typy , jako jsou pole a seznamy , jsou implementovány podobně, ale jsou již unárními konstruktory typu vector(pole neměnných prvků), array(pole proměnných prvků) a list.
Ve standardním ML existují dva různé konstrukty pro definování typových konstruktorů - typea datatype. První definuje alias pro existující typový konstruktor nebo jejich složení, druhý zavádí nový algebraický datový typ s vlastními konstruktory . Nově definované typové konstruktory mohou mít libovolný počet argumentů. Proměnná typu se používá jako argument konstruktoru typu . Typy parametrizované jedním nebo více argumenty se nazývají polymorfní ; typy bez argumentů jsou monomorfní.
datový typ t0 = T of int * skutečný (* 0 argumentů *) typ ' a t1 = ' a * int (* 1 argument *) datový typ ( ' a , ' b ) t2 = A | B typu ' a * ' b (* 2 argumenty *) ( ' a , ' b , ' c ) t3 = ' a * ( ' b -> ' c ) ( * 3 argumenty *)Jsou zde definovány čtyři typové konstruktory: t0, t1, t2a t3. Chcete-li vytvořit objekty typů 'a t1a , 'a t2musíte zavolat jejich konstruktory T a A.B
Příklad složení typových konstruktérů ukazující konstrukci nových typů:
typ t4 = t0 t1Zde je typ použit jako skutečná hodnota proměnné 'a typu konstruktoru typu . Výsledným typem je n-tice dvou prvků, z nichž druhý je celé číslo a první byl zkonstruován aplikací konstruktoru na n-tici celého čísla a real. t1t0 T
Složitější příklad:
zadejte ' a t5 = ( ' a , ' a , ' a ) t3 t1Objekty typu t5budou n-tice dvou prvků, z nichž první je speciální případ typu t3, ve kterém musí být všechny tři argumenty identické, a druhý je celé číslo.
Haskell již má tři konstrukty pro definování typových konstruktorů - type, dataa newtype.
Konstrukce typea jsou datapoužívány podobně typeve Standard ML , nicméně existují následující rozdíly: datatype
Příklad:
datový bod a = Pt a a _Ve všech jazycích rodiny ML jsou konstruktory typů a konstruktory hodnot v různých jmenných prostorech, takže v takových případech lze použít stejný identifikátor:
data Bod a = Bod a aPoužití algebraického typu má určitou režii na výkon, protože konstruktor hodnot je aplikován dynamicky. Jeho nahrazení aliasem typu (definovaným přes type) zvyšuje efektivitu, ale snižuje bezpečnost typu (protože je nemožné ovládat jedinečné vlastnosti nadstavbového typu, které zužují jeho použití vzhledem k základnímu typu). K vyřešení tohoto dilematu Haskell přidal konstrukci newtype:
newtype Bod a = Bod ( a , a )Takto definovaný typ může mít jeden a pouze jeden hodnotový konstruktor s právě jedním parametrem. Ve zdrojovém kódu jsou takové typy použity shodně s těmi, které jsou definovány přes data, což poskytuje typovou bezpečnost. Ve spustitelném kódu však neexistuje jako samostatná entita newtype, místo toho se používá typ jeho parametru konstruktoru. V tomto případě bude spustitelný kód pro operace s Point astejně efektivní jako kód pro operace s n-ticemi (a, a).
| Typy dat | |
|---|---|
| Neinterpretovatelné | |
| Numerický | |
| Text | |
| Odkaz | |
| Kompozitní | |
| abstraktní | |
| jiný | |
| související témata | |